OAI/Probability/SLEGauge/ModelCandidates.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidateScale line 22
  2. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidateLower line 25
  3. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidateScale_one line 27
  4. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidateScale_pos line 28
  5. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidateLower_pos line 29
  6. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.spatialMass line 34
  7. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.spatialMass_apply line 36
  8. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.spatialMass_measurable line 40
  9. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidate line 45
  10. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.candidate_measurable line 49
  11. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.success_implies_candidate line 54
  12. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.batch_candidates line 100
  13. lemma OAI.SLEExactGauge.LoewnerGeometry.diskAt_norm_le_one line 126
  14. theorem OAI.SLEExactGauge.LoewnerGeometry.halfPlane_harnack_ball line 136
  15. theorem OAI.SLEExactGauge.LoewnerGeometry.alive_of_height_floor line 190
  16. lemma OAI.SLEExactGauge.LoewnerGeometry.loewnerMap_height_antitone line 242
  17. theorem OAI.SLEExactGauge.LoewnerGeometry.center_alive_of_ball_survival line 266
  18. theorem OAI.SLEExactGauge.LoewnerGeometry.frontier_avoids_ball_of_no_crossing line 298
  19. theorem OAI.SLEExactGauge.LoewnerGeometry.radial_crossing_of_frontier_visit line 330
  20. theorem OAI.SLEExactGauge.LoewnerGeometry.trace_visit_probability_large line 339
  21. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.alpha_lt_one line 384
  22. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupEvent line 390
  23. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finalRadius_height line 397
  24. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupEvent_measurable line 403
  25. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cellConstant line 415
  26. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cellConstant_pos line 417
  27. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cell_factor line 420
  28. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanup_near line 429
  29. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanup_far line 453
  30. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanup_covers line 472
  31. lemma OAI.SLEExactGauge.CoverCost.hausdorff_le_liminf_bound line 511
  32. lemma OAI.SLEExactGauge.CoverCost.hausdorff_le_liminf_of_exists line 522
  33. theorem OAI.SLEExactGauge.CoverCost.liminf_cost_bound line 542
  34. theorem OAI.SLEExactGauge.CoverCost.ae_hausdorff_finite_of_covers line 555