OAI/Probability/SLE/Mass/CellMassComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At a fixed conformal-radius level the normalized disk mass bounds the mass of a small cell and is bounded by the mass of a larger physical ball.

  1. lemma OAI.SLEExactGauge.Multipoint.ContinuousMassPath.zero_on_surviving line 16
  2. lemma OAI.SLEExactGauge.Multipoint.ContinuousMassPath.zero_on_surviving_subset line 30
  3. lemma OAI.SLEExactGauge.measure_sub_apply_of_zero line 37
  4. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.cell_mass_comparison line 43