OAI/Probability/SLE/Angle/TargetLevelMeasurability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joint angle, level and driver measurability of the exact rational level stop and its prescribed change-of-law density.

  1. lemma OAI.SLEExactGauge.Target.levelTime_eq_iInf line 14
  2. lemma OAI.SLEExactGauge.Target.measurable_levelTime_joint line 28
  3. lemma OAI.SLEExactGauge.Target.measurable_levelTime_angle line 63
  4. lemma OAI.SLEExactGauge.Target.measurable_levelDensity_joint line 70
  5. lemma OAI.SLEExactGauge.Target.measurable_levelDensity_angle line 96