SphereNormalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.complexEuclidean_finrank_real line 11
def OAI.Mahler.sphereArea line 17
Source documentation
The concrete area measure induced by Euclidean volume on the unit sphere.
```
noncomputable def sphereArea (n : ℕ) : Measure (sphere (0 : ComplexEuclidean n) 1) :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
theorem OAI.Mahler.reference_sphere_density_integral line 22
Source documentation
The numerical integral for sphere normalization. This does not assume equality of the constant density and the reference exterior form.
```
theorem reference_sphere_density_integral (n : ℕ) (hn : 1 ≤ n) :
    (∫ _z : sphere (0 : ComplexEuclidean n) 1,
      ((n - 1).factorial : ℝ) / 2 ∂sphereArea n) = Real.pi ^ n := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereArea