LaneInterface

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

ABK26, §4.1, p.independence.between.scales. The proof of that proposition splits 𝟙{𝒢(m; s, ε)ᶜ} into the three constituent complements and applies each lane's ratio lemma "with θ replaced by θ/3". This module is the interface of that step:

• LaneTail M Ev θ c₁ — the common endpoint shape of one lane: at every window {0,…,n} the density of scales at which Ev fails exceeds θ with probability at most exp(−c₁n)/3. It is exactly the conclusion shape the 𝒢₀ lane (RatioTailClosed) and the 𝒢₁ lane (G1RatioTail/G1ThresholdArith) deliver.
• scaleProp_add_scaleProp_compl — the complementarity avsum 𝟙{𝒢} + avsum 𝟙{𝒢ᶜ} = 1 of the good and bad scale densities, which converts a bad-density endpoint into the frozen display's good form.

References

• ABK26, p.independence.between.scales; d.good.event.for.lambda, (e.lambda.good.events).

1. The common lane endpoint

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

The shape of one lane's ratio-tail endpoint. LaneTail M Ev θ c₁ says that for every window {0,…,n} — including the short windows n < r that p.concentration.for.scales does not itself reach (covered inside the proved ratioTail_of_concentration) — the density of scales at which Ev fails exceeds θ with probability at most exp(−c₁n)/3.

The prefactor 1/3 is the union-bound share of the three-lane split: three lanes at exp(−c₁n)/3 recombine to exp(−c₁n).

Equations

• One or more equations did not get rendered due to their size.

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

A lane endpoint transfers to every larger level: the bad-density event shrinks as the level rises.

2. The good and bad scale densities

theorem Algsuperdiff.Section4.Provider.Proportion.scaleProp_add_scaleProp_compl {Omega : Type u_1} (Ev : ℤ → Set Omega) (n : ℕ) (omega : Omega) : Probability.IndicatorDensity.scaleProp Ev n omega + Probability.IndicatorDensity.scaleProp (fun (m : ℤ) => (Ev m)ᶜ) n omega = 1

The good and bad scale densities are complementary.