ShiftedInterface

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

The three-lane interface of the §4.1 proportion assembly, at an arbitrary base

ABK26, §4.1, p.independence.between.scales. LaneInterface is the base-0 interface: each lane delivers a tail for the window {0,…,n}. The §4.1 proportion display is quantified over every base scale m₀ : ℤ and reads its window as Finset.range (Mw+1) shifted by m₀. This module is that interface, re-based:

• LaneTailFrom M Ev θ c₁ — one lane's endpoint at every base: for every m₀ : ℤ and every window length n, the density of scales k ∈ {m₀,…,m₀+n} at which Ev fails exceeds θ with probability at most exp(−c₁n)/3.
• measure_scaleProp_compl_goodEventBase_le_shift / measure_scaleProp_goodEventBase_le_shift — the three-fold union bound, at every base.
• exists_ratioTail_goodEventBase_shift — the composition: the two proved lanes (𝒢₀ from ShiftedG0Lane, 𝒢₁ from ShiftedG1Lane) plus the 𝒢₂ lane as a named LaneTailFrom slot of the identical shape.

References

• ABK26, p.independence.between.scales; d.good.event.for.lambda, (e.lambda.good.events); p.concentration.for.scales, (the m₀ reduction).

1. The lane endpoint at every base

def Algsuperdiff.Section4.Provider.Proportion.LaneTailFrom {d : ℕ} (M : Section3.ABKModel d) (Ev : ℤ → Set (Section3.Cutoff.CutoffSample d)) (theta c1 : ℝ) : Prop

One lane's ratio-tail endpoint at every base scale. LaneTailFrom M Ev θ c₁ says that for every base m₀ : ℤ and every window {m₀,…,m₀+n} the density of scales at which Ev fails exceeds θ with probability at most exp(−c₁n)/3.

The base-0 instance is LaneTail M Ev θ c₁; the prefactor 1/3 is the union-bound share of the three-lane split.

Equations

• Algsuperdiff.Section4.Provider.Proportion.LaneTailFrom M Ev theta c1 = ∀ (m0 : ℤ), Algsuperdiff.Section4.Provider.Proportion.LaneTail M (fun (k : ℤ) => Ev (m0 + k)) theta c1

theorem Algsuperdiff.Section4.Provider.Proportion.LaneTailFrom.mono_level {d : ℕ} {M : Section3.ABKModel d} {Ev : ℤ → Set (Section3.Cutoff.CutoffSample d)} {theta theta' c1 : ℝ} (h : theta ≤ theta') (H : LaneTailFrom M Ev theta c1) : LaneTailFrom M Ev theta' c1

A based lane endpoint transfers to every larger level.

2. The three-fold union bound, at every base

theorem Algsuperdiff.Section4.Provider.Proportion.measure_scaleProp_compl_goodEventBase_le_shift {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (s : { s : ℝ // 0 < s }) (ep theta c1 : ℝ) (h0 : LaneTailFrom M (fun (k : ℤ) => Support.eventG0 M Ccg k) (theta / 3) c1) (h1 : LaneTailFrom M (fun (k : ℤ) => Support.eventG1 M k (↑s) (↑s * ep * √(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)) (theta / 3) c1) (h2 : LaneTailFrom M (fun (k : ℤ) => Support.eventG2 M k s ep) (theta / 3) c1) (m0 : ℤ) (n : ℕ) : ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Support.goodEventBase M Ccg (m0 + k) s ep)ᶜ) n omega} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n))

The three lanes recombine into the good event, at every base. With the three lane endpoints at level θ/3, the density of scales k ∈ {m₀,…,m₀+n} at which the frozen good event's untranslated body goodEventBase fails exceeds θ with probability at most exp(−c₁n).

theorem Algsuperdiff.Section4.Provider.Proportion.measure_scaleProp_goodEventBase_le_shift {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (s : { s : ℝ // 0 < s }) (ep theta c1 : ℝ) (htheta0 : 0 < theta) (h0 : LaneTailFrom M (fun (k : ℤ) => Support.eventG0 M Ccg k) (theta / 4) c1) (h1 : LaneTailFrom M (fun (k : ℤ) => Support.eventG1 M k (↑s) (↑s * ep * √(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)) (theta / 4) c1) (h2 : LaneTailFrom M (fun (k : ℤ) => Support.eventG2 M k s ep) (theta / 4) c1) (m0 : ℤ) (n : ℕ) : ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => Support.goodEventBase M Ccg (m0 + k) s ep) n omega ≤ 1 - theta} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n))

The good-proportion form of the three-lane union bound, at every base. With the three lane endpoints at level θ/4, the frozen display's own clause avsum 𝟙{𝒢} ≤ 1 − θ over the window {m₀,…,m₀+n} has probability at most exp(−c₁n). The conversion from the bad form the lanes deliver costs one strict inequality, which is why the lanes are run at θ/4 instead of θ/3.

3. The two proved lane certificates, at every base

theorem Algsuperdiff.Section4.Provider.Proportion.exists_laneTailFrom_eventG0 (d : ℕ) : ∃ (r : ℕ), 1 ≤ r ∧ ∃ (C : ℝ), 6 ≤ C ∧ ∀ (M : Section3.ABKModel d) (theta c1 : ℝ), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → 0 < theta → theta * (↑r + 1) < 1 → C ^ 9 * M.gamma ^ 2 ≤ theta * Section3.Disorder.cstar M ^ 8 → 0 ≤ c1 → c1 * M.gamma ≤ 1 → LaneTailFrom M (fun (k : ℤ) => Support.eventG0 M (Support.cgEllipLowerConstant d) k) theta c1

The 𝒢₀ lane in LaneTailFrom shape, with one dependence range r(d) and one constant C(d) chosen before the level, the rate, the model and the base. This is ShiftedG0Lane.exists_ratioTail_eventG0_uniform_shift read through LaneTailFrom.

theorem Algsuperdiff.Section4.Provider.Proportion.laneTailFrom_eventG1_shellThreshold {d : ℕ} (M : Section3.ABKModel d) {s ep theta c1 : ℝ} {r : ℕ} (hs0 : 0 < s) (hs1 : s ≤ 1) (hep0 : 0 < ep) (hr1 : 1 ≤ r) (htheta0 : 0 < theta) (hthetar : theta * (↑r + 1) < 1) (hc1 : 0 ≤ c1) (hcond : g1ThresholdConst d r * (1 + c1) * M.gamma ≤ theta * Section3.Disorder.cstar M * s ^ 6 * ep ^ 2) : LaneTailFrom M (fun (k : ℤ) => Support.eventG1 M k s (s * ep * √(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)) theta c1

The 𝒢₁ lane in LaneTailFrom shape, at the substituted threshold s ε √c⋆ (√γ)⁻¹ of e.lambda.good.events and at any dependence range r ≥ 1. This is ShiftedG1Lane.ratioTail_eventG1_shellThreshold_shift read through LaneTailFrom.

4. The three-lane endpoint at every base, with the 𝒢₂ slot

theorem Algsuperdiff.Section4.Provider.Proportion.exists_ratioTail_goodEventBase_shift (d : ℕ) : ∃ (r : ℕ), 1 ≤ r ∧ ∃ (C : ℝ), 6 ≤ C ∧ ∀ (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (ep theta c1 : ℝ), ↑s ≤ 1 → 0 < ep → 0 < theta → theta * (↑r + 1) < 1 → 0 ≤ c1 → c1 * M.gamma ≤ 1 → M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → C ^ 10 * M.gamma ^ 2 ≤ theta * Section3.Disorder.cstar M ^ 8 → C * (1 + c1) * M.gamma ≤ theta * Section3.Disorder.cstar M * ↑s ^ 6 * ep ^ 2 → LaneTailFrom M (fun (k : ℤ) => Support.eventG2 M k s ep) (theta / 4) c1 → (∀ (m0 : ℤ) (n : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | theta < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Support.goodEventBase M (Support.cgEllipLowerConstant d) (m0 + k) s ep)ᶜ) n omega} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n))) ∧ ∀ (m0 : ℤ) (n : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => Support.goodEventBase M (Support.cgEllipLowerConstant d) (m0 + k) s ep) n omega ≤ 1 - theta} ≤ ENNReal.ofReal (Real.exp (-c1 * ↑n))

The §4.1 proportion premise at every base, from two proved lanes and one named slot.

One dependence range r(d) and one constant C(d), both fixed before every parameter and before the base. The 𝒢₀ and 𝒢₁ lanes are proved; the 𝒢₂ lane enters as the named hypothesis hG2, in the identical LaneTailFrom shape. Both output forms are delivered at every base m₀ : ℤ: the bad-density form the union bound produces, and the good-proportion form avsum 𝟙{𝒢} ≤ 1 − θ in which the printed display is stated.

Every window n is covered, including the short windows n < r. The rate c₁ is the caller's, up to the 𝒢₀ lane's ceiling c₁γ ≤ 1.