OAI/Probability/SLE/Mass/WeightedCompactMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded compact weights preserve the scalar continuity estimates used for the canonical disk mass.

  1. lemma OAI.SLEExactGauge.integral_weight_difference_le line 15
  2. lemma OAI.SLEExactGauge.Multipoint.compact_weight_bounded line 43
  3. lemma OAI.SLEExactGauge.Multipoint.compact_weight_integrable line 49
  4. lemma OAI.SLEExactGauge.Multipoint.compact_weight_difference_le line 55
  5. theorem OAI.SLEExactGauge.Multipoint.ContinuousMassPath.weighted_compact_continuous line 74