OAI/Probability/SLE/Mass/HalfPlaneHerglotzMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Schwarz–Pick bound for a half-plane map vanishing at infinity. Only the total mass coefficient is used; no representation theorem is assumed.

  1. lemma OAI.SLEExactGauge.halfPlane_schwarz_pick_vanishing_scaled line 13
  2. theorem OAI.SLEExactGauge.halfPlane_vanishing_mass_bound line 31
  3. lemma OAI.SLEExactGauge.norm_le_mass_div_height line 52