OAI/Probability/SLE/Mass/MassCompensatorEndpoint.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The last full dyadic cell before a finite or infinite time.

  1. lemma OAI.SLEExactGauge.compensatorMeshTime_eq_div line 13
  2. lemma OAI.SLEExactGauge.compensatorMeshTime_end line 17
  3. def OAI.SLEExactGauge.compensatorFiniteIndex line 23
  4. lemma OAI.SLEExactGauge.compensatorFiniteIndex_le line 26
  5. lemma OAI.SLEExactGauge.compensator_cell_before_iff line 29
  6. lemma OAI.SLEExactGauge.compensator_before_sum line 35
  7. lemma OAI.SLEExactGauge.compensatorFiniteIndex_eq_floor line 45
  8. lemma OAI.SLEExactGauge.compensatorEndpoint_le line 52
  9. lemma OAI.SLEExactGauge.compensatorEndpoint_lower line 57
  10. theorem OAI.SLEExactGauge.compensatorEndpoint_tendsto line 65

    Source documentation

    A finite endpoint is approached from below even though the grid horizon grows.

    theorem compensatorEndpoint_tendsto (t : ℝ≥0) :
    Tendsto (fun n => compensatorMeshTime n (compensatorFiniteIndex n t)) atTop (𝓝 t) := by
…

    Mentions: OAI.SLEExactGauge.compensatorMeshTime, OAI.SLEExactGauge.compensatorFiniteIndex

  11. def OAI.SLEExactGauge.compensatorStopIndex line 83
  12. lemma OAI.SLEExactGauge.compensatorStopIndex_measurable line 86
  13. lemma OAI.SLEExactGauge.compensatorStopIndex_le line 92
  14. def OAI.SLEExactGauge.massAtExtendedTime line 99
  15. theorem OAI.SLEExactGauge.massAt_compensatorEndpoint_tendsto line 102