OAI/Analysis/Mahler/EuclideanRegularLevels.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.euclideanRealCoordinates line 11
2. lemma OAI.SymmetricMahler.euclideanTau_eq_real line 15
3. lemma OAI.SymmetricMahler.euclideanDomain_eq_real line 21
4. theorem OAI.SymmetricMahler.euclideanSpecial_positive_regular line 30

   Source documentation

   Every positive level remains regular in the exact Euclidean coordinates used by the mass theorem. This uses the actual special map, without Sard.

   theorem euclideanSpecial_positive_regular (A : Matrix (Fin N) (Fin n) ℝ)
       (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
       {R : ℝ} (hR : 0 < R) {z : Mahler.ComplexEuclidean n}
       (hz : z ∈ euclideanStripDomain A) (hlevel : Mahler.tau (euclideanSpecialMap A m) z = R) :
       Function.Surjective (fderiv ℝ (Mahler.tau (euclideanSpecialMap A m)) z) := by
   …

   Mentions: OAI.SymmetricMahler.measurement, OAI.Mahler.ComplexEuclidean, OAI.SymmetricMahler.euclideanStripDomain, OAI.Mahler.tau, OAI.SymmetricMahler.euclideanSpecialMap