LeanPool.Rupert.Equivalences.Util

Imported Lean Pool material for LeanPool.Rupert.Equivalences.Util.

noncomputable def projXyLinear : ℝ³ →ₗ[ℝ] ℝ²

Projecting from ℝ³ to ℝ² is linear

Equations

• projXyLinear = { toFun := projXy, map_add' := projXyLinear._proof_1, map_smul' := projXyLinear._proof_2 }

noncomputable def rotationAffine (rot : ↥SO3) : ℝ³ →ᵃ[ℝ] ℝ³

Rotation by an element of SO3, viewed as an affine map.

Equations

• rotationAffine rot = (Matrix.toEuclideanLin ↑rot).toAffineMap

noncomputable def offsetAffine (off : E 2) : ℝ² →ᵃ[ℝ] ℝ²

Translating is affine.

Equations

• offsetAffine off = { toFun := fun (v : ℝ²) => off + v, linear := LinearMap.id, map_vadd' := ⋯ }

noncomputable def projXyRotationIsAffine (rot : ↥SO3) : ℝ³ →ᵃ[ℝ] ℝ²

Projection of a rotated point onto the xy-plane, as an affine map.

Equations

• projXyRotationIsAffine rot = projXyLinear.toAffineMap.comp (rotationAffine rot)

noncomputable def fullTransformAffine (off : E 2) (rot : ↥SO3) : ℝ³ →ᵃ[ℝ] ℝ²

Full affine transform used for projected Rupert shadows.

Equations

• fullTransformAffine off rot = (offsetAffine off).comp (projXyRotationIsAffine rot)