OAI/Probability/SLE/Gauge/RandomBadGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Measurability and almost-sure finiteness of the bad-grid mass sum. Only expectations of the actual cell masses occur in the criterion.

  1. lemma OAI.SLEExactGauge.measurableSet_random_badGridCells line 14
  2. lemma OAI.SLEExactGauge.random_badGrid_mass_measurable line 44
  3. lemma OAI.SLEExactGauge.badGrid_mass_le_sum line 52
  4. lemma OAI.SLEExactGauge.expected_badGrid_mass_le_sum line 65
  5. lemma OAI.SLEExactGauge.ae_prescribedBadGrid_sum_finite line 84
  6. lemma OAI.SLEExactGauge.ae_positive_prescribed_hausdorff_of_bad_mass line 100