OAI/Probability/SLE/Loewner/UnivalentKoebeTransform.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact second-derivative calculation for disk recentering. A bound on the second coefficient of normalized univalent functions therefore controls their logarithmic derivative throughout the disk.

  1. lemma OAI.SLEExactGauge.diskRecenter_second_deriv_zero line 15
  2. lemma OAI.SLEExactGauge.deriv_comp_diskRecenter_zero line 30
  3. lemma OAI.SLEExactGauge.second_deriv_comp_diskRecenter_zero line 38
  4. lemma OAI.SLEExactGauge.univalent_preSchwarzian_of_second_derivative line 62