OAI/Probability/SLE/Geometry/HalfPlaneBoundaryDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite continuous boundary value makes the inverse derivative small after multiplication by the height.

  1. lemma OAI.SLEExactGauge.vertical_approach_halfPlane line 14
  2. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_tip_limit line 24
  3. theorem OAI.SLEExactGauge.halfPlane_boundary_derivative_vanishes line 33
  4. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_tip_derivative_vanishes line 78