OAI/Probability/SLE/Loewner/InverseBoundaryShrink.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Small closed image semicircles force the images of their entire half-disks to be small. The Loewner height inequality supplies the exterior endpoint of each radial crossing.

  1. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_im_ge line 15
  2. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.inverse_arc_traps_radial_point line 23
  3. lemma OAI.SLEExactGauge.polar_representation_upperHalfPlane line 60
  4. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.small_boundary_halfdisk line 79