OAI/Analysis/Mahler/ImplicitAngle.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.exists_local_real_level line 14

   Source documentation

   The scalar implicit function theorem with the angular nonzero derivative as its explicit hypothesis.

   theorem exists_local_real_level {f : ℝ × ℝ → ℝ} {a b c : ℝ}
       (hC : ContDiffAt ℝ ∞ f (a,b))
       (hD : HasDerivAt (fun y => f (a,y)) c b) (hc : c ≠ 0) :
       ∃ θ : ℝ → ℝ, θ a = b ∧ ContDiffAt ℝ ∞ θ a ∧
         ∀ᶠ r in 𝓝 a, f (r,θ r) = f (a,b) := by
   …

2. lemma OAI.SymmetricMahler.contDiffAt_Q_uncurry line 44
3. lemma OAI.SymmetricMahler.contDiffAt_S_uncurry line 60
4. theorem OAI.SymmetricMahler.exists_local_angle line 78

   Source documentation

   A smooth local angular fiber exists at every point of the upper half-disk. This instantiates the implicit theorem with the actual power-series real part.

   theorem exists_local_angle {r θ : ℝ} (hr : 0 < r) (hr1 : r < 1)
       (hθ : 0 < θ) (hθπ : θ < Real.pi) :
       ∃ ψ : ℝ → ℝ, ψ r = θ ∧ ContDiffAt ℝ ∞ ψ r ∧
         ∀ᶠ s in 𝓝 r, MahlerConformal.Q s (ψ s) = MahlerConformal.Q r θ := by
   …

   Mentions: OAI.MahlerConformal.Q