OAI/Analysis/Mahler/ConformalInjectivity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MahlerConformal.norm_add_sub_sq line 10
  2. lemma OAI.MahlerConformal.re_mul_log_cayley_pos line 16
  3. lemma OAI.MahlerConformal.re_mul_log_cayley_nonneg line 28
  4. lemma OAI.MahlerConformal.im_mul_arg_cayley_pos line 34
  5. lemma OAI.MahlerConformal.im_mul_arg_cayley_nonneg line 43
  6. theorem OAI.MahlerConformal.deriv_F_re_pos line 51

    Source documentation

    A consequence of the derivative formula on the full disk, used for injectivity. This is not a formula for M'(r), nor does it assume univalence.

    theorem deriv_F_re_pos {w : ℂ} (hw : ‖w‖ < 1) : 0 < (deriv F w).re := by
…

    Mentions: OAI.MahlerConformal.F

  7. lemma OAI.MahlerConformal.segment_mem_disk line 80
  8. theorem OAI.MahlerConformal.F_injOn_disk line 92

    Source documentation

    Injectivity on the exact open unit disk, with no assumed inverse or central univalence theorem. Positive real derivative makes the segment projection strict.

    theorem F_injOn_disk : Set.InjOn F (ball (0 : ℂ) 1) := by
…

    Mentions: OAI.MahlerConformal.F