OAI/Probability/SLE/Geometry/FiniteCellTailKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The upper physical cell comparison gives the reverse test inequality: a large canonical cell mass forces a large normalized finite disk mass.

  1. def OAI.SLEExactGauge.Multipoint.CanonicalMass.finiteCellMassTest line 16
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.finiteCellMassTest_measurable line 24
  3. lemma OAI.SLEExactGauge.Multipoint.cell_ball_live_of_radius line 37
  4. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.finite_cell_mass_disk_tail line 52