RadiusSphereIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.positiveSphereDilation line 11
Source documentation
The positive radial parametrization, packaged as a homeomorphism so change of variables is valid even before proving integrability.
```
def positiveSphereDilation (k : ℕ) (r : ℝ) (hr : 0 < r) :
    sphere (0 : EuclideanSpace ℂ (Fin k)) 1 ≃ₜ sphere (0 : EuclideanSpace ℂ (Fin k)) r := by
…
```

theorem OAI.MahlerStokes.sphereFlux_eq_positiveRadiusAreaIntegral line 33

Source documentation

The actual radius-r sphere integral. Its measure is the positive dilation of volume.toSphere with tangential Jacobian r^(2k-1), exactly the construction used in Mahler.radiusSphereArea. No integration law is an assumption.

theorem sphereFlux_eq_positiveRadiusAreaIntegral {d k : ℕ} (h : d+1 = k*2)
    {r : ℝ} (hr : 0 < r)
    (ω : (Fin (d+1) → ℝ) → (Fin (d+1) → ℝ) [⋀^Fin d]→L[ℝ] ℝ)
    (hω : ContinuousOn ω {x | radiusSq x = r^2}) :
    sphereFlux r ω =
      ∫ z : sphere (0 : EuclideanSpace ℂ (Fin k)) r,
        coordinateSphereDensity r ω
          (ofLp ((complexSphereCoordinates d k h).symm (r⁻¹ • (z : EuclideanSpace ℂ (Fin k)))))
        ∂(ENNReal.ofReal (r^(2*k-1)) •
          (volume : Measure (EuclideanSpace ℂ (Fin k))).toSphere.map (positiveSphereDilation k r hr)) := by
…

Mentions: OAI.MahlerStokes.radiusSq, OAI.MahlerStokes.sphereFlux, OAI.MahlerStokes.coordinateSphereDensity, OAI.MahlerStokes.complexSphereCoordinates, OAI.MahlerStokes.positiveSphereDilation