OAI/Analysis/Mahler/ConformalRadialRegularity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerConformal.F_chord_re_pos line 12

   Source documentation

   The positive-real derivative yields a strictly positive projection on any chord of the disk.

   theorem F_chord_re_pos {a b : ℂ} (ha : ‖a‖ < 1) (hb : ‖b‖ < 1)
       (hab : a ≠ b) : 0 < ((F b - F a) / (b-a)).re := by
   …

   Mentions: OAI.MahlerConformal.F

2. lemma OAI.MahlerConformal.F_re_mul_re_pos line 37
3. lemma OAI.MahlerConformal.F_im_mul_im_pos line 56
4. lemma OAI.MahlerConformal.F_re_eq_zero_of_re_eq_zero line 74
5. lemma OAI.MahlerConformal.F_im_eq_zero_of_im_eq_zero line 81
6. lemma OAI.MahlerConformal.mul_pos_of_common_factor line 88
7. theorem OAI.MahlerConformal.F_radial_pairing_pos line 96

   Source documentation

   The actual F and its radial derivative have positive Euclidean pairing. This gives radial regularity for its inverse without invoking Sard.

   theorem F_radial_pairing_pos {w : ℂ} (hw : ‖w‖ < 1) (hw0 : w ≠ 0) :
       0 < (F w).re * (w * deriv F w).re + (F w).im * (w * deriv F w).im := by
   …

   Mentions: OAI.MahlerConformal.F