RandomRestartEvents.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Random geometric restrictions after restart. The actual restricted restart law determines the joint law of the stopped past and the fresh path. Consequently a past-measurable family of positive-probability passage events has positive conditional probability, without countable past certificates.

theorem OAI.SLEExactGauge.restart_joint_law line 16
theorem OAI.SLEExactGauge.restart_lintegral_random_test line 37

theorem OAI.SLEExactGauge.restart_condLExp_random_test line 60

Source documentation

Conditional integration for a genuinely random restriction on the fresh path, provided its dependence on the stopped past is measurable.

theorem restart_condLExp_random_test
    {Ω 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 • ν)
    (f : Ω × X → ℝ≥0∞) (hf : @Measurable (Ω × X) ℝ≥0∞ (m.prod mX) _ f) :
    (fun ω => ∫⁻ x, f (ω, x) ∂ν) =ᵐ[P]
      P⁻[(fun ω => f (ω, Y ω)) | m] := by
…

theorem OAI.SLEExactGauge.conditional_passage_positive_of_random_sections line 87