Volume and derivative coordinates for slicing

Coordinate insertion is an isometric embedding on each line; coordinate deletion and insertion preserve Lebesgue volume as a product decomposition.

theorem LiebThirring.coordinateLine_zero_one_eq_basis (a : Fin 3) : coordinateLine a 0 1 = (EuclideanSpace.basisFun (Fin 3) ℝ) a

theorem LiebThirring.isometry_coordinateLine (a : Fin 3) (q : Planar) : Isometry (coordinateLine a q)

theorem LiebThirring.isClosedEmbedding_coordinateLine (a : Fin 3) (q : Planar) : Topology.IsClosedEmbedding (coordinateLine a q)

noncomputable def LiebThirring.coordinateSplit (a : Fin 3) : Position ≃ᵐ Planar × ℝ

Measure-preserving separation of a selected spatial coordinate from its plane.

Equations

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

theorem LiebThirring.coordinateSplit_preserving (a : Fin 3) : MeasureTheory.MeasurePreserving (⇑(coordinateSplit a)) MeasureTheory.volume MeasureTheory.volume

theorem LiebThirring.integral_coordinateLines (a : Fin 3) (f : Position → ℝ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : Position), f x = ∫ (q : Planar) (t : ℝ), f (coordinateLine a q t)

theorem LiebThirring.hasDerivAt_coordinateLine (a : Fin 3) (q : Planar) (t : ℝ) : HasDerivAt (coordinateLine a q) ((EuclideanSpace.basisFun (Fin 3) ℝ) a) t