OAI/Probability/SLE/Loewner/UnivalentOddRoot.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized odd square-root transform used in the sharp disk growth argument. The square root is constructed, not assumed.

  1. lemma OAI.SLEExactGauge.hasDerivAt_of_continuous_square_root line 15
  2. lemma OAI.SLEExactGauge.differentiableOn_continuous_square_root line 34
  3. lemma OAI.SLEExactGauge.exists_normalized_analytic_square_root line 44
  4. theorem OAI.SLEExactGauge.univalent_odd_square_root line 65

    Source documentation

    Every normalized disk-univalent map has a normalized odd univalent square-root transform on the same disk.

    theorem univalent_odd_square_root {f : ℂ → ℂ}
    (hf : DifferentiableOn ℂ f (ball 0 1)) (hi : InjOn f (ball 0 1))
    (hf0 : f 0=0) (hd0 : deriv f 0=1) :
    ∃ h : ℂ → ℂ, DifferentiableOn ℂ h (ball 0 1) ∧ InjOn h (ball 0 1) ∧
      h 0=0 ∧ deriv h 0=1 ∧
      (∀ z∈ball (0:ℂ) 1, h z^2=f (z^2)) ∧ (∀ z, h (-z)= -h z) := by
…