OAI/Probability/SLEGauge/GreenIdentities.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff gauges, Loewner evolution and trace measures.

  1. theorem OAI.ExactSLEGreen.actual_surviving_green line 37
  2. lemma OAI.ExactSLEGreen.remainingMassDensity_le_surviving line 100
  3. theorem OAI.ExactSLEGreen.actual_remaining_spatial_L1 line 117
  4. lemma OAI.ExactSLEGreen.actualMassEval_raw_measurable line 183
  5. lemma OAI.ExactSLEGreen.actualUpperMass_eval_raw_measurable line 191
  6. lemma OAI.ExactSLEGreen.raw_ae_measurable_limit line 196
  7. theorem OAI.ExactSLEGreen.actual_radon_raw_evaluations line 205
  8. lemma OAI.ExactSLEGreen.actualUpperMass_finite_kernel line 257
  9. lemma OAI.ExactSLEGreen.actualUpper_remaining_integral_tendsto line 286
  10. lemma OAI.ExactSLEGreen.setIntegral_tendsto_of_L1 line 341
  11. lemma OAI.ExactSLEGreen.scalar_convex_tail_limit line 353
  12. theorem OAI.ExactSLEGreen.actual_radon_compact_conditional line 379