OAI/Probability/SLEGauge/SurvivalLocalization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.localizationStop_after_survival line 38
  2. lemma OAI.ExactSLEGreen.localizationRemaining_tendsto line 66
  3. theorem OAI.ExactSLEGreen.joint_radialRemaining_measurable line 97
  4. lemma OAI.ExactSLEGreen.radialRemaining_driver_congr line 157
  5. theorem OAI.ExactSLEGreen.radialRemaining_raw_joint line 175
  6. def OAI.ExactSLEGreen.remainingMassDensity line 208
  7. lemma OAI.ExactSLEGreen.remainingMassDensity_measurable line 215
  8. lemma OAI.ExactSLEGreen.remainingMassDensity_local_bound line 225
  9. lemma OAI.ExactSLEGreen.remainingMassEval_joint_integrable line 243
  10. lemma OAI.ExactSLEGreen.finite_density_conditional line 269
  11. theorem OAI.ExactSLEGreen.actual_finite_conditional_mass line 302
  12. def OAI.ExactSLEGreen.survivingGreen line 344
  13. lemma OAI.ExactSLEGreen.physicalRadius_actual_pos line 350
  14. lemma OAI.ExactSLEGreen.physicalRadius_actual_anti line 356
  15. lemma OAI.ExactSLEGreen.survivingGreen_nonneg line 369
  16. lemma OAI.ExactSLEGreen.remainingMassDensity_nonneg line 373
  17. lemma OAI.ExactSLEGreen.remaining_to_surviving line 377
  18. lemma OAI.ExactSLEGreen.remainingMassDensity_mean_bound line 406