OAI/Probability/SLEGauge/CandidateCover.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.CandidateCover.closedBall_subset_triple_of_inter line 18
  2. theorem OAI.SLEExactGauge.CandidateCover.finite_disjoint_triples line 30
  3. lemma OAI.SLEExactGauge.CandidateCover.ediam_closedBall_le_of_nonneg line 69
  4. lemma OAI.SLEExactGauge.CandidateCover.diameterCost_le_radius line 77
  5. lemma OAI.SLEExactGauge.CandidateCover.disjoint_charge line 86
  6. theorem OAI.SLEExactGauge.CandidateCover.finite_candidate_charge line 100
  7. lemma OAI.SLEExactGauge.CandidateCover.quadratic_multiple_le line 118
  8. lemma OAI.SLEExactGauge.CandidateCover.quadratic_candidate_cost line 131
  9. theorem OAI.SLEExactGauge.CandidateCover.finite_quadratic_candidates line 155
  10. lemma OAI.SLEExactGauge.BoundaryGreen.height_power_lintegral line 190
  11. def OAI.SLEExactGauge.BoundaryGreen.rectangle line 204
  12. lemma OAI.SLEExactGauge.BoundaryGreen.rectangle_measurable line 207
  13. lemma OAI.SLEExactGauge.BoundaryGreen.image_rectangle line 211
  14. lemma OAI.SLEExactGauge.BoundaryGreen.rectangle_height_integral line 221
  15. lemma OAI.SLEExactGauge.BoundaryGreen.initialGreen_height_bound line 244
  16. theorem OAI.SLEExactGauge.BoundaryGreen.initialGreen_rectangle_bound line 257
  17. lemma OAI.SLEExactGauge.BoundaryGreen.initialGreen_rectangle_finite line 280
  18. theorem OAI.SLEExactGauge.BoundaryGreen.canonical_rectangle_mean line 290
  19. def OAI.SLEExactGauge.BoxGrid.box line 317
  20. def OAI.SLEExactGauge.BoxGrid.region line 319
  21. lemma OAI.SLEExactGauge.BoxGrid.region_measurable line 321
  22. lemma OAI.SLEExactGauge.BoxGrid.preimage_region line 325
  23. def OAI.SLEExactGauge.BoxGrid.columns line 329
  24. def OAI.SLEExactGauge.BoxGrid.rows line 331
  25. abbrev OAI.SLEExactGauge.BoxGrid.Cells line 333
  26. def OAI.SLEExactGauge.BoxGrid.center line 335
  27. lemma OAI.SLEExactGauge.BoxGrid.center_im_pos line 338
  28. lemma OAI.SLEExactGauge.BoxGrid.columns_width line 342
  29. lemma OAI.SLEExactGauge.BoxGrid.rows_height line 349
  30. lemma OAI.SLEExactGauge.BoxGrid.center_bounds line 356
  31. lemma OAI.SLEExactGauge.BoxGrid.covered line 368
  32. lemma OAI.SLEExactGauge.BoxGrid.ball_subset_region line 395
  33. def OAI.SLEExactGauge.BoundaryRows.rowConstant line 421
  34. lemma OAI.SLEExactGauge.BoundaryRows.rowConstant_pos line 423
  35. theorem OAI.SLEExactGauge.BoundaryRows.half_integer_sum line 429
  36. lemma OAI.SLEExactGauge.BoundaryRows.scaled_half_integer_sum line 465
  37. theorem OAI.SLEExactGauge.BoundaryRows.rows_below_height line 485
  38. theorem OAI.SLEExactGauge.BoundaryRows.truncated_rows line 494
  39. theorem OAI.SLEExactGauge.BoundaryRows.rectangle_rows line 515
  40. theorem OAI.SLEExactGauge.BoundaryRows.rectangle_truncated_rows line 531