OAI/Analysis/Mahler/ConformalSeries.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerConformal.term line 22
2. def OAI.MahlerConformal.series line 23
3. def OAI.MahlerConformal.F line 24
4. def OAI.MahlerConformal.H line 25
5. lemma OAI.MahlerConformal.odd_cast_ne line 27
6. lemma OAI.MahlerConformal.term_bound line 30
7. theorem OAI.MahlerConformal.summable_series line 36
8. lemma OAI.MahlerConformal.series_zero line 44
9. lemma OAI.MahlerConformal.term_deriv_one line 47
10. lemma OAI.MahlerConformal.term_deriv_two line 56
11. lemma OAI.MahlerConformal.derivative_bound line 64
12. theorem OAI.MahlerConformal.hasDerivAt_series_two line 70
13. theorem OAI.MahlerConformal.hasDerivAt_H line 84
14. lemma OAI.MahlerConformal.one_sub_ne line 105
15. lemma OAI.MahlerConformal.one_add_ne line 110
16. lemma OAI.MahlerConformal.one_sub_sq_ne line 113
17. def OAI.MahlerConformal.cayley line 118
18. theorem OAI.MahlerConformal.cayley_re_pos line 121

    Source documentation

    The branch-domain assertion for the logarithmic derivative.

    theorem cayley_re_pos {w : ℂ} (hw : ‖w‖ < 1) : 0 < (cayley w).re := by
    …

    Mentions: OAI.MahlerConformal.cayley

19. lemma OAI.MahlerConformal.hasDerivAt_log_cayley line 131
20. theorem OAI.MahlerConformal.two_H_eq_log line 143

    Source documentation

    Auxiliary logarithm identity, established without assuming a logarithmic series.

    theorem two_H_eq_log {w : ℂ} (hw : ‖w‖ < 1) :
        2 * H w = Complex.log (cayley w) := by
    …

    Mentions: OAI.MahlerConformal.H, OAI.MahlerConformal.cayley

21. def OAI.MahlerConformal.D line 160
22. lemma OAI.MahlerConformal.w_mul_D line 162
23. lemma OAI.MahlerConformal.D_zero line 170
24. lemma OAI.MahlerConformal.pi_cast_ne line 178
25. theorem OAI.MahlerConformal.hasDerivAt_F_series line 182

    Source documentation

    Termwise differentiation of the conformal series.

    theorem hasDerivAt_F_series {w : ℂ} (hw : ‖w‖ < 1) :
        HasDerivAt F ((8/(Real.pi : ℂ)^2) * D w) w :=
    …

    Mentions: OAI.MahlerConformal.F, OAI.MahlerConformal.D

26. theorem OAI.MahlerConformal.differentiableOn_F line 187

    Source documentation

    Holomorphicity on the open unit disk.

    theorem differentiableOn_F : DifferentiableOn ℂ F (ball 0 1) := by
    …

    Mentions: OAI.MahlerConformal.F

27. theorem OAI.MahlerConformal.F_zero line 191
28. theorem OAI.MahlerConformal.hasDerivAt_F_zero line 194

    Source documentation

    The removable value of the derivative at zero.

    theorem hasDerivAt_F_zero : HasDerivAt F (8/(Real.pi : ℂ)^2) 0 := by
    …

    Mentions: OAI.MahlerConformal.F

29. theorem OAI.MahlerConformal.hasDerivAt_F_log line 198

    Source documentation

    The derivative formula away from zero, with the principal logarithm.

    theorem hasDerivAt_F_log {w : ℂ} (hw : ‖w‖ < 1) (hw0 : w ≠ 0) :
        HasDerivAt F (4/((Real.pi : ℂ)^2*w) * Complex.log ((1+w)/(1-w))) w := by
    …

    Mentions: OAI.MahlerConformal.F

30. lemma OAI.MahlerConformal.log_cayley_ne_zero line 207
31. theorem OAI.MahlerConformal.deriv_F_ne_zero line 217

    Source documentation

    Nonvanishing of the derivative.

    theorem deriv_F_ne_zero {w : ℂ} (hw : ‖w‖ < 1) : deriv F w ≠ 0 := by
    …

    Mentions: OAI.MahlerConformal.F

32. theorem OAI.MahlerConformal.hasSum_F line 228

    Source documentation

    Convergence to the normalized conformal series.

    theorem hasSum_F {w : ℂ} (hw : ‖w‖ < 1) :
        HasSum (fun k : ℕ => (8/(Real.pi : ℂ)^2) *
          (w^(2*k+1) / ((2*k+1 : ℕ) : ℂ)^2)) (F w) :=
    …

    Mentions: OAI.MahlerConformal.F

33. theorem OAI.MahlerConformal.F_odd line 234

    Source documentation

    Oddness of the conformal map.

    theorem F_odd (w : ℂ) : F (-w) = -F w := by
    …

    Mentions: OAI.MahlerConformal.F

34. theorem OAI.MahlerConformal.F_conj line 241

    Source documentation

    Conjugation symmetry of the conformal map.

    theorem F_conj (w : ℂ) : F (starRingEnd ℂ w) = starRingEnd ℂ (F w) := by
    …

    Mentions: OAI.MahlerConformal.F

35. theorem OAI.MahlerConformal.log_formula_limit_zero line 246

    Source documentation

    The logarithmic derivative formula has a removable limit at zero.

    theorem log_formula_limit_zero :
        Filter.Tendsto (fun w : ℂ =>
          4/((Real.pi : ℂ)^2*w) * Complex.log ((1+w)/(1-w)))
          (𝓝[≠] 0) (𝓝 (8/(Real.pi : ℂ)^2)) := by
    …

36. theorem OAI.MahlerConformal.conformal_series_main line 267

    Source documentation

    The conformal series, its derivative including zero, nonvanishing, and the logarithm branch domain.

    theorem conformal_series_main (w : ℂ) (hw : ‖w‖ < 1) :
        HasSum (fun k : ℕ => (8/(Real.pi : ℂ)^2) *
          (w^(2*k+1) / ((2*k+1 : ℕ) : ℂ)^2)) (F w) ∧
        HasDerivAt F (if w = 0 then 8/(Real.pi : ℂ)^2
          else 4/((Real.pi : ℂ)^2*w) * Complex.log ((1+w)/(1-w))) w ∧
        deriv F w ≠ 0 ∧ 0 < ((1+w)/(1-w)).re := by
    …

    Mentions: OAI.MahlerConformal.F