RestartWeightedKernel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integration of measurable marked-state density kernels against the actual independent restarted driver. This is used with the proved centered SLE section bounds and the deterministic restarted Green-density bound.

theorem OAI.SLEExactGauge.restart_setLIntegral_random_test line 15

theorem OAI.SLEExactGauge.restart_weighted_event_lower_bound line 44

Source documentation

A lower section bound gives a lower tilted probability on every event in the stopped past. The density domination is pointwise along the actual fresh driver and is supplied by Loewner restart composition.

theorem restart_weighted_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 • ν)
    (K : Ω × X → ℝ≥0∞) (hK : @Measurable (Ω × X) ℝ≥0∞ (m.prod mX) _ K)
    (C : Set (Ω × X)) (hC : @MeasurableSet (Ω × X) (m.prod mX) C)
    (V Z : Ω → ℝ≥0∞) (q : ℝ≥0∞) (hq : q ≠ ∞)
    (E : Set Ω) (hE : MeasurableSet[mΩ] E)
    (hsections : ∀ᵐ ω ∂P, q * V ω ≤ ∫⁻ x, C.indicator K (ω, x) ∂ν)
…