CoverChangeOfLaw.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-stop change of measure in the missed-cell estimate of prop:dense-cover-upper, An explicit exact Hausdorff gauge for SLE.

A conditional approach estimate is the hypothesis for the conditioning and change-of-law steps.

theorem OAI.SLEExactGauge.setLIntegral_eq_mul_normalizedDensity line 22

Source documentation

Restricting a normalized density to an event exactly recovers its unnormalized integral. No measurability of the density is needed here.

theorem setLIntegral_eq_mul_normalizedDensity
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (w : Ω → ℝ) {a : ℝ} (ha : 0 < a) {A : Set Ω} (hA : MeasurableSet A) :
    (∫⁻ ω in A, ENNReal.ofReal (w ω) ∂P) =
      ENNReal.ofReal a *
        P.withDensity (fun ω => ENNReal.ofReal (w ω / a)) A := by
…

theorem OAI.SLEExactGauge.finiteCenteredLaw_event_identity line 37

Source documentation

The precise event identity for the finite centered law, at a fixed logarithmic conformal-radius stop.

theorem finiteCenteredLaw_event_identity
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (κ : ℝ)
    (B : ℝ≥0 → Ω → ℝ) (γ : Ω → ℝ≥0 → ℂ)
    (G : Ω → ℝ≥0 → ℂ → ℂ) (z : ℂ) (hz : z ∈ upperHalfPlane)
    (u : ℝ) {A : Set Ω} (hA : MeasurableSet A) :
    (∫⁻ ω in A, ENNReal.ofReal
      (stoppedGreen κ (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) z u) ∂P) =
      ENNReal.ofReal (initialGreen κ z) * finiteCenteredLaw P κ B γ G z u A :=
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.stoppedGreen, OAI.SLEExactGauge.initialGreen, OAI.SLEExactGauge.finiteCenteredLaw

theorem OAI.SLEExactGauge.measure_le_setLIntegral_of_conditional_approach line 49

Source documentation

A conditional approach bound can be integrated on any event determined by the conditioning sigma algebra. The smaller event need not be measurable.

theorem measure_le_setLIntegral_of_conditional_approach
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
    (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
    {E V A : Set Ω} (hV : MeasurableSet[mΩ] V) (hA : MeasurableSet[m] A)
    (hE : E ⊆ V ∩ A) (W : Ω → ℝ≥0∞) (K : ℝ≥0∞) (hK : K ≠ ∞)
    (happroach : ∀ᵐ ω ∂P, ω ∈ A →
      P⁻[V.indicator (fun _ => 1) | m] ω ≤ K * W ω) :
    P E ≤ K * ∫⁻ ω in A, W ω ∂P := by
…

theorem OAI.SLEExactGauge.finiteCenteredLaw_missed_cell_bound line 72

Source documentation

Transfer a visited cell with no candidate from the original law to a finite centered law. A is the adapted failure event and V the visit event. The displayed conditional approach bound is the only probabilistic estimate assumed by this reduction.

theorem finiteCenteredLaw_missed_cell_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
    (κ : ℝ) (B : ℝ≥0 → Ω → ℝ) (γ : Ω → ℝ≥0 → ℂ)
    (G : Ω → ℝ≥0 → ℂ → ℂ) (z : ℂ) (hz : z ∈ upperHalfPlane) (u : ℝ)
    (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
    {E V A : Set Ω} (hV : MeasurableSet[mΩ] V) (hA : MeasurableSet[m] A)
    (hE : E ⊆ V ∩ A) (C r p : ℝ)
    (happroach : ∀ᵐ ω ∂P, ω ∈ A →
      P⁻[V.indicator (fun _ => 1) | m] ω ≤ ENNReal.ofReal (C * r ^ p) *
        ENNReal.ofReal (stoppedGreen κ (fun t => Real.sqrt κ * B t ω)
          (γ ω) (G ω) z u)) :
    P E ≤ ENNReal.ofReal (C * r ^ p) * ENNReal.ofReal (initialGreen κ z) *
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.stoppedGreen, OAI.SLEExactGauge.initialGreen

theorem OAI.SLEExactGauge.finiteCenteredLaw_missed_cell_bound_of_failure_bound line 94

Source documentation

Any tilted-law failure estimate, in particular the stretched exponential bound from repeated adapted tests, gives the corresponding missed-cell bound.

theorem finiteCenteredLaw_missed_cell_bound_of_failure_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
    (κ : ℝ) (B : ℝ≥0 → Ω → ℝ) (γ : Ω → ℝ≥0 → ℂ)
    (G : Ω → ℝ≥0 → ℂ → ℂ) (z : ℂ) (hz : z ∈ upperHalfPlane) (u : ℝ)
    (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
    {E V A : Set Ω} (hV : MeasurableSet[mΩ] V) (hA : MeasurableSet[m] A)
    (hE : E ⊆ V ∩ A) (C r p : ℝ) (ε : ℝ≥0∞)
    (happroach : ∀ᵐ ω ∂P, ω ∈ A →
      P⁻[V.indicator (fun _ => 1) | m] ω ≤ ENNReal.ofReal (C * r ^ p) *
        ENNReal.ofReal (stoppedGreen κ (fun t => Real.sqrt κ * B t ω)
          (γ ω) (G ω) z u))
    (hfailure : @finiteCenteredLaw Ω mΩ P κ B γ G z u A ≤ ε) :
…

Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.stoppedGreen, OAI.SLEExactGauge.finiteCenteredLaw

theorem OAI.SLEExactGauge.finiteCenteredLaw_adapted_failures_bound line 113

Source documentation

The failure probability is a product bound under the centered law; no independence assumption is used.

theorem finiteCenteredLaw_adapted_failures_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (κ : ℝ) (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)
    (filtration : Filtration ℕ mΩ) (failure : ℕ → Set Ω)
    (hmeas : ∀ n, MeasurableSet[filtration (n + 1)] (failure n))
    (q : ℝ≥0∞)
    (hstep : ∀ n (A : Set Ω), MeasurableSet[filtration n] A →
…

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