ProportionArith

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

The arithmetic of the §4.1 proportion assembly

ABK26, §4.1, p.independence.between.scales. The three lane endpoints of ShiftedInterface deliver, at every base m₀, a tail exp(−c₁n) for the window {m₀,…,m₀+n}. The §4.1 display asks instead for 6·exp(−A(M_w+1)) at a specific rate A read off the model. Four pieces of arithmetic separate the two, and they are collected here so that the assembly file carries only the composition:

• the window offset (exp_le_six_exp_of_one_le, exp_le_six_exp_of_zero): running the lanes at c₁ = 2A gives exp(−2A·M_w) ≤ 6·exp(−A(M_w+1)) for every M_w ≥ 1; the prefactor 6 of the printed display is exactly what pays for the (M_w+1)-versus-M_w offset, so it is not free.
• the M_w = 0 instance (setOf_scalePropFrom_zero_eq_compl, half_le_scaleProp_one_of_mem): at M_w = 0 the printed clause avsum 𝟙{𝒢} ≤ 1 − θ is the single bad event 𝒢(m₀)ᶜ, whose mass the lane package does not bound at window 0 (the bound there is 1). A single bad scale inside the window {m₀, m₀+1} already carries density ½, so the lane endpoint at window 1 bounds it as soon as the level is < ½.
• the level split (couplingG0_at_split, honestG1_at_split): the two proved lanes need θ(r+1) < 1, which the printed θ ≤ ½ does not give once r ≥ 2. Running them at θ/(8L), L = r+1, costs one factor L in each coupling, and that factor is absorbed into the assembly's own constant — the anchor's constant enters both couplings linearly, so an L-fold split is free while a C-fold split would not be.
• the anchor's clauses at a smaller constant (anchorRegime_shrink, anchorLevel_weaken, anchorNumerator_le): the regime clause is used only through the first branch of its min; the s⁻⁶ level clause implies the printed s⁻⁴ one once the constant is lowered; and on the printed window c⋆ ≤ 3/2, s, ε, θ ≤ ½ the numerator of the printed rate is at most 9/4, which is what keeps the 𝒢₀ lane's rate ceiling non-binding.

References

• ABK26, p.independence.between.scales; d.good.event.for.lambda.

1. The window offset

theorem Algsuperdiff.Section4.Provider.Proportion.exp_le_six_exp_of_one_le {A : ℝ} (hA : 0 ≤ A) {Mw : ℕ} (hMw : 1 ≤ Mw) : Real.exp (-(2 * A) * ↑Mw) ≤ 6 * Real.exp (-(A * (↑Mw + 1)))

The rate match on the long windows. With the lanes run at c₁ = 2A, the composed tail exp(−2A·M_w) sits under the printed 6·exp(−A(M_w+1)) for every M_w ≥ 1: 2M_w ≥ M_w + 1 there. The prefactor 6 is not consumed on this branch, but the (M_w+1)-versus-M_w offset is.

theorem Algsuperdiff.Section4.Provider.Proportion.exp_le_six_exp_of_zero {A : ℝ} (hA : 0 ≤ A) : Real.exp (-(2 * A) * ↑1) ≤ 6 * Real.exp (-(A * (↑0 + 1)))

The rate match at the single-scale window. At M_w = 0 the assembly reads the lane endpoint at window 1, whose tail is exp(−2A); the printed right-hand side there is 6·exp(−A).

2. The M_w = 0 instance

theorem Algsuperdiff.Section4.Provider.Proportion.setOf_scalePropFrom_zero_eq_compl {Ω : Type u_1} (Ev : ℤ → Set Ω) (m0 : ℤ) {theta : ℝ} (htheta0 : 0 < theta) (htheta1 : theta ≤ 1) : {omega : Ω | scalePropFrom Ev m0 0 omega ≤ 1 - theta} = (Ev m0)ᶜ

The single-scale window reads the printed clause as one bad event. At M_w = 0 the average avsum 𝟙{Ev} over {m₀} is the indicator of Ev m₀, and for 0 < θ ≤ 1 the clause avsum 𝟙{Ev} ≤ 1 − θ holds exactly on (Ev m₀)ᶜ.

theorem Algsuperdiff.Section4.Provider.Proportion.half_le_scaleProp_one_of_mem {Ω : Type u_1} (F : ℤ → Set Ω) (omega : Ω) (homega : omega ∈ F 0) : 1 / 2 ≤ Probability.IndicatorDensity.scaleProp F 1 omega

One member scale already fills half of a two-scale window. If ω ∈ F 0 then the density of F-scales over {0, 1} is at least ½. Read at F = fun k => (Ev (m₀+k))ᶜ, this is the device that reaches the M_w = 0 instance of the printed display from the lane package: the level at which the lanes run is far below ½.

3. The level split

theorem Algsuperdiff.Section4.Provider.Proportion.couplingG0_at_split {C1 L Ca cs s ep theta gamma : ℝ} (hC1 : 6 ≤ C1) (hL : 2 ≤ L) (hcs0 : 0 < cs) (hcs32 : cs ≤ 3 / 2) (hs0 : 0 < s) (hs12 : s ≤ 1 / 2) (hep0 : 0 < ep) (hep12 : ep ≤ 1 / 2) (hg0 : 0 < gamma) (hCa : (8 * L * C1) ^ 5 ≤ Ca) (hreg : gamma ≤ Ca⁻¹ * cs ^ 10) (hthetacond : Ca * cs⁻¹ ^ 2 * s⁻¹ ^ 4 * ep⁻¹ ^ 2 * gamma ≤ theta) : C1 ^ 10 * gamma ^ 2 ≤ theta / (8 * L) * cs ^ 8

The 𝒢₀ coupling survives the level split. The frozen proportion anchor's regime and level clauses, at any anchor constant C_a ≥ (8LC₁)⁵, give the 𝒢₀ lane's coupling at the split level θ/(8L). The split factor L enters the anchor constant polynomially, which is why absorbing L = r+1 into the assembly's C(d) is free.

theorem Algsuperdiff.Section4.Provider.Proportion.honestG1_at_split {C1 L C A cs s ep theta gamma : ℝ} (hL : 2 ≤ L) (hC : 8 * L * C1 ≤ C) (hA0 : 0 ≤ A) (hg0 : 0 < gamma) (hhonest : C * (1 + 2 * A) * gamma ≤ theta * cs * s ^ 6 * ep ^ 2) : C1 * (1 + 2 * A) * gamma ≤ theta / (8 * L) * cs * s ^ 6 * ep ^ 2

The honest 𝒢₁ condition survives the level split. If the honest 𝒢₁ condition C(1+2A)γ ≤ θ c⋆ s⁶ ε² holds at a constant C ≥ 8LC₁, then the 𝒢₁ lane's own coupling holds at the split level θ/(8L) with its constant C₁. The split factor L enters the honest condition's constant linearly, so absorbing L = r+1 into the assembly's C(d) is free.

4. Reading the anchor's clauses at a smaller constant

theorem Algsuperdiff.Section4.Provider.Proportion.anchorRegime_shrink {C0 Ca cs s ep gamma : ℝ} (hC00 : 0 < C0) (hle : C0 ≤ Ca) (hreg : gamma ≤ Ca⁻¹ * min (cs ^ 10) (cs ^ 2 * s ^ 5 * ep ^ 2)) : gamma ≤ C0⁻¹ * cs ^ 10

The anchor's regime, read at a smaller constant and without the min. The min of the frozen regime clause is only ever used through its first branch.

theorem Algsuperdiff.Section4.Provider.Proportion.anchorLevel_weaken {C0 Ca cs s ep theta gamma : ℝ} (hC00 : 0 < C0) (hle : C0 ≤ Ca) (hs0 : 0 < s) (hs12 : s ≤ 1 / 2) (hg0 : 0 < gamma) (hlevel : Ca * cs⁻¹ ^ 2 * s⁻¹ ^ 6 * ep⁻¹ ^ 2 * gamma ≤ theta) : C0 * cs⁻¹ ^ 2 * s⁻¹ ^ 4 * ep⁻¹ ^ 2 * gamma ≤ theta

The s⁻⁶ level clause implies the printed s⁻⁴ one, at a smaller constant. Two powers of s⁻¹ are thrown away and the constant is lowered; both directions are the easy ones, because s ≤ ½ makes s⁻¹ ≥ 1.

theorem Algsuperdiff.Section4.Provider.Proportion.anchorNumerator_le {cs s ep theta : ℝ} {n : ℕ} (hcs0 : 0 < cs) (hcs32 : cs ≤ 3 / 2) (hs0 : 0 < s) (hs12 : s ≤ 1 / 2) (hep0 : 0 < ep) (hep12 : ep ≤ 1 / 2) (htheta0 : 0 < theta) (htheta12 : theta ≤ 1 / 2) : cs ^ 2 * s ^ n * ep ^ 2 * theta ≤ 9 / 4

The numerator of the printed rate is bounded on the printed parameter window. On c⋆ ≤ 3/2, s, ε, θ ≤ ½ one has c⋆²sⁿε²θ ≤ 9/4 for every n, which is what makes the 𝒢₀ lane's rate ceiling c₁γ ≤ 1 non-binding at the anchor's parameters.