OAI/Probability/SLE/Geometry/RestartContinuationKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Conditional path tests after a finite restart. Splitting again at τ+t identifies the conditional mean in the full original stopped filtration; no factorization of its events through the restarted path is required.

  1. def OAI.SLEExactGauge.driverContinuationMean line 19
  2. lemma OAI.SLEExactGauge.driverContinuation_test_measurable line 23
  3. lemma OAI.SLEExactGauge.driverContinuationMean_measurable line 32
  4. lemma OAI.SLEExactGauge.sourceRestartDriverPath_measurable line 38
  5. theorem OAI.SLEExactGauge.source_driver_continuation_condLExp line 48
  6. theorem OAI.SLEExactGauge.driverContinuationMean_eq_of_past_integrals line 82

    Source documentation

    Deterministic-time conditional identities identify the continuation section on the canonical driver law.

    theorem driverContinuationMean_eq_of_past_integrals
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
    (t : ℝ≥0) (f K : C(ℝ≥0,ℝ) → ℝ≥0∞) (hf : Measurable f)
    (hK : Measurable[driverPathFiltration t] K)
    (hmean : ∀ A : Set Ω,
      MeasurableSet[(Filtration.natural B (fun s => (hm s).stronglyMeasurable)) t] A →
      (∫⁻ ω in A, f (sourceDriverPath B hc ω) ∂P)=
        ∫⁻ ω in A, K (sourceDriverPath B hc ω) ∂P) :
    driverContinuationMean (P.map (sourceDriverPath B hc)) t f =ᵐ[P.map (sourceDriverPath B hc)] K := by
…

    Mentions: OAI.SLEExactGauge.driverPathFiltration, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.driverContinuationMean

  7. theorem OAI.SLEExactGauge.source_restart_continuation_condLExp line 108

    Source documentation

    The conditioning sigma algebra is the full original past at τ+t.

    theorem source_restart_continuation_condLExp
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
    (τ : Ω → ℝ≥0)
    (hτ : IsStoppingTime (Filtration.natural B (fun s => (hm s).stronglyMeasurable))
      (fun ω => (τ ω : WithTop ℝ≥0)))
    (t : ℝ≥0) (f : C(ℝ≥0,ℝ) → ℝ≥0∞) (hf : Measurable f) :
    (fun ω => driverContinuationMean (P.map (sourceDriverPath B hc)) t f
      (sourceRestartDriverPath B hc τ ω)) =ᵐ[P]
    P⁻[(fun ω => f (sourceRestartDriverPath B hc τ ω)) | shiftedStoppingFiltration hτ t] := by
…

    Mentions: OAI.SLEExactGauge.driverContinuationMean, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.sourceRestartDriverPath, OAI.SLEExactGauge.shiftedStoppingFiltration

  8. theorem OAI.SLEExactGauge.source_restart_condLExp_of_section_ae line 145

    Source documentation

    A canonical section identity therefore holds in the larger shifted filtration, not merely in the natural filtration of the fresh driver.

    theorem source_restart_condLExp_of_section_ae
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
    (τ : Ω → ℝ≥0)
    (hτ : IsStoppingTime (Filtration.natural B (fun s => (hm s).stronglyMeasurable))
      (fun ω => (τ ω : WithTop ℝ≥0)))
    (t : ℝ≥0) (f K : C(ℝ≥0,ℝ) → ℝ≥0∞) (hf : Measurable f) (hK : Measurable K)
    (hsection : driverContinuationMean (P.map (sourceDriverPath B hc)) t f
      =ᵐ[P.map (sourceDriverPath B hc)] K) :
    (fun ω => K (sourceRestartDriverPath B hc τ ω)) =ᵐ[P]
    P⁻[(fun ω => f (sourceRestartDriverPath B hc τ ω)) | shiftedStoppingFiltration hτ t] := by
…

    Mentions: OAI.SLEExactGauge.driverContinuationMean, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.sourceRestartDriverPath, OAI.SLEExactGauge.shiftedStoppingFiltration

  9. theorem OAI.SLEExactGauge.source_restart_integral_of_section_ae line 169
  10. theorem OAI.SLEExactGauge.source_restart_integral_of_original_kernel line 190
  11. theorem OAI.SLEExactGauge.source_restart_bind_of_original_kernel line 213

    Source documentation

    Measure-kernel form of the continuation identity. This applies to the sum of the finite-time raw mass and its current Green measure.

    theorem source_restart_bind_of_original_kernel
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
    (t : ℝ≥0) (N K : C(ℝ≥0,ℝ) → Measure upperHalfPlane) (hN : Measurable N)
    (hK : Measurable[driverPathFiltration t] K)
    (hmean : ∀ A : Set Ω,
      MeasurableSet[(Filtration.natural B (fun s => (hm s).stronglyMeasurable)) t] A →
      (P.restrict A).bind (fun ω => N (sourceDriverPath B hc ω))=
        (P.restrict A).bind (fun ω => K (sourceDriverPath B hc ω)))
    (τ : Ω → ℝ≥0)
    (hτ : IsStoppingTime (Filtration.natural B (fun s => (hm s).stronglyMeasurable))
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.driverPathFiltration, OAI.SLEExactGauge.sourceDriverPath