OAI/Analysis/Mahler/EuclideanSpecialMap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.euclideanCoordinates line 11
2. def OAI.SymmetricMahler.euclideanStripDomain line 14
3. def OAI.SymmetricMahler.euclideanSpecialMap line 17
4. lemma OAI.SymmetricMahler.euclideanSpecialTau line 21
5. lemma OAI.SymmetricMahler.differentiableOn_euclideanSpecialMap line 26
6. lemma OAI.SymmetricMahler.euclideanSpecial_remainder line 31
7. lemma OAI.SymmetricMahler.euclideanSpecial_compact_closure line 50
8. theorem OAI.SymmetricMahler.euclideanSpecial_massHypotheses line 69

   Source documentation

   The mass hypotheses hold for the special map, including the Euclidean Taylor estimate.

   theorem euclideanSpecial_massHypotheses (A : Matrix (Fin N) (Fin n) ℝ)
       (hn : 1 ≤ n) (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 2 ≤ m) :
       Mahler.MassHypotheses n N m (euclideanStripDomain A)
         (euclideanSpecialMap A m) (specialLeadingPolynomial A m) := by
   …

   Mentions: OAI.SymmetricMahler.measurement, OAI.Mahler.MassHypotheses, OAI.SymmetricMahler.euclideanStripDomain, OAI.SymmetricMahler.euclideanSpecialMap, OAI.SymmetricMahler.specialLeadingPolynomial