OAI/Analysis/Mahler/StripGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.stripTau_nonneg line 11
2. lemma OAI.SymmetricMahler.stripTau_zero line 16
3. theorem OAI.SymmetricMahler.stripTau_eq_zero_iff line 21

   Source documentation

   No hidden zero away from the origin occurs in the literal tau.

   theorem stripTau_eq_zero_iff (A : J → I → ℝ)
       (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m)
       {z : (I → ℝ) × (I → ℝ)} (hz : z ∈ stripDomain A) :
       stripTau A m z = 0 ↔ z = 0 := by
   …

   Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau

4. theorem OAI.SymmetricMahler.manuscript_finite_strip_geometry line 40