OAI/Probability/SLE/Stochastic/BrownianOptionalIntervals.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Conditional optional stopping between two bounded stopping times. The compensated identity follows from the discrete grid identity. The drift is required to have its sign only between the two stops, as needed between multipoint activation and completion switches.

  1. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.eval_joint_measurable line 15
  2. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.compensated_joint_measurable line 26
  3. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.compensated_bound line 36
  4. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.compensated_path_continuous line 51
  5. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.eval_stopped_integrable line 69
  6. lemma OAI.SLEExactGauge.SmoothTimeBrownianField.compensated_stopped_integrable line 84
  7. theorem OAI.SLEExactGauge.brownian_compensated_optional_integral line 101

    Source documentation

    The full compensated optional identity. No sign restriction on the drift is needed for this identity.

    theorem brownian_compensated_optional_integral
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t))
    (hBm : Measurable (fun q : ℝ≥0 × Ω => B q.1 q.2))
    (hBc : ∀ ω, Continuous (fun t => B t ω))
    {K : ℝ≥0} {F a : ℝ≥0 → Ω → ℝ → ℝ}
    (hF : SmoothTimeBrownianField B hm K F a)
    (τ : Ω → ℝ≥0)
    (hτ : IsStoppingTime (Filtration.natural B
      (fun t => (hm t).stronglyMeasurable)) (fun ω => (τ ω : WithTop ℝ≥0)))
    (T : ℝ≥0) (hb : ∀ ω, τ ω ≤ T) :
…

    Mentions: OAI.SLEExactGauge.SmoothTimeBrownianField

  8. lemma OAI.SLEExactGauge.stopping_time_piecewise_after line 148
  9. theorem OAI.SLEExactGauge.brownian_compensated_optional_interval line 169

    Source documentation

    Conditional compensated equality between two bounded stopping times.

    theorem brownian_compensated_optional_interval
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t))
    (hBm : Measurable (fun q : ℝ≥0 × Ω => B q.1 q.2))
    (hBc : ∀ ω, Continuous (fun t => B t ω))
    {K : ℝ≥0} {F a : ℝ≥0 → Ω → ℝ → ℝ}
    (hF : SmoothTimeBrownianField B hm K F a)
    (σ τ : Ω → ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
      (fun t => (hm t).stronglyMeasurable)) (fun ω => (σ ω : WithTop ℝ≥0)))
    (hτ : IsStoppingTime (Filtration.natural B
…

    Mentions: OAI.SLEExactGauge.SmoothTimeBrownianField

  10. theorem OAI.SLEExactGauge.brownian_time_field_optional_interval_le line 220

    Source documentation

    Only the drift between the stops needs to be nonpositive, and the inequality remains valid after restricting to any event known at the first stop.

    theorem brownian_time_field_optional_interval_le
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t))
    (hBm : Measurable (fun q : ℝ≥0 × Ω => B q.1 q.2))
    (hBc : ∀ ω, Continuous (fun t => B t ω))
    {K : ℝ≥0} {F a : ℝ≥0 → Ω → ℝ → ℝ}
    (hF : SmoothTimeBrownianField B hm K F a)
    (σ τ : Ω → ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
      (fun t => (hm t).stronglyMeasurable)) (fun ω => (σ ω : WithTop ℝ≥0)))
    (hτ : IsStoppingTime (Filtration.natural B
…

    Mentions: OAI.SLEExactGauge.SmoothTimeBrownianField