OAI/Geometry/ProjectionBody/AffineChartMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.measure_projected_affine_chart line 18

   Source documentation

   The volume of a projected affine chart, with its genuine linear Jacobian.

   theorem measure_projected_affine_chart (L : U →ₗ[ℝ] V) (c : V)
       (q : V →ₗ[ℝ] V) (s : Set U) :
       μHE[Module.finrank ℝ U] (q '' ((fun x => c + L x) '' s)) =
         ENNReal.ofReal (q.comp L).normDet * volume s := by
   …

2. theorem OAI.ProjectionCounterexample.measure_projected_transverse_intersection line 33

   Source documentation

   Intersecting a facet chart with a genuinely transverse affine equation has zero facet-dimensional measure, including after any linear projection.

   theorem measure_projected_transverse_intersection (L : U →ₗ[ℝ] V) (c : V)
       (q : V →ₗ[ℝ] V) (g : V →ₗ[ℝ] ℝ) (r : ℝ) (S T : Set V)
       (hS : S ⊆ (fun x => c + L x) '' (univ : Set U))
       (hT : T ⊆ {y | g y = r}) (hg : g.comp L ≠ 0) :
       μHE[Module.finrank ℝ U] (q '' (S ∩ T)) = 0 := by
   …