RandomScaleWitness

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The random minimal scale as an ℕ∞-valued witness

A bad-window predicate is a family bad : ℕ → Ω → Prop, where bad n ω says that the window of length n is bad for the sample ω. The associated random minimal scale is

minimalScale bad ω = ⨆ (n) (_ : bad n ω), (n + 1),

taken in the complete lattice ℕ∞ = WithTop ℕ. Working in ℕ∞ rather than ℕ is what makes the domination property "every bad window length is < Z" hold for every ω with no boundedness hypothesis: le_iSup needs none in a complete lattice. Consequently the deterministic extraction minimalScaleEN_not_bad_of_le is a genuine, ω-uniform fact — vacuous precisely on the ⊤-event where bad windows of unbounded length occur.

Contents

• minimalScaleEN — the witness.
• minimalScaleEN_not_bad_of_le and minimalScaleEN_tail_eq — its two deterministic extractions.
• minimalScaleEN_tail_subset — the tail-event inclusion used by summation.
• minimalScaleEN_sup — the witness for a disjunction is the pointwise maximum.
• measurable_minimalScaleEN — measurability from measurable bad-window events.

Everything is generic over the sample space Ω: no source-specific carrier and no measure appears in this module.

noncomputable def Algsuperdiff.Probability.minimalScaleEN {Ω : Type u_1} (bad : ℕ → Ω → Prop) (ω : Ω) : ℕ∞

The random minimal scale, ℕ∞-valued: minimalScale bad ω = ⨆ (n) (_ : bad n ω), (n + 1). It is 0 when no window is bad, and ⊤ when bad windows of unbounded length occur.

Equations

• Algsuperdiff.Probability.minimalScaleEN bad ω = ⨆ (n : ℕ), ⨆ (_ : bad n ω), ↑n + 1

theorem Algsuperdiff.Probability.minimalScaleEN_not_bad_of_le {Ω : Type u_1} {bad : ℕ → Ω → Prop} {ω : Ω} {L : ℕ} (h : minimalScaleEN bad ω ≤ ↑L) : ¬bad L ω

Deterministic extraction. If the random scale is at most the window length L, then the window of length L is not bad. (Vacuous when minimalScale bad ω = ⊤, since then no finite L bounds it.)

theorem Algsuperdiff.Probability.minimalScaleEN_tail_eq {Ω : Type u_1} (bad : ℕ → Ω → Prop) (N : ℕ) : {ω : Ω | ↑(N + 1) ≤ minimalScaleEN bad ω} = ⋃ (i : ℕ), {ω : Ω | bad (N + i) ω}

The tail event of the minimal scale is exactly a union of bad windows. Since minimalScale bad ω = ⨆ (l) (_ : bad l ω), (l + 1), the event {N + 1 ≤ Z} says that some bad window has length ≥ N. Note the index shift: the union starts at N, not at N + 1.

theorem Algsuperdiff.Probability.minimalScaleEN_tail_subset {Ω : Type u_1} (bad : ℕ → Ω → Prop) (N : ℕ) : {ω : Ω | ↑(N + 1) ≤ minimalScaleEN bad ω} ⊆ ⋃ (i : ℕ), {ω : Ω | bad (N + i) ω}

The tail event of the minimal scale is contained in a union of bad windows — the half consumed by the geometric summation.

theorem Algsuperdiff.Probability.minimalScaleEN_sup {Ω : Type u_1} (bad₁ bad₂ : ℕ → Ω → Prop) (ω : Ω) : minimalScaleEN (fun (n : ℕ) (ω : Ω) => bad₁ n ω ∨ bad₂ n ω) ω = max (minimalScaleEN bad₁ ω) (minimalScaleEN bad₂ ω)

The maximum of two witnesses is the witness of the disjunction. This is the assembly rule for a scale built from two independent families of bad windows.

theorem Algsuperdiff.Probability.measurableSet_minimalScaleEN_tail {Ω : Type u_1} [MeasurableSpace Ω] {bad : ℕ → Ω → Prop} (hbad : ∀ (n : ℕ), MeasurableSet {ω : Ω | bad n ω}) (N : ℕ) : MeasurableSet {ω : Ω | ↑N ≤ minimalScaleEN bad ω}

Measurability of the ℕ∞-tail events. If every bad-window event is measurable, then so is every tail event {(N : ℕ∞) ≤ Z} of the witness.

theorem Algsuperdiff.Probability.measurable_minimalScaleEN {Ω : Type u_1} [MeasurableSpace Ω] {bad : ℕ → Ω → Prop} (hbad : ∀ (n : ℕ), MeasurableSet {ω : Ω | bad n ω}) : Measurable (minimalScaleEN bad)

The measurability criterion for the random minimal scale.

If every bad-window event {ω | bad n ω} is measurable, then the witness minimalScale bad is measurable as a map into ℕ∞.

The mechanism: {Z = n} is the difference of the two tail events {n ≤ Z} and {n + 1 ≤ Z}, each of which is a countable union of bad-window events; the ⊤-fibre is then automatic because ℕ∞ is countable.