Plane projection integration formula

Coordinate formulas for nonnegative extended integration on affine planes.

theorem LiebThirring.isClosedEmbedding_planeGraph (n b : Position) (a : Fin 3) (ha : n.ofLp a ≠ 0) : Topology.IsClosedEmbedding (planeGraph n b a ha)

The inverse coordinate projection chart is a closed embedding into ambient space.

theorem LiebThirring.planeMeasure_eq_projection_map (n b : Position) (hn : ‖n‖ = 1) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) : planeMeasure F = ENNReal.ofReal |n.ofLp a|⁻¹ • MeasureTheory.Measure.map (planeGraph n b a ha) MeasureTheory.volume

The plane surface measure equals the explicit graph pushforward times the inverse absolute normal coordinate.

theorem LiebThirring.integrable_planeMeasure_projection_iff (n b : Position) (hn : ‖n‖ = 1) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) (h : Position → ℝ) : MeasureTheory.Integrable h (planeMeasure F) ↔ MeasureTheory.Integrable (h ∘ planeGraph n b a ha) MeasureTheory.volume

Real integrability on the plane is exactly integrability in the coordinate projection chart.

theorem LiebThirring.integral_planeMeasure_projection (n b : Position) (hn : ‖n‖ = 1) (a : Fin 3) (ha : n.ofLp a ≠ 0) (F : PlaneFrame (affinePlane n b)) (h : Position → ℝ) : ∫ (x : Position), h x ∂planeMeasure F = |n.ofLp a|⁻¹ * ∫ (q : Planar), h (planeGraph n b a ha q)

Real coordinate projection formula (3.2). The closed embedding also makes this valid for the total Bochner integral convention; integrable_planeMeasure_projection_iff identifies the integrable locus.