Coordinate projection charts on affine planes

Delete coordinate a, retaining the Euclidean norm on the remaining coordinates.

The graph formula solving the omitted coordinate of a plane.

noncomputable def LiebThirring.planeProjection (a : Fin 3) (x : Position) : Planar

Delete coordinate a, retaining the Euclidean norm on the remaining coordinates.

Equations

• LiebThirring.planeProjection a x = WithLp.toLp 2 fun (i : Fin 2) => x.ofLp (a.succAbove i)

noncomputable def LiebThirring.planeGraph (n b : Position) (a : Fin 3) (_ha : n.ofLp a ≠ 0) (q : Planar) : Position

The graph formula solving the omitted coordinate of a plane.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LiebThirring.planeProjection_apply (a : Fin 3) (x : Position) (i : Fin 2) : (planeProjection a x).ofLp i = x.ofLp (a.succAbove i)

@[simp]

theorem LiebThirring.planeGraph_apply_same (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (q : Planar) : (planeGraph n b a ha q).ofLp a = b.ofLp a - (∑ i : Fin 2, n.ofLp (a.succAbove i) * (q.ofLp i - b.ofLp (a.succAbove i))) / n.ofLp a

@[simp]

theorem LiebThirring.planeGraph_apply_succAbove (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (q : Planar) (i : Fin 2) : (planeGraph n b a ha q).ofLp (a.succAbove i) = q.ofLp i

theorem LiebThirring.inner_sub_eq_coordinate_sum (n x b : Position) : inner ℝ n (x - b) = ∑ i : Fin 3, n.ofLp i * (x.ofLp i - b.ofLp i)

The Euclidean plane equation expanded in its three coordinates.

theorem LiebThirring.planeGraph_mem (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (q : Planar) : planeGraph n b a ha q ∈ affinePlane n b

The graph formula takes values on the plane when the deleted normal coordinate is nonzero.

@[simp]

theorem LiebThirring.planeProjection_planeGraph (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (q : Planar) : planeProjection a (planeGraph n b a ha q) = q

Projecting the graph returns its two parameters.

theorem LiebThirring.planeGraph_planeProjection (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (x : Position) (hx : x ∈ affinePlane n b) : planeGraph n b a ha (planeProjection a x) = x

Solving the normal equation reconstructs each point on the plane.

theorem LiebThirring.planeProjection_bijective (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) : Function.Bijective fun (x : ↥(affinePlane n b)) => planeProjection a ↑x

Coordinate deletion is bijective on a plane with nonzero corresponding normal component.

noncomputable def LiebThirring.planeProjectionLinear (a : Fin 3) : Position →ₗ[ℝ] Planar

Coordinate deletion as a linear map on Euclidean carriers.

Equations

• LiebThirring.planeProjectionLinear a = { toFun := LiebThirring.planeProjection a, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def LiebThirring.planeProjectionChart (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) : Planar ≃ᵃ[ℝ] Planar

Coordinate deletion after an orthonormal frame, as a bijective affine chart.

Equations

• LiebThirring.planeProjectionChart n b a ha F = AffineEquiv.ofBijective ⋯

theorem LiebThirring.planeProjectionChart_symm_frame (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) (q : Planar) : ↑(F ((planeProjectionChart n b a ha F).symm q)) = planeGraph n b a ha q

The inverse of the projection chart, followed by the frame, is the explicit plane graph.

theorem LiebThirring.map_planar_affineEquiv_volume (e : Planar ≃ᵃ[ℝ] Planar) : MeasureTheory.Measure.map (⇑e) MeasureTheory.volume = ENNReal.ofReal |(LinearMap.det ↑e.linear)⁻¹| • MeasureTheory.volume

A planar affine coordinate change rescales volume by its inverse absolute determinant.