OAI/Probability/SLE/Mass/CanonicalMassRandomTime.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Evaluating the common convex sequence at any measurable extended time preserves convergence in mean on every event.

  1. def OAI.SLEExactGauge.Multipoint.extendedCanonicalMass line 18
  2. lemma OAI.SLEExactGauge.Multipoint.extendedCanonicalMass_radon line 22
  3. theorem OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.all_extended_times_limit line 33
  4. theorem OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.random_time_nonnegative_mean_tendsto line 57
  5. lemma OAI.SLEExactGauge.Multipoint.convexLevelMeasure_random_time_test_integrable line 111
  6. theorem OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.random_time_test_mean_tendsto line 137