MultipointPiecewiseClock.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Bounded discount rates selected at finitely many stopping-time switches. The rate may jump at the switches; its accumulated clock is adapted and Lipschitz, and its derivative agrees with the rate almost everywhere.

lemma OAI.SLEExactGauge.Multipoint.sortedStopAt_no_intermediate line 20

Source documentation

Sorting all raw switches leaves no original switch strictly between successive entries, including when some entries coincide.

lemma sortedStopAt_no_intermediate {Ω : Type*} (l : List (Ω → ℝ≥0)) (H : ℝ≥0)
    (hl : ∀ σ ∈ l, ∀ ω, σ ω ≤ H) (σ : Ω → ℝ≥0) (hσ : σ ∈ l)
    (n : ℕ) (ω : Ω) (hn : sortedStopAt l H n ω < σ ω) :
    sortedStopAt l H (n+1) ω ≤ σ ω := by
…

Mentions: OAI.SLEExactGauge.Multipoint.sortedStopAt

lemma OAI.SLEExactGauge.Multipoint.sortedStopAt_reached_iff line 34
def OAI.SLEExactGauge.Multipoint.stoppedBranchRate line 46
lemma OAI.SLEExactGauge.Multipoint.stoppedBranchRate_measurable line 51

lemma OAI.SLEExactGauge.Multipoint.stoppedBranch_start_measurable line 65

Source documentation

A branch known at its starting stop gives a measurable stochastic interval on every finite deterministic horizon.

lemma stoppedBranch_start_measurable {Ω : Type*} [mΩ : MeasurableSpace Ω]
    (ℱ : Filtration ℝ≥0 mΩ) (σ : Ω → ℝ≥0)
    (hσ : IsStoppingTime ℱ (fun ω => (σ ω : WithTop ℝ≥0)))
    (A : Set Ω) (hA : MeasurableSet[hσ.measurableSpace] A) (T : ℝ≥0) :
    MeasurableSet[Subtype.instMeasurableSpace.prod (ℱ T)]
      {p : Iic T × Ω | p.2 ∈ A ∧ σ p.2 ≤ p.1} := by
…

lemma OAI.SLEExactGauge.Multipoint.stoppedBranchRate_progressive line 94
lemma OAI.SLEExactGauge.Multipoint.stoppedBranchRate_norm_le line 118
lemma OAI.SLEExactGauge.Multipoint.stoppedBranchRate_nonneg line 126

lemma OAI.SLEExactGauge.Multipoint.bounded_rate_locallyIntegrable line 135

Source documentation

Local integrability of a bounded measurable rate, without continuity.

lemma bounded_rate_locallyIntegrable {Ω : Type*}
    (g : ℝ≥0 → Ω → ℝ) (hg : ∀ ω, Measurable (fun t => g t ω))
    (C : ℝ≥0) (hC : ∀ t ω, |g t ω| ≤ C) (ω : Ω) :
    LocallyIntegrable (fun u : ℝ => g u.toNNReal ω) volume := by
…

lemma OAI.SLEExactGauge.Multipoint.discountClock_lipschitz_of_measurable line 146
lemma OAI.SLEExactGauge.Multipoint.discountClock_increment_of_measurable line 167
lemma OAI.SLEExactGauge.Multipoint.discountClock_ae_derivative line 178
lemma OAI.SLEExactGauge.Multipoint.discountClock_adapted_of_progressive line 189
def OAI.SLEExactGauge.Multipoint.finiteSwitchRate line 214
Source documentation
The finite index may comprise a stage and its finite past-measurable pattern. Empty or simultaneous stages contribute zero.
```
def finiteSwitchRate {Ω ι : Type*} (s : Finset ι) (σ τ : ι → Ω → ℝ≥0)
    (A : ι → Set Ω) (g : ι → ℝ≥0 → Ω → ℝ) (t : ℝ≥0) (ω : Ω) : ℝ :=
…
```
lemma OAI.SLEExactGauge.Multipoint.finiteSwitchRate_measurable line 218
lemma OAI.SLEExactGauge.Multipoint.finiteSwitchRate_progressive line 228
lemma OAI.SLEExactGauge.Multipoint.finiteSwitchRate_norm_le line 240
lemma OAI.SLEExactGauge.Multipoint.finiteSwitchRate_nonneg line 249

theorem OAI.SLEExactGauge.Multipoint.finiteSwitchClock_regular line 258

Source documentation

The state used by the smooth-field adapter. No differentiability of rates at switching times is required.

theorem finiteSwitchClock_regular {Ω ι : Type*} [mΩ : MeasurableSpace Ω]
    (ℱ : Filtration ℝ≥0 mΩ) (s : Finset ι) (σ τ : ι → Ω → ℝ≥0)
    (hσ : ∀ i ∈ s, IsStoppingTime ℱ (fun ω => (σ i ω : WithTop ℝ≥0)))
    (hτ : ∀ i ∈ s, IsStoppingTime ℱ (fun ω => (τ i ω : WithTop ℝ≥0)))
    (A : ι → Set Ω) (hA : ∀ (i) (hi : i ∈ s), MeasurableSet[(hσ i hi).measurableSpace] (A i))
    (g : ι → ℝ≥0 → Ω → ℝ)
    (hgm : ∀ i ∈ s, Measurable (Function.uncurry (g i)))
    (hgp : ∀ i ∈ s, IsProgressive ℱ (g i))
    (C : ι → ℝ≥0) (hC : ∀ i ∈ s, ∀ t ω, |g i t ω| ≤ C i) :
    let R := finiteSwitchRate s σ τ A g
…

Mentions: OAI.SLEExactGauge.Multipoint.finiteSwitchRate