OAI/Probability/SLE/Mass/CanonicalPhysicalMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The upper cover is charged to the canonical terminal measure on the physical plane. Its mean is the initial Green measure, also on sets meeting the real boundary.

  1. def OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.physicalTerminal line 18
  2. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.physicalTerminal_measurable line 21
  3. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.physicalTerminal_apply line 25
  4. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.physicalTerminal_mean line 30
  5. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.physicalTerminal_bounded_mean_lt_top line 42