OAI/Probability/SLEGauge/PostStopPotential.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LoewnerRestart.lintegral_finite_stop_guard line 18
  2. theorem OAI.SLEExactGauge.LoewnerRestart.recoveredPostStop_potential line 32
  3. theorem OAI.SLEExactGauge.LoewnerRestart.recoveredRestart_potential line 98
  4. lemma OAI.SLEExactGauge.MassVersions.measure_eq_of_determiningTests line 139
  5. theorem OAI.SLEExactGauge.MassVersions.ae_all_measure_eq_of_test_eq line 175
  6. def OAI.SLEExactGauge.MassVersions.positiveTest line 185
  7. lemma OAI.SLEExactGauge.MassVersions.positiveTest_nonneg line 191
  8. lemma OAI.SLEExactGauge.MassVersions.positiveTest_sub line 198
  9. lemma OAI.SLEExactGauge.MassVersions.integral_positiveTest_sub line 205
  10. def OAI.SLEExactGauge.MeshEnergy.grid line 226
  11. lemma OAI.SLEExactGauge.MeshEnergy.grid_zero line 228
  12. lemma OAI.SLEExactGauge.MeshEnergy.grid_last line 230
  13. lemma OAI.SLEExactGauge.MeshEnergy.grid_mono line 234
  14. lemma OAI.SLEExactGauge.MeshEnergy.grid_mem line 239
  15. lemma OAI.SLEExactGauge.MeshEnergy.dist_grid_succ line 242
  16. lemma OAI.SLEExactGauge.MeshEnergy.tendsto_mesh line 250
  17. def OAI.SLEExactGauge.MeshEnergy.energy line 257
  18. lemma OAI.SLEExactGauge.MeshEnergy.energy_nonneg line 260
  19. lemma OAI.SLEExactGauge.MeshEnergy.energy_le line 264
  20. theorem OAI.SLEExactGauge.MeshEnergy.tendsto_energy_zero line 288
  21. lemma OAI.SLEExactGauge.TaylorVariation.remainder_le_sq line 347
  22. lemma OAI.SLEExactGauge.TaylorVariation.lipschitz_of_deriv_bound line 364
  23. lemma OAI.SLEExactGauge.TaylorVariation.remainder_le_abs line 372
  24. def OAI.SLEExactGauge.TaylorVariation.error line 384
  25. lemma OAI.SLEExactGauge.TaylorVariation.error_eq_sum line 388
  26. lemma OAI.SLEExactGauge.TaylorVariation.abs_error_le_energy line 395
  27. lemma OAI.SLEExactGauge.TaylorVariation.abs_error_le_variation line 407
  28. lemma OAI.SLEExactGauge.TaylorVariation.tendsto_error_zero line 426
  29. def OAI.SLEExactGauge.TaylorVariation.detector line 438
  30. def OAI.SLEExactGauge.TaylorVariation.detectorDeriv line 440
  31. lemma OAI.SLEExactGauge.TaylorVariation.one_le_root line 442
  32. lemma OAI.SLEExactGauge.TaylorVariation.hasDerivAt_root line 445
  33. lemma OAI.SLEExactGauge.TaylorVariation.hasDerivAt_detector line 452
  34. lemma OAI.SLEExactGauge.TaylorVariation.hasDerivAt_detectorDeriv line 455
  35. lemma OAI.SLEExactGauge.TaylorVariation.abs_detectorDeriv_le line 467
  36. lemma OAI.SLEExactGauge.TaylorVariation.lipschitz_detector line 473
  37. lemma OAI.SLEExactGauge.TaylorVariation.lipschitz_detectorDeriv line 476
  38. lemma OAI.SLEExactGauge.TaylorVariation.detector_zero line 484
  39. lemma OAI.SLEExactGauge.TaylorVariation.detector_nonneg line 486
  40. lemma OAI.SLEExactGauge.TaylorVariation.detector_eq_zero_iff line 488
  41. lemma OAI.SLEExactGauge.TaylorVariation.abs_detector_le line 498