OAI/Probability/SLE/Gauge/RandomPassageBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.measurable_random_finiteBoundaryPath line 26
2. lemma OAI.SLEExactGauge.measurableSet_random_finite_frontMassEvent line 35
3. lemma OAI.SLEExactGauge.restart_condLExp_event_sections line 45
4. theorem OAI.SLEExactGauge.restart_event_lower_bound line 75

   Source documentation

   Uniform section bounds integrate on every event in the stopped past. No countable list of possible pasts and no independence of steps is used.

   theorem restart_event_lower_bound
       {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X]
       (P : Measure Ω) [IsFiniteMeasure P] (ν : Measure X) [IsFiniteMeasure ν]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
       (Y : Ω → X) (hY : Measurable[mΩ] Y)
       (hlaw : ∀ A : Set Ω, MeasurableSet[m] A →
         @Measure.map Ω X mΩ mX Y (P.restrict A) = P A • ν)
       (C : Set (Ω × X)) (hC : @MeasurableSet (Ω × X) (m.prod mX) C)
       (E : Set Ω) (q : ℝ≥0∞)
       (hsections : ∀ᵐ ω ∂P, ω ∈ E → q ≤ ν {x | (ω, x) ∈ C})
       (A : Set Ω) (hA : MeasurableSet[m] A) (hAE : A ⊆ E) :
       q * P A ≤ P (A ∩ {ω | (ω, Y ω) ∈ C}) := by
   …

5. theorem OAI.SLEExactGauge.normalizedDensity_event_lower_bound_of_condExp line 105

   Source documentation

   A lower bound on the density at a finite stop transfers any event observable there to the terminal tilted law.

   theorem normalizedDensity_event_lower_bound_of_condExp
       {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
       (Z M : Ω → ℝ) (hZ : Integrable Z P) (hZpos : 0 ≤ᵐ[P] Z)
       (hM : M =ᵐ[P] P[Z | m])
       (a c : ℝ) (ha : 0 < a) (hc : 0 ≤ c)
       (E : Set Ω) (hE : MeasurableSet[m] E)
       (hbound : ∀ᵐ ω ∂P, ω ∈ E → c * a ≤ M ω) :
       ENNReal.ofReal c * P E ≤
         P.withDensity (fun ω => ENNReal.ofReal (Z ω / a)) E := by
   …