OAI/Probability/SLEGauge/PlanarGrid.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.PlanarGrid.cell line 18
  2. lemma OAI.SLEExactGauge.PlanarGrid.cell_measurable line 22
  3. lemma OAI.SLEExactGauge.PlanarGrid.mem_floor_cell line 27
  4. def OAI.SLEExactGauge.PlanarGrid.nearby line 36
  5. lemma OAI.SLEExactGauge.PlanarGrid.floor_interval_card line 40
  6. lemma OAI.SLEExactGauge.PlanarGrid.nearby_card line 53
  7. lemma OAI.SLEExactGauge.PlanarGrid.subset_nearby line 71
  8. theorem OAI.SLEExactGauge.PlanarGrid.outerMass_le line 92
  9. lemma OAI.SLEExactGauge.PlanarGrid.cell_closed line 124
  10. lemma OAI.SLEExactGauge.PlanarGrid.cell_dist line 130
  11. lemma OAI.SLEExactGauge.PlanarGrid.index_mem_pair line 138
  12. def OAI.SLEExactGauge.PlanarGrid.containingIndices line 151
  13. lemma OAI.SLEExactGauge.PlanarGrid.mem_containingIndices line 154
  14. lemma OAI.SLEExactGauge.PlanarGrid.containingIndices_card line 159
  15. lemma OAI.SLEExactGauge.PlanarGrid.tsum_cell_mass line 165
  16. def OAI.SLEExactGauge.PlanarGrid.maximalMass line 206
  17. lemma OAI.SLEExactGauge.PlanarGrid.maximalMass_nonempty line 209
  18. lemma OAI.SLEExactGauge.PlanarGrid.maximalMass_bdd line 213
  19. lemma OAI.SLEExactGauge.PlanarGrid.maximalMass_bounds line 219
  20. lemma OAI.SLEExactGauge.PlanarGrid.mass_le_maximalMass line 227
  21. lemma OAI.SLEExactGauge.PlanarGrid.maximalMass_grid line 232
  22. theorem OAI.SLEExactGauge.PlanarGrid.full_density line 243
  23. theorem OAI.SLEExactGauge.PlanarGrid.hausdorff_pos_of_grid line 274
  24. def OAI.SLEExactGauge.PlanarGrid.badRegion line 299
  25. lemma OAI.SLEExactGauge.PlanarGrid.badRegion_measurable line 302
  26. def OAI.SLEExactGauge.PlanarGrid.retained line 306
  27. lemma OAI.SLEExactGauge.PlanarGrid.retained_measurable line 309
  28. lemma OAI.SLEExactGauge.PlanarGrid.exists_positive_retained line 316
  29. lemma OAI.SLEExactGauge.PlanarGrid.retained_cell_bound line 334
  30. theorem OAI.SLEExactGauge.PlanarGrid.hausdorff_pos_of_finitely_bad line 350
  31. theorem OAI.SLEExactGauge.PlanarGrid.ae_ae_finite_bad line 368
  32. def OAI.SLEExactGauge.PlanarGrid.testedBadCell line 393
  33. lemma OAI.SLEExactGauge.PlanarGrid.testedBadCell_mass line 399
  34. theorem OAI.SLEExactGauge.PlanarGrid.ae_finitely_bad_of_spatial_tails line 412