MultipointSwitches.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite switching for the regularized multipoint product. Smooth pieces may change at bounded stopping times, provided the jumps are downward. A completed factor can therefore remain constant on all later pieces without any condition on its subsequent lifetime.

theorem OAI.SLEExactGauge.brownian_finite_branch_optional_interval_le line 21

Source documentation

At a switching time the active/completed pattern has only finitely many possibilities. Apply the conditional interval estimate on each past-measurable branch and sum. The branch formula also covers several simultaneous switches.

theorem brownian_finite_branch_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 ω))
    (σ τ : Ω → ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
      (fun t => (hm t).stronglyMeasurable)) (fun ω => (σ ω : WithTop ℝ≥0)))
    (hτ : IsStoppingTime (Filtration.natural B
      (fun t => (hm t).stronglyMeasurable)) (fun ω => (τ ω : WithTop ℝ≥0)))
    (hστ : ∀ ω, σ ω ≤ τ ω) (T : ℝ≥0) (hb : ∀ ω, τ ω ≤ T)
…

theorem OAI.SLEExactGauge.brownian_finite_switch_optional_le line 64

Source documentation

Patching finitely many bounded stopping intervals preserves the conditional expectation bound. Each field is required to have nonpositive drift only on its own interval.

theorem brownian_finite_switch_optional_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 ω))
    (N : ℕ) (τ : ℕ → Ω → ℝ≥0)
    (hτ : ∀ n, n ≤ N → IsStoppingTime (Filtration.natural B
      (fun t => (hm t).stronglyMeasurable)) (fun ω => (τ n ω : WithTop ℝ≥0)))
    (hmono : ∀ n, n < N → ∀ ω, τ n ω ≤ τ (n+1) ω)
    (T : ℝ≥0) (hbound : ∀ n, n ≤ N → ∀ ω, τ n ω ≤ T)
    (K : ℕ → ℝ≥0) (F a : ℕ → ℝ≥0 → Ω → ℝ → ℝ)
…

def OAI.SLEExactGauge.Multipoint.activeFactor line 128
lemma OAI.SLEExactGauge.Multipoint.activeFactor_activation_le line 131
lemma OAI.SLEExactGauge.Multipoint.activeFactor_completion_jump line 141
Source documentation
Completion freezes the factor at its angle-independent lower bound.
```
lemma activeFactor_completion_jump {p β U θ : ℝ}
    (hp : 0 < p) (hU : 0 ≤ U) (hθ : 0 ≤ Real.sin θ) :
    Real.exp (p / 2 * U) / 3 ≤ activeFactor p β U U θ := by
…
```
Mentions: OAI.SLEExactGauge.Multipoint.activeFactor
lemma OAI.SLEExactGauge.Multipoint.activeFactor_nonneg line 149
lemma OAI.SLEExactGauge.Multipoint.finite_factor_switch_le line 158
Source documentation
Simultaneous activation or completion of any subset still gives a downward jump for the finite product. Unchanged completed factors need only be nonnegative constants.
```
lemma finite_factor_switch_le {ι : Type*} (s : Finset ι) (before after : ι → ℝ)
    (hafter : ∀ i ∈ s, 0 ≤ after i) (hle : ∀ i ∈ s, after i ≤ before i) :
    (∏ i ∈ s, after i) ≤ ∏ i ∈ s, before i :=
…
```