OAI/Probability/SLE/Loewner/UnivalentLocalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A coarse local growth bound from the proved Bloch omitted-value estimate. This bound does not use the sharp disk growth input.

  1. lemma OAI.SLEExactGauge.univalent_inverse_derivative_product line 14
  2. lemma OAI.SLEExactGauge.univalent_coarse_ball_subset_image line 24
  3. lemma OAI.SLEExactGauge.univalent_coarse_local_bound line 36