OAI/Probability/SLEGauge/RadialConditionalMixing.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.SLEExactGauge.LoewnerRestart.radialLaw_consistent_le line 19
  2. theorem OAI.SLEExactGauge.LoewnerRestart.finiteAngle_conditional_integral_bounds line 34
  3. theorem OAI.SLEExactGauge.LoewnerRestart.finiteAngle_conditional_bounds line 75
  4. lemma OAI.SLEExactGauge.LoewnerRestart.radial_change_law_event line 93
  5. theorem OAI.SLEExactGauge.LoewnerRestart.radial_change_law_past_bound line 114
  6. lemma OAI.SLEExactGauge.CenteredMoments.actualUpperMass_eval_joint_measurable line 159
  7. lemma OAI.SLEExactGauge.CenteredMoments.recoveredMass_joint_measurable line 169
  8. lemma OAI.SLEExactGauge.CenteredMoments.centeredTime_measurable line 180
  9. lemma OAI.SLEExactGauge.CenteredMoments.centeredWeight_measurable line 198
  10. lemma OAI.SLEExactGauge.CenteredMoments.diskMap_joint_measurable line 222
  11. lemma OAI.SLEExactGauge.CenteredMoments.diskWeight_joint_measurable line 227
  12. lemma OAI.SLEExactGauge.CenteredMoments.diskMass_joint_measurable line 239
  13. def OAI.SLEExactGauge.CenteredMoments.centeredMass line 269
  14. lemma OAI.SLEExactGauge.CenteredMoments.centeredMass_measurable line 273
  15. def OAI.SLEExactGauge.CenteredMoments.finiteAngleLaw line 300
  16. lemma OAI.SLEExactGauge.CenteredMoments.finiteAngleLaw_absolutelyContinuous line 304
  17. lemma OAI.SLEExactGauge.CenteredMoments.finiteAngleLaw_lintegral line 308
  18. lemma OAI.SLEExactGauge.CenteredMoments.finiteAngleLaw_probability line 329
  19. def OAI.SLEExactGauge.CenteredMoments.finiteMoment line 352
  20. theorem OAI.SLEExactGauge.CenteredMoments.common_limit_mixed_moment_bound line 358
  21. def OAI.SLEExactGauge.LoewnerRestart.pointAngle line 405
  22. lemma OAI.SLEExactGauge.LoewnerRestart.pointAngle_measurable line 407
  23. lemma OAI.SLEExactGauge.LoewnerRestart.point_norm_pos line 410
  24. lemma OAI.SLEExactGauge.LoewnerRestart.fromDisk_pointAngle line 412
  25. lemma OAI.SLEExactGauge.LoewnerRestart.norm_mul_fromDisk_pointAngle line 434
  26. lemma OAI.SLEExactGauge.LoewnerRestart.sin_pointAngle line 439
  27. def OAI.SLEExactGauge.LoewnerRestart.normalizeDriver line 443
  28. lemma OAI.SLEExactGauge.LoewnerRestart.continuous_normalizeDriver line 446
  29. lemma OAI.SLEExactGauge.LoewnerRestart.radiusDensity_scaled line 459
  30. lemma OAI.SLEExactGauge.LoewnerRestart.radialLaw_scale_integral line 474