OAI/Probability/SLE/Mass/LevelApproximants.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-level random measures used to construct canonical trace mass. Time truncation retains precisely levels already attained.

  1. lemma OAI.SLEExactGauge.Multipoint.actual_radiusLevel_joint_measurable line 17
  2. def OAI.SLEExactGauge.Multipoint.levelApproximationDensity line 33
  3. def OAI.SLEExactGauge.Multipoint.levelApproximation line 40
  4. lemma OAI.SLEExactGauge.Multipoint.levelApproximationDensity_joint_measurable line 45
  5. lemma OAI.SLEExactGauge.Multipoint.levelApproximationDensity_mono line 57
  6. lemma OAI.SLEExactGauge.Multipoint.levelApproximation_mono line 70
  7. lemma OAI.SLEExactGauge.Multipoint.levelApproximation_apply_top line 78
  8. lemma OAI.SLEExactGauge.Multipoint.levelApproximation_apply_le line 86
  9. lemma OAI.SLEExactGauge.Multipoint.levelApproximation_measurable_apply line 94