HemisphereMeasure.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MahlerStokes.setLIntegral_slice line 14

Source documentation

Nonnegative Fubini in the distinguished coordinate; no integrability assumption is needed for the singular hemisphere area density.

theorem setLIntegral_slice {n : ℕ} (i : Fin (n+1)) {s : Set (Fin (n+1) → ℝ)}
    (hs : MeasurableSet s) (f : (Fin (n+1) → ℝ) → ℝ≥0∞) (hf : Measurable f) :
    (∫⁻ x in s, f x) = ∫⁻ y : Fin n → ℝ,
      ∫⁻ t in {t | i.insertNth t y ∈ s}, f (i.insertNth t y) := by
…

lemma OAI.MahlerStokes.measurableSet_hemisphereConeDomain line 34
theorem OAI.MahlerStokes.lintegral_hemisphereCone line 41
Source documentation
The nonnegative change of variables for radial hemisphere coordinates, with its computed Jacobian rather than an assumed surface integration law.
```
theorem lintegral_hemisphereCone {n : ℕ} (i : Fin (n+1))
    (g : (Fin (n+1) → ℝ) → ℝ≥0∞) :
    (∫⁻ z in coordBall (n+1) 1 ∩ {z | 0 < z i}, g z) =
      ∫⁻ x in hemisphereConeDomain i,
        ENNReal.ofReal ((x i)^n * (chord 1 (i.removeNth x))⁻¹) * g (hemisphereCone i x) := by
…
```
Mentions: OAI.MahlerStokes.coordBall, OAI.MahlerStokes.hemisphereConeDomain, OAI.MahlerStokes.chord, OAI.MahlerStokes.hemisphereCone
lemma OAI.MahlerStokes.lintegral_pow_unitInterval line 57
def OAI.MahlerStokes.coneStrip line 67
lemma OAI.MahlerStokes.measurableSet_coneStrip line 70
lemma OAI.MahlerStokes.coneStrip_subset line 74
theorem OAI.MahlerStokes.volume_hemisphereCone_strip line 80
Source documentation
Integrating the exact radial Jacobian leaves the hemisphere area density, with the inverse dimension factor appearing in the cone definition of area.
```
theorem volume_hemisphereCone_strip {n : ℕ} (i : Fin (n+1))
    {S : Set (Fin n → ℝ)} (hS : MeasurableSet S) (hSB : S ⊆ coordBall n 1) :
    volume (hemisphereCone i '' coneStrip i S) =
      ENNReal.ofReal ((n+1 : ℝ)⁻¹) * ∫⁻ y in S, ENNReal.ofReal (chord 1 y)⁻¹ := by
…
```
Mentions: OAI.MahlerStokes.coordBall, OAI.MahlerStokes.hemisphereCone, OAI.MahlerStokes.coneStrip, OAI.MahlerStokes.chord