OAI/Probability/SLE/Mass/MassCompensatorRecovery.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.meshMassIncrement line 17
2. def OAI.SLEExactGauge.meshMassCompensator line 20
3. lemma OAI.SLEExactGauge.meshMassIncrement_memLp line 25
4. lemma OAI.SLEExactGauge.meshMassCompensator_decomposition line 43
5. theorem OAI.SLEExactGauge.meshMassCentered_selected_tendstoInMeasure line 57
6. lemma OAI.SLEExactGauge.meshMassCompensator_selected_measurable line 77
7. theorem OAI.SLEExactGauge.meshMassCompensator_selected_tendstoInMeasure line 92

   Source documentation

   Any measurable choice of endpoints where the sampled mass has its pathwise limit recovers that same mass from the predictable increments.

   theorem meshMassCompensator_selected_tendstoInMeasure
       (ℱ : ℕ → Filtration ℕ mΩ) (A : ℝ≥0 → Ω → ℝ) (L V : Ω → ℝ)
       (hA : ∀ t, Measurable (A t))
       (hgrid : ∀ n i, StronglyMeasurable[ℱ n i] (A (compensatorMeshTime n i)))
       (hL : MemLp L 2 P)
       (hp : ∀ᵐ ω ∂P, Monotone (fun t => A t ω) ∧ A 0 ω=0 ∧
         Continuous (fun t => A t ω) ∧ Tendsto (fun t => A t ω) atTop (𝓝 (L ω)) ∧
         ∀ t, A t ω ≤ L ω)
       (J : ℕ → Ω → ℕ) (hJm : ∀ n, Measurable (J n))
       (hJ : ∀ n ω, J n ω ≤ n*2^n)
       (hJV : ∀ᵐ ω ∂P, Tendsto (fun n => A (compensatorMeshTime n (J n ω)) ω)
         atTop (𝓝 (V ω))) :
   …

   Mentions: OAI.SLEExactGauge.compensatorMeshTime

8. theorem OAI.SLEExactGauge.meshMassCompensator_stopped_tendstoInMeasure line 120

   Source documentation

   The exact last-full-cell convention, including an infinite endpoint, recovers the stopped mass in probability.

   theorem meshMassCompensator_stopped_tendstoInMeasure
       (ℱ : ℕ → Filtration ℕ mΩ) (A : ℝ≥0 → Ω → ℝ) (L : Ω → ℝ)
       (hA : ∀ t, Measurable (A t))
       (hgrid : ∀ n i, StronglyMeasurable[ℱ n i] (A (compensatorMeshTime n i)))
       (hL : MemLp L 2 P)
       (hp : ∀ᵐ ω ∂P, Monotone (fun t => A t ω) ∧ A 0 ω=0 ∧
         Continuous (fun t => A t ω) ∧ Tendsto (fun t => A t ω) atTop (𝓝 (L ω)) ∧
         ∀ t, A t ω ≤ L ω)
       (T : Ω → ℝ≥0∞) (hT : Measurable T) :
       TendstoInMeasure P
         (fun n ω => meshMassCompensator P ℱ A n (compensatorStopIndex n (T ω)) ω)
         atTop (fun ω => massAtExtendedTime (fun t => A t ω) (L ω) (T ω)) := by
   …

   Mentions: OAI.SLEExactGauge.compensatorMeshTime, OAI.SLEExactGauge.meshMassCompensator, OAI.SLEExactGauge.compensatorStopIndex, OAI.SLEExactGauge.massAtExtendedTime