OAI/Probability/SLEGauge/NormalizedRadialTests.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LoewnerRestart.radialLaw_normalize_integral line 18
  2. def OAI.SLEExactGauge.LoewnerRestart.finiteTestKernel line 40
  3. lemma OAI.SLEExactGauge.LoewnerRestart.finiteTestKernel_eq line 44
  4. lemma OAI.SLEExactGauge.LoewnerRestart.finiteTestKernel_measurable line 61
  5. lemma OAI.SLEExactGauge.LoewnerRestart.finiteTestKernel_mixed line 67
  6. lemma OAI.SLEExactGauge.LoewnerRestart.pointAngle_radialPoint line 72
  7. def OAI.SLEExactGauge.LoewnerRestart.normalizedTest line 82
  8. lemma OAI.SLEExactGauge.LoewnerRestart.normalizedTest_measurable line 87
  9. theorem OAI.SLEExactGauge.LoewnerRestart.normalizedTest_conditional line 97
  10. theorem OAI.SLEExactGauge.LoewnerRestart.normalizedTest_conditional_bounds line 132
  11. lemma OAI.SLEExactGauge.CenteredMoments.centered_radius_le line 176
  12. lemma OAI.SLEExactGauge.CenteredMoments.centered_radius_pos line 184
  13. lemma OAI.SLEExactGauge.CenteredMoments.centered_radius_strict line 188
  14. lemma OAI.SLEExactGauge.CenteredMoments.centeredTime_stopping line 195
  15. lemma OAI.SLEExactGauge.CenteredMoments.centeredTime_monotone line 206
  16. lemma OAI.SLEExactGauge.CenteredMoments.centeredMass_monotone line 217
  17. lemma OAI.SLEExactGauge.CenteredMoments.centeredMass_raw_measurable line 225
  18. lemma OAI.SLEExactGauge.CenteredMoments.centered_laws_lintegral_consistent line 238
  19. lemma OAI.SLEExactGauge.CenteredMoments.finiteAngleLaw_lintegral_consistent line 272
  20. theorem OAI.SLEExactGauge.CenteredMoments.finiteMoment_monotone line 284
  21. lemma OAI.SLEExactGauge.LoewnerRestart.raw_stopped_function_congr line 319
  22. def OAI.SLEExactGauge.LoewnerRestart.finiteStoppedTest line 329
  23. lemma OAI.SLEExactGauge.LoewnerRestart.finiteStoppedTest_raw_measurable line 332
  24. lemma OAI.SLEExactGauge.LoewnerRestart.normalized_levelTime_restart line 340
  25. lemma OAI.SLEExactGauge.LoewnerRestart.normalizedTest_history_congr line 376
  26. lemma OAI.SLEExactGauge.LoewnerRestart.finiteStoppedTest_normalizedTest_eq line 439
  27. def OAI.SLEExactGauge.CompactSequence.initialVector line 466
  28. lemma OAI.SLEExactGauge.CompactSequence.continuous_initialVector line 468
  29. lemma OAI.SLEExactGauge.CompactSequence.measurable_initialVector line 471
  30. theorem OAI.SLEExactGauge.CompactSequence.exists_sequence_law line 476
  31. lemma OAI.SLEExactGauge.CompactSequence.lintegral_initialVector line 511
  32. lemma OAI.SLEExactGauge.CompactSequence.lintegral_coordinate line 520