OAI/Analysis/Mahler/ConformalInverse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerConformal.Omega line 17
2. def OAI.MahlerConformal.inverseF line 18
3. lemma OAI.MahlerConformal.inverseF_mem line 20
4. lemma OAI.MahlerConformal.inverseF_right line 23
5. lemma OAI.MahlerConformal.inverseF_left line 26
6. lemma OAI.MahlerConformal.hasStrictDerivAt_F line 29
7. theorem OAI.MahlerConformal.isOpen_Omega line 34
8. theorem OAI.MahlerConformal.isConnected_Omega line 43
9. theorem OAI.MahlerConformal.hasDerivAt_inverseF line 50

   Source documentation

   The selected inverse is holomorphic on its exact image domain, with the reciprocal derivative. Its local inverse hypotheses follow from proved injectivity.

   theorem hasDerivAt_inverseF {u : ℂ} (hu : u ∈ Omega) :
       HasDerivAt inverseF (deriv F (inverseF u))⁻¹ u := by
   …

   Mentions: OAI.MahlerConformal.Omega, OAI.MahlerConformal.inverseF, OAI.MahlerConformal.F

10. theorem OAI.MahlerConformal.differentiableOn_inverseF line 61
11. theorem OAI.MahlerConformal.inverseF_deriv_ne_zero line 64
12. theorem OAI.MahlerConformal.Omega_conj line 68
13. theorem OAI.MahlerConformal.inverseF_conj line 73
14. theorem OAI.MahlerConformal.zero_mem_Omega line 78
15. theorem OAI.MahlerConformal.inverseF_zero line 80
16. theorem OAI.MahlerConformal.inverseF_eq_zero_iff line 83
17. theorem OAI.MahlerConformal.conformal_biholomorphism line 92

    Source documentation

    The biholomorphic-map property of F. No vertical fiber property or primitive estimate is hidden in this statement.

    theorem conformal_biholomorphism :
        IsOpen Omega ∧ IsConnected Omega ∧
        Set.BijOn F (ball (0 : ℂ) 1) Omega ∧
        DifferentiableOn ℂ F (ball (0 : ℂ) 1) ∧
        DifferentiableOn ℂ inverseF Omega ∧
        Set.LeftInvOn inverseF F (ball (0 : ℂ) 1) ∧ Set.RightInvOn inverseF F Omega ∧
        F 0 = 0 ∧ deriv F 0 ≠ 0 ∧
        Complex.re '' Omega = Ioo (-1 : ℝ) 1 ∧ Set.MapsTo (starRingEnd ℂ) Omega Omega := by
    …

    Mentions: OAI.MahlerConformal.Omega, OAI.MahlerConformal.F, OAI.MahlerConformal.inverseF