OAI/Probability/SLE/Mass/PastThresholdMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous mass crosses an intermediate level at a dense test time. Consequently a cell with twice the threshold has at least half its mass strictly after a successful past test.

  1. lemma OAI.SLEExactGauge.Multipoint.dense_time_between_mass_levels line 17
  2. lemma OAI.SLEExactGauge.Multipoint.past_threshold_detects_half line 28