SphereTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.sphereIsometry line 15
Source documentation
The actual restriction of a real linear isometry to the unit sphere.
```
def sphereIsometry (e : E ≃ₗᵢ[ℝ] F) : sphere (0 : E) 1 ≃ₜ sphere (0 : F) 1 := by
…
```
lemma OAI.MahlerStokes.sphereIsometry_cone_preimage line 25
theorem OAI.MahlerStokes.measurePreserving_sphereIsometry line 42
Source documentation
Surface area induced by ambient volume is transported without a factor by a volume-preserving real linear isometry.
```
theorem measurePreserving_sphereIsometry (e : E ≃ₗᵢ[ℝ] F)
    (μ : Measure E) (ν : Measure F) (he : MeasurePreserving e μ ν) :
    MeasurePreserving (sphereIsometry e) μ.toSphere ν.toSphere := by
…
```
Mentions: OAI.MahlerStokes.sphereIsometry

theorem OAI.MahlerStokes.measurePreserving_interleavedSphere line 55

Source documentation

The explicit interleaved real/complex map preserves the actual unit sphere area.

theorem measurePreserving_interleavedSphere (n : ℕ) :
    MeasurePreserving (sphereIsometry (interleavedEuclidean n))
      (volume : Measure (EuclideanSpace ℝ (Fin (n*2)))).toSphere
      (volume : Measure (EuclideanSpace ℂ (Fin n))).toSphere :=
…

Mentions: OAI.MahlerStokes.sphereIsometry, OAI.MahlerStokes.interleavedEuclidean

theorem OAI.MahlerStokes.integral_interleavedSphere line 63

Source documentation

No integrability hypothesis is needed for change of variables along the measure-preserving measurable equivalence.

theorem integral_interleavedSphere (n : ℕ)
    (f : sphere (0 : EuclideanSpace ℂ (Fin n)) 1 → ℝ) :
    (∫ x, f (sphereIsometry (interleavedEuclidean n) x)
      ∂(volume : Measure (EuclideanSpace ℝ (Fin (n*2)))).toSphere) =
    ∫ z, f z ∂(volume : Measure (EuclideanSpace ℂ (Fin n))).toSphere :=
…

Mentions: OAI.MahlerStokes.sphereIsometry, OAI.MahlerStokes.interleavedEuclidean