OAI/Probability/SLEGauge/FutureSupport.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.SLEExactGauge.MassVersions.random_set_sub_null_of_compact_means line 22
  2. lemma OAI.ExactSLEGreen.survivingGreen_eq_zero_iff line 66
  3. lemma OAI.ExactSLEGreen.deadSet_raw_measurable line 74
  4. theorem OAI.ExactSLEGreen.conditional_future_support line 84
  5. lemma OAI.ExactSLEGreen.radialTime_ne_zero line 140
  6. lemma OAI.ExactSLEGreen.actualUpperMass_zero line 150
  7. lemma OAI.ExactSLEGreen.level_step_lt_one line 157
  8. theorem OAI.ExactSLEGreen.recoveredMass_zero line 166
  9. theorem OAI.SLEExactGauge.MassVersions.compact_mass_memLp line 191
  10. def OAI.ExactSLEGreen.initialGreen line 220
  11. lemma OAI.ExactSLEGreen.initialGreen_pos line 223
  12. lemma OAI.ExactSLEGreen.initialGreen_continuous line 226
  13. def OAI.ExactSLEGreen.initialGreenMeasure line 236
  14. lemma OAI.ExactSLEGreen.initialGreenMeasure_compact_integrable line 239
  15. instance OAI.ExactSLEGreen.initialGreenMeasure_finite line 249
  16. lemma OAI.ExactSLEGreen.initialGreenMeasure_compact_eval line 252
  17. theorem OAI.ExactSLEGreen.initialGreenMeasure_eq_average line 261
  18. theorem OAI.ExactSLEGreen.terminal_null_of_area_null line 274
  19. lemma OAI.ExactSLEGreen.remainingMassDensity_mean_antitone line 297
  20. lemma OAI.ExactSLEGreen.survivingGreen_mean_antitone line 339
  21. lemma OAI.ExactSLEGreen.survivingGreen_eq_killed line 366
  22. lemma OAI.ExactSLEGreen.physicalGreen_measurable line 373
  23. lemma OAI.ExactSLEGreen.killedGreen_nonneg line 377
  24. lemma OAI.ExactSLEGreen.killedGreen_integrable line 381
  25. lemma OAI.ExactSLEGreen.killedGreen_mean_antitone line 389
  26. lemma OAI.ExactSLEGreen.killedGreen_lintegral_antitone line 399