OAI/Probability/SLEGauge/CleanupCost.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.CleanupCost.nat_mul_exp_neg_linear line 19
  2. lemma OAI.SLEExactGauge.CleanupCost.nat_mul_exp_neg_two_pow line 29
  3. lemma OAI.SLEExactGauge.CleanupCost.nat_mul_boundary_power line 39
  4. def OAI.SLEExactGauge.CleanupCost.envelope line 65
  5. lemma OAI.SLEExactGauge.CleanupCost.envelope_tendsto line 68
  6. lemma OAI.SLEExactGauge.CleanupCost.envelope_uniform_bound line 76
  7. lemma OAI.SLEExactGauge.CleanupCost.two_region_cell_sum line 85
  8. theorem OAI.SLEExactGauge.CleanupCost.cleanup_sum line 126
  9. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupCost line 166
  10. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupCost_measurable line 171
  11. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupCost_integral line 177
  12. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupCost_integral_bound line 204
  13. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanupCost_uniform_bound line 238
  14. def OAI.SLEExactGauge.CenteredMoments.allFrontiers line 289
  15. lemma OAI.SLEExactGauge.CenteredMoments.exp_neg_nat_sq_tendsto line 292
  16. abbrev OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.GridCells line 301
  17. abbrev OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.CandidateIndices line 302
  18. abbrev OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.CoverIndices line 303
  19. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gridCenter line 305
  20. def OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.costBound line 308
  21. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.costBound_measurable line 312
  22. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.costBound_uniform line 316
  23. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finalRadius_le_one line 335
  24. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.gauge_admissible_actual line 338
  25. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.cleanup_ball_cost line 341
  26. lemma OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.finite_cover line 359
  27. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.frontier_box_finite line 482
  28. theorem OAI.SLEExactGauge.CenteredMoments.CenteredMomentModel.frontier_boxes_finite line 518
  29. def OAI.SLEExactGauge.CenteredMoments.dimension line 540
  30. lemma OAI.SLEExactGauge.CenteredMoments.parameterDimension_pos line 542
  31. lemma OAI.SLEExactGauge.CenteredMoments.dimension_lt_two line 546
  32. theorem OAI.SLEExactGauge.CenteredMoments.exists_parameter_moment_gauge line 552
  33. def OAI.SLEExactGauge.CenteredMoments.parameterMomentGauge line 577
  34. lemma OAI.SLEExactGauge.CenteredMoments.parameterMomentGauge_admissible line 580
  35. lemma OAI.SLEExactGauge.CenteredMoments.parameterMomentGauge_doubling line 584
  36. lemma OAI.SLEExactGauge.CenteredMoments.parameterMomentGauge_model line 589