OAI/Probability/SLE/Geometry/BoundedTerminalMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The canonical mass has finite expected mass on bounded physical sets, including sets that approach the real boundary. Compactness inside the half-plane is not needed for the upper-cover charge.

  1. lemma OAI.SLEExactGauge.Multipoint.initialGreenMeasure_bounded_ball_lt_top line 15
  2. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.terminal_bounded_mean_lt_top line 44