OAI/Analysis/Mahler/GlobalPlanarMonotonicity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.strictMonoOn_planarPrimitive_global line 11

   Source documentation

   The original primitive is strictly increasing on every entire actual vertical section, including across its possible zero derivative at the origin.

   theorem strictMonoOn_planarPrimitive_global {m : ℕ} (hm : 0 < m) {q : ℝ}
       (hq : q ∈ Ioo (-1 : ℝ) 1) :
       StrictMonoOn (planarPrimitive m q) (verticalFiber q) := by
   …

   Mentions: OAI.SymmetricMahler.planarPrimitive, OAI.SymmetricMahler.verticalFiber