OAI/Analysis/Mahler/ReferenceSphereIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.exists_unitary_referencePole line 10
2. lemma OAI.Mahler.sphereVolume_unitary line 25
3. lemma OAI.Mahler.normEnergy_boundaryFin_unitary line 34
4. lemma OAI.Mahler.reference_boundaryFin_on_tangent line 44
5. theorem OAI.Mahler.reference_boundary_density line 58

   Source documentation

   The actual reference logarithmic boundary form has the constant outward sphere density k!/2 in complex dimension k+1.

   theorem reference_boundary_density {k : ℕ} {x : ComplexEuclidean (k+1)} (hx : ‖x‖ = 1) :
       orientedDensity (sphereFrame k) (sphereVolume k)
         (boundaryFormFin (dcLinear (logTau (coordinateMap (k+1)))) x) x =
         (k.factorial : ℂ)/2 := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.orientedDensity, OAI.Mahler.sphereFrame, OAI.Mahler.sphereVolume, OAI.Mahler.boundaryFormFin, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.Mahler.coordinateMap

6. theorem OAI.Mahler.reference_boundary_flux line 88

   Source documentation

   Integration of the reference boundary form against Euclidean sphere area, with outward orientation and the dc convention.

   theorem reference_boundary_flux (k : ℕ) :
       sphereFlux k (boundaryFormFin (dcLinear (logTau (coordinateMap (k+1))))) =
         Real.pi^(k+1) := by
   …

   Mentions: OAI.Mahler.sphereFlux, OAI.Mahler.boundaryFormFin, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.Mahler.coordinateMap