OAI/Analysis/Mahler/VerticalSpeed.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.vertical_speed_algebra line 12

   Source documentation

   The Cauchy--Riemann algebra on a real-level curve.

   theorem vertical_speed_algebra {z : ℂ} {t : ℝ}
       (hreal : (z*(1+Complex.I*(t : ℂ))).re = 0) (him : 0 < z.im) :
       (z*(1+Complex.I*(t : ℂ))).im = Complex.normSq z/z.im := by
   …

2. theorem OAI.SymmetricMahler.vertical_speed_algebra_pos line 23
3. def OAI.SymmetricMahler.polarCurve line 31
4. theorem OAI.SymmetricMahler.hasDerivAt_polarCurve line 35

   Source documentation

   The derivative of a polar curve with differentiable angle.

   theorem hasDerivAt_polarCurve {θ : ℝ → ℝ} {r t : ℝ} (hθ : HasDerivAt θ t r) :
       HasDerivAt (polarCurve θ)
         (Complex.exp ((θ r : ℂ)*Complex.I)*(1+Complex.I*((r*t : ℝ) : ℂ))) r := by
   …

   Mentions: OAI.SymmetricMahler.polarCurve

5. theorem OAI.SymmetricMahler.hasDerivAt_image_polarCurve line 51

   Source documentation

   The image curve's derivative is obtained by the actual complex chain rule.

   theorem hasDerivAt_image_polarCurve {F : ℂ → ℂ} {θ : ℝ → ℝ} {r t : ℝ} {g : ℂ}
       (hF : HasDerivAt F g (polarCurve θ r)) (hθ : HasDerivAt θ t r) :
       HasDerivAt (fun s => F (polarCurve θ s))
         ((g*Complex.exp ((θ r : ℂ)*Complex.I))*(1+Complex.I*((r*t : ℝ) : ℂ))) r := by
   …

   Mentions: OAI.SymmetricMahler.polarCurve

6. theorem OAI.SymmetricMahler.image_polarCurve_vertical_derivative line 61

   Source documentation

   Constancy of the real part forces the image curve to move upward under the angular derivative sign condition.

   theorem image_polarCurve_vertical_derivative {F : ℂ → ℂ} {θ : ℝ → ℝ}
       {r t q : ℝ} {g : ℂ}
       (hF : HasDerivAt F g (polarCurve θ r)) (hθ : HasDerivAt θ t r)
       (hlevel : ∀ᶠ s in 𝓝 r, (F (polarCurve θ s)).re = q)
       (him : 0 < (g*Complex.exp ((θ r : ℂ)*Complex.I)).im) :
       HasDerivAt (fun s => (F (polarCurve θ s)).im)
         (Complex.normSq (g*Complex.exp ((θ r : ℂ)*Complex.I)) /
           (g*Complex.exp ((θ r : ℂ)*Complex.I)).im) r := by
   …

   Mentions: OAI.SymmetricMahler.polarCurve