HemisphereArea.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.MahlerStokes.continuous_hemisphereGraph line 11
def OAI.MahlerStokes.hemisphereParam line 16
Source documentation
The upper hemisphere parametrization into the actual Euclidean unit sphere.
```
def hemisphereParam {n : ℕ} (i : Fin (n+1)) :
    coordBall n 1 → sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1 := fun y =>
…
```
Mentions: OAI.MahlerStokes.coordBall
lemma OAI.MahlerStokes.continuous_hemisphereParam line 23
lemma OAI.MahlerStokes.hemisphereParam_injective line 27
lemma OAI.MahlerStokes.hemisphereParam_range line 35
lemma OAI.MahlerStokes.hemisphereParam_measurableEmbedding line 63
lemma OAI.MahlerStokes.hemisphereCone_image_toLp line 68
lemma OAI.MahlerStokes.volume_toLp_image line 82
theorem OAI.MahlerStokes.toSphere_hemisphereParam_image line 93
Source documentation
The hemisphere chart pushes forward exactly the reciprocal-chord area measure. This is proved from the cone definition of volume.toSphere.
```
theorem toSphere_hemisphereParam_image {n : ℕ} (i : Fin (n+1))
    {S : Set (coordBall n 1)} (hS : MeasurableSet S) :
    (volume : Measure (EuclideanSpace ℝ (Fin (n+1)))).toSphere (hemisphereParam i '' S) =
      ∫⁻ y in (Subtype.val '' S), ENNReal.ofReal (chord 1 y)⁻¹ := by
…
```
Mentions: OAI.MahlerStokes.coordBall, OAI.MahlerStokes.hemisphereParam, OAI.MahlerStokes.chord
def OAI.MahlerStokes.hemisphereParameterArea line 117
Source documentation
Actual Euclidean hemisphere area in graph coordinates.
```
def hemisphereParameterArea (n : ℕ) : Measure (coordBall n 1) :=
…
```
Mentions: OAI.MahlerStokes.coordBall
lemma OAI.MahlerStokes.measurableSet_hemisphereRange line 121
theorem OAI.MahlerStokes.measurePreserving_hemisphereParam line 127
Source documentation
Full measure equality, sufficient for Bochner as well as nonnegative integration. No sphere integration identity is a premise.
```
theorem measurePreserving_hemisphereParam {n : ℕ} (i : Fin (n+1)) :
    MeasurePreserving (hemisphereParam i) (hemisphereParameterArea n)
      ((volume : Measure (EuclideanSpace ℝ (Fin (n+1)))).toSphere.restrict
        (range (hemisphereParam i))) := by
…
```
Mentions: OAI.MahlerStokes.hemisphereParam, OAI.MahlerStokes.hemisphereParameterArea