OAI/Probability/SLE/Mass/LocalGridMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A translated finite grid count for arbitrary sets of bounded diameter. No regularity of the set being covered is required.

  1. lemma OAI.SLEExactGauge.localGrid_coordinate line 14
  2. def OAI.SLEExactGauge.localGridIndex line 36
  3. lemma OAI.SLEExactGauge.localGrid_covers line 41
  4. lemma OAI.SLEExactGauge.localGrid_card_bound line 51
  5. lemma OAI.SLEExactGauge.localGrid_mass_bound line 92