OAI/Probability/SLEGauge/StoppedFiniteMass.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. lemma OAI.ExactSLEGreen.timeMassDensity_stopping_joint_measurable line 19
  2. def OAI.ExactSLEGreen.stoppedMassKernel line 30
  3. instance OAI.ExactSLEGreen.stoppedMassKernel_sfinite line 35
  4. lemma OAI.ExactSLEGreen.stoppedMassKernel_apply line 39
  5. lemma OAI.ExactSLEGreen.actualUpperMass_measurable_stopping line 45
  6. lemma OAI.ExactSLEGreen.actualUpperMass_add_unhit line 55
  7. theorem OAI.ExactSLEGreen.actualUpperMass_stopped_random_test line 72
  8. lemma OAI.ExactSLEGreen.remainingMassDensity_antitone_level line 114
  9. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_antitone_level line 129
  10. lemma OAI.ExactSLEGreen.remainingMassDensity_eventually_eq_surviving line 138
  11. lemma OAI.ExactSLEGreen.stoppedRemainingDensity_eventually_eq_surviving line 165
  12. theorem OAI.ExactSLEGreen.stoppedRemainingDensity_random_test_tendsto line 177
  13. theorem OAI.ExactSLEGreen.actual_stopped_remaining_spatial_L1 line 228
  14. lemma OAI.ExactSLEGreen.actualUpper_stopped_remaining_integral_tendsto line 289
  15. lemma OAI.ExactSLEGreen.actualUpperMass_stopped_norm_bound line 355
  16. theorem OAI.ExactSLEGreen.actualUpperMass_stopped_Lp_bound line 367
  17. lemma OAI.ExactSLEGreen.actualUpperMass_stopped_eval_integrable line 389
  18. lemma OAI.ExactSLEGreen.stoppedRemainingKernel_compact_eval line 399
  19. theorem OAI.ExactSLEGreen.actualUpperMass_stopped_finite_kernel line 414
  20. theorem OAI.ExactSLEGreen.actualUpperMass_stopped_convex_potential_limit line 446