OAI/Analysis/Mahler/EuclideanMassDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.euclideanSpecial_jacobian line 11
2. theorem OAI.SymmetricMahler.euclideanSpecial_massDensity line 28

   Source documentation

   The complex Hessian has precisely the n! times Gram-determinant density used in the finite-strip mass bridge.

   theorem euclideanSpecial_massDensity (A : Matrix (Fin N) (Fin n) ℝ) (m : ℕ)
       {z : Mahler.ComplexEuclidean n} (hz : z ∈ euclideanStripDomain A) :
       Mahler.massDensity (euclideanSpecialMap A m) z =
         (Nat.factorial n : ℝ) * specialGramDet A m (euclideanCoordinates z) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.SymmetricMahler.euclideanStripDomain, OAI.Mahler.massDensity, OAI.SymmetricMahler.euclideanSpecialMap, OAI.SymmetricMahler.specialGramDet, OAI.SymmetricMahler.euclideanCoordinates

3. theorem OAI.SymmetricMahler.euclideanSpecial_massIntegral line 42

   Source documentation

   Measure transport converts the complex Euclidean mass integral to the real-coordinate integral. The integrands and domains are those of the general mass theorem and the finite-strip construction.

   theorem euclideanSpecial_massIntegral
       (hvolume : MeasurePreserving (euclideanCoordinates (n := n)))
   …

   Mentions: OAI.SymmetricMahler.euclideanCoordinates