OAI/Probability/SLE/Gauge/ExtendedExperimentStop.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.cutoffStop line 15
2. lemma OAI.SLEExactGauge.cutoffStop_coe line 18
3. lemma OAI.SLEExactGauge.cutoffStop_stopping line 24
4. lemma OAI.SLEExactGauge.cutoffStop_success_measurable line 33
5. lemma OAI.SLEExactGauge.cutoffStop_eq_on_success line 43
6. theorem OAI.SLEExactGauge.normalizedDensity_completed_event_lower_bound line 50

   Source documentation

   The normalized terminal density pays the same fixed cost when the completion stop is finite only on success.

   theorem normalizedDensity_completed_event_lower_bound
       {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
       (ℱ : Filtration ℝ≥0 mΩ)
       (Z : Ω → ℝ) (hZ : Integrable Z P) (hZpos : 0 ≤ᵐ[P] Z)
       (M : ℝ≥0 → Ω → ℝ)
       (hM : ∀ (σ : Ω → ℝ≥0) (hσ : IsStoppingTime ℱ
           (fun ω => (σ ω : WithTop ℝ≥0))),
         (fun ω => M (σ ω) ω) =ᵐ[P] P[Z | hσ.measurableSpace])
       (τ : Ω → WithTop ℝ≥0) (hτ : IsStoppingTime ℱ τ)
       (a c : ℝ) (ha : 0 < a) (hc : 0 ≤ c)
       (E : Set Ω) (hE : MeasurableSet[hτ.measurableSpace] E)
       (hfinite : ∀ᵐ ω ∂P, ω ∈ E → τ ω ≠ ⊤)
   …

7. theorem OAI.SLEExactGauge.finiteCenteredLaw_completed_experiment_lower_bound line 105

   Source documentation

   The successful dense experiment need not finish on unsuccessful samples. Its actual finite completion and angle bound on success suffice for the centered-law lower bound.

   theorem finiteCenteredLaw_completed_experiment_lower_bound
       {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
       {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
       (hBm : Measurable (fun p : ℝ≥0 × Ω => B p.1 p.2))
       (hBc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
       (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
       (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
       (hw : ∀ᵐ ω ∂P, IsCapacityTwoWitness
         (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
       (z : ℂ) (hz : z ∈ upperHalfPlane) (u : ℝ) (hu : 0 ≤ u)
       (τ : Ω → WithTop ℝ≥0)
       (hτ : IsStoppingTime (Filtration.natural B
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane