DDecomposition

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

The D-decomposition of l.minimal.scale.sep

ABK26, §4.2. The proof of l.minimal.scale.sep opens by applying p.mathcalE.annular.decomp and taking a square root:

sup_{L ≥ k} 𝓔_{s,∞,2}(□_k; a_L − (k_L − k_k)_{□_k}, σ_k) · 1_{𝒢(k;s,1)}
  ≤ C (D₁(k) + D₂(k) + D₃(k) + c⋆^{−2}s^{−1}γ|log γ|²)

with the three groups. The remainder is then absorbed into the lemma's own envelope and the obligation becomes e.kick.Dees.Dees.

What the square root actually does

The anchor Algsuperdiff.Frozen.Section4.annular_decomposition states its clause (i) for the squared supremum, with four right-hand groups. Taking a square root of a four-term sum costs √(a+b+c+e) ≤ √a+√b+√c+√e, and each group loses a square in a different way:

• the 𝐣-Hessian group loses its inner square by ∑ aᵢ² ≤ (∑ aᵢ)² and its outer 3^{−½s(k−n)} halves to 3^{−¼s(k−n)}.

Every one of these steps is performed in ℝ≥0∞, where √(∑ b²) ≤ ∑ b needs no summability side condition at all: the four helpers tsum_sq_le_sq_tsum, sum_sq_le_sq_sum, iSup_sq_le_sq_iSup and sq_add_four_le are unconditional, and the "square root" is taken by comparing squares (ENNReal.pow_le_pow_left_iff) rather than by forming a root. This is why no analogue of the real-valued annular_sqrt_domination's hsum hypothesis appears anywhere below.

Deviations from the printed text

• The remainder's s-exponent is s^{−3/2}, not the printed s^{−1}. The printed §4.2 remainder c⋆^{−2}s^{−1}γ|log γ|² is the exact square root of the printed §4.1 second group C s^{−2}c⋆^{−4}γ²|log γ|⁴; the anchor carries C s^{−3}c⋆^{−4}γ²|log γ|⁴, one power of s weaker, which is precisely the cost of the missing annulus multiplicity. Its square root is s^{−3/2}.
• Every statement below carries the window s ∈ [8γ, 1/4] verbatim.
• The good event of the display is 𝒢(k;s,1) = goodEventBase M Ccg k s 1, while the anchor's clause (i) is gated by 𝒢₀(k) ∩ 𝒢₁(k;s,√c⋆ γ^{−1/2}) only (resolution A6b). goodEventBase_subset_anchorEvent proves the inclusion — the only input is s ≤ 1, because the composed event's 𝒢₁ threshold carries the extra factor s·ε = s.
• D₁ carries the indicator 1_{𝒢(k;s,1)} inside, exactly as printed; D₂, D₃ and the remainder do not, exactly as printed.

Main definitions

• annularHalfSum — the halved-exponent annular ℓ¹ sum.
• dOne, dTwo, dThree — the three groups D₁(k), D₂(k), D₃(k), in ℝ≥0∞.
• dRemainder — the deterministic remainder, in ℝ (honest s^{−3/2}).

Main results

• exists_dDecomposition — the √-split of the anchor's clause (i): the D-decomposition.
• dRemainder_le_envelope —: the remainder is below the lemma's own envelope c⋆^{−1}s^{−7/2}√γ in the printed regime γ ≤ C^{−10}c⋆^{10}. The smallness is D, never assumed.
• exists_dDecomposition_absorbed — the two composed: the decomposition with the remainder already replaced by the envelope, i.e. the reduction of the display to the obligation e.kick.Dees.Dees.

References

• ABK26, l.minimal.scale.sep; p.mathcalE.annular.decomp.

1. The unconditional ℓ² ↪ ℓ¹ layer in ℝ≥0∞

Four elementary facts. In ℝ≥0∞ each of them is unconditional: there is no summability hypothesis, because an ℝ≥0∞ sum always exists, and the degenerate case ∑ = ∞ makes every statement trivially true.

theorem Algsuperdiff.Section4.Provider.MinimalScale.tsum_sq_le_sq_tsum {iota : Type u_1} (f : iota → ENNReal) : ∑' (i : iota), f i ^ 2 ≤ (∑' (i : iota), f i) ^ 2

∑' (f i)² ≤ (∑' f i)² in ℝ≥0∞ — the ℓ² ↪ ℓ¹ inequality, with no summability side condition.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sum_sq_le_sq_sum {iota : Type u_1} (S : Finset iota) (f : iota → ENNReal) : ∑ i ∈ S, f i ^ 2 ≤ (∑ i ∈ S, f i) ^ 2

The Finset companion of tsum_sq_le_sq_tsum.

theorem Algsuperdiff.Section4.Provider.MinimalScale.iSup_sq_le_sq_iSup {iota : Type u_1} (f : iota → ENNReal) : ⨆ (i : iota), f i ^ 2 ≤ (⨆ (i : iota), f i) ^ 2

The supremum companion: a supremum of squares is below the square of the supremum.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sq_add_four_le (a b c e : ENNReal) : a ^ 2 + b ^ 2 + c ^ 2 + e ^ 2 ≤ (a + b + c + e) ^ 2

The four-term square root, in the form the decomposition uses: the sum of four squares is below the square of the sum.

2. Weight arithmetic

theorem Algsuperdiff.Section4.Provider.MinimalScale.three_rpow_sq (y : ℝ) : Real.rpow 3 y ^ 2 = Real.rpow 3 (2 * y)

(3^y)² = 3^{2y} — the exponent halving of the annular weights.

theorem Algsuperdiff.Section4.Provider.MinimalScale.three_rpow_nonneg (y : ℝ) : 0 ≤ Real.rpow 3 y

theorem Algsuperdiff.Section4.Provider.MinimalScale.ofReal_three_rpow_half_sq (s x : ℝ) : ENNReal.ofReal (Real.rpow 3 (-(1 / 2) * s * x)) ^ 2 = ENNReal.ofReal (Real.rpow 3 (-s * x))

The squared halved weight is the anchor's weight, in ℝ≥0∞.

theorem Algsuperdiff.Section4.Provider.MinimalScale.ofReal_three_rpow_quarter_sq (s x : ℝ) : ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * s * x)) ^ 2 = ENNReal.ofReal (Real.rpow 3 (-(1 / 2) * s * x))

The squared quarter weight is the anchor's half weight, in ℝ≥0∞.

3. The three groups D₁, D₂, D₃ and the remainder

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.annularHalfSum {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The halved-exponent annular ℓ¹ sum. The anchor's annular group with the exponent −s(k−n) halved to −½s(k−n) and the square removed from the lattice maximum.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.dOne {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (s : { s : ℝ // 0 < s }) (k : ℤ) : Section3.Cutoff.CutoffSample d → ENNReal

D₁(k), with the indicator of 𝒢(k;s,1) inside exactly as printed.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.dTwo {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) : Section3.Cutoff.CutoffSample d → ENNReal

D₂(k): c⋆^{−1/2}s^{−1}γ^{1/2} ∑_{l ≥ k} 3^{(2−γ)k}‖∇𝐣_l‖_{W^{1,∞}(□_k)}.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.dThree {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) : Section3.Cutoff.CutoffSample d → ENNReal

D₃(k): c⋆^{−1/2}s^{−1}γ^{1/2} ∑_{l ≤ k} 3^{−¼s(k−l)} ∑_{i=l−1}^{k} 3^{(2−γ)i} max_{z ∈ 3^iℤ^d ∩ □_k} ‖𝐣_i‖_{W^{2,∞}(z+□_i)}.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.dRemainder {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : ℝ

The deterministic remainder c⋆^{−2}s^{−3/2}γ|log γ|², the square root of the anchor's second group. The printed §4.2 exponent is s^{−1}; see the module docstring.

Equations

• Algsuperdiff.Section4.Provider.MinimalScale.dRemainder M s = (Algsuperdiff.Section3.Disorder.cstar M)⁻¹ ^ 2 * (√↑s ^ 3)⁻¹ * M.gamma * |Real.log M.gamma| ^ 2

theorem Algsuperdiff.Section4.Provider.MinimalScale.dRemainder_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) : 0 ≤ dRemainder M s

4. The event inclusion

theorem Algsuperdiff.Section4.Provider.MinimalScale.goodEventBase_subset_anchorEvent {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (k : ℤ) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) : Support.goodEventBase M Ccg k s 1 ⊆ Support.eventG0 M Ccg k ∩ Support.eventG1 M k (↑s) (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)

𝒢(k;s,1) ⊆ 𝒢₀(k) ∩ 𝒢₁(k;s,√c⋆ γ^{−1/2}) — the gate of the anchor's clause (i) (resolution A6b). The composed good event reads 𝒢₁ at the threshold s·ε·√c⋆ γ^{−1/2}, which at ε = 1 and s ≤ 1 is below the anchor's.

5. The √-split of the anchor's clause (i)

theorem Algsuperdiff.Section4.Provider.MinimalScale.anchor_annular_le_sq {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ∑' (j : { j : ℤ // j ≤ k }) (n : { n : ℤ // n ≤ ↑j - 1 }), ENNReal.ofReal (Real.rpow 3 (-↑s * ↑(k - ↑n))) * ⨆ (v : ↑(Support.latticeAnnulusSet d (↑n) (↑j) (↑j - 1))), ENNReal.ofReal (Support.annularErrorObservable M (↑n) s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint ↑n ↑v) omega) ^ 2) ≤ annularHalfSum M s k omega ^ 2

The anchor's annular group is below the square of the halved-exponent sum.

theorem Algsuperdiff.Section4.Provider.MinimalScale.anchor_hessian_le_sq {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ∑' (n : { n : ℤ // n ≤ k }), ENNReal.ofReal (Real.rpow 3 (-(1 / 2) * ↑s * ↑(k - ↑n))) * ∑ i ∈ Finset.Icc (↑n - 1) k, (ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑i)) * ⨆ (v : ↑(Support.latticeCubeSet d i k)), ENNReal.ofReal (Support.shellW2InfNormAt (Support.triadicLatticePoint i ↑v) i (↑omega i))) ^ 2 ≤ (∑' (n : { n : ℤ // n ≤ k }), ENNReal.ofReal (Real.rpow 3 (-(1 / 4) * ↑s * ↑(k - ↑n))) * ∑ i ∈ Finset.Icc (↑n - 1) k, ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑i)) * ⨆ (v : ↑(Support.latticeCubeSet d i k)), ENNReal.ofReal (Support.shellW2InfNormAt (Support.triadicLatticePoint i ↑v) i (↑omega i))) ^ 2

The anchor's Hessian group is below the square of the quarter-exponent sum.

6. The real prefactor algebra of the four square roots

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_le_one_add {x : ℝ} (hx : 0 ≤ x) : √x ≤ 1 + x

√x ≤ 1 + x — the one comparison that lets the output constant 1 + C of the decomposition dominate the anchor's √C.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_mul_sqrt_sq {C x : ℝ} (hC : 0 ≤ C) (hx : 0 ≤ x) : (√C * √x) ^ 2 = C * x

The annular prefactor squared: (√C·√s)² = C·s.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_mul_pref_sq {C cs sv gam : ℝ} (hC : 0 ≤ C) (hcs : 0 < cs) (hgam : 0 ≤ gam) : (√C * ((√cs)⁻¹ * sv⁻¹ * √gam)) ^ 2 = C * sv⁻¹ ^ 2 * cs⁻¹ * gam

The 𝐣-group prefactor squared: (√C·c⋆^{−1/2}s^{−1}√γ)² = C s^{−2}c⋆^{−1}γ.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_mul_remainder_sq {C cs sv gam lg : ℝ} (hC : 0 ≤ C) (hsv : 0 < sv) : (√C * (cs⁻¹ ^ 2 * (√sv ^ 3)⁻¹ * gam * |lg| ^ 2)) ^ 2 = C * sv⁻¹ ^ 3 * cs⁻¹ ^ 4 * gam ^ 2 * |lg| ^ 4

The remainder prefactor squared: the square of √C·c⋆^{−2}s^{−3/2}γ|log γ|² is the anchor's second group C s^{−3}c⋆^{−4}γ²|log γ|⁴.

7. THE D-D

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_dDecomposition (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≤ ↑s → ↑s ≤ 1 / 4 → ∀ (k : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (Support.goodEventBase M (Support.cgEllipLowerConstant d) k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ ENNReal.ofReal C * (dOne M (Support.cgEllipLowerConstant d) s k omega + dTwo M s k omega + dThree M s k omega + ENNReal.ofReal (dRemainder M s))

THE D-D OF l.minimal.scale.sep.

There is a dimensional constant C such that, in the printed regime γ ≤ C^{−10}c⋆^{10} and on the window s ∈ [8γ, 1/4], for every scale k and almost every sample,

sup_{L ≥ k} 𝓔_{s,∞,2}(□_k; a_L − (k_L − k_k)_{□_k}, σ_k) · 1_{𝒢(k;s,1)}
  ≤ C (D₁(k) + D₂(k) + D₃(k) + c⋆^{−2}s^{−3/2}γ|log γ|²) .

The three groups are the printed ones at the halved geometric exponents; the remainder's exponent is s^{−3/2} rather than the printed s^{−1} because the anchor carries the annulus multiplicity (see the module docstring).

Hypotheses. Exactly the premises of the anchor annular_decomposition, which are the kicking lemma's own premises with the window s ≤ 1/4 in place of the printed 1/2. No summability, no measurability and no finiteness hypothesis: the whole ℓ² ↪ ℓ¹ step happens in ℝ≥0∞.

8. The remainder absorption

theorem Algsuperdiff.Section4.Provider.MinimalScale.sqrt_mul_log_sq_le_cstar {d : ℕ} (M : Section3.ABKModel d) {C : ℝ} (hC : 64 ≤ C) (hreg : M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10) (hgam1 : M.gamma ≤ 1) : √M.gamma * Real.log M.gamma ^ 2 ≤ Section3.Disorder.cstar M

The smallness of √γ (log γ)², D from the printed regime. From γ ≤ C^{−10}c⋆^{10} with C ≥ 64 and the standing c⋆ ≤ 3/2 (never c⋆ ≤ 1, which the frozen tail does not deliver) one gets √γ (log γ)² ≤ c⋆. The transcendental content is the proved sqrt_mul_log_sq_le_quarter; everything else is a comparison of fourth powers.

theorem Algsuperdiff.Section4.Provider.MinimalScale.dRemainder_le_envelope {d : ℕ} (M : Section3.ABKModel d) {C : ℝ} (hC : 64 ≤ C) (hreg : M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) (hgam1 : M.gamma ≤ 1) : dRemainder M s ≤ (Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma

The remainder absorption. The deterministic remainder of the D-decomposition is below the kicking lemma's own envelope c⋆^{−1}s^{−7/2}√γ, at the printed regime γ ≤ C^{−10}c⋆^{10} and with NO smallness hypothesis: the smallness is derived by sqrt_mul_log_sq_le_cstar.

s^{−7/2} = ((√s)⁷)⁻¹, so no rpow appears.

9. The reduced obligation e.kick.Dees.Dees

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_dDecomposition_absorbed (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≤ ↑s → ↑s ≤ 1 / 4 → ∀ (k : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (Support.goodEventBase M (Support.cgEllipLowerConstant d) k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ ENNReal.ofReal C * (dOne M (Support.cgEllipLowerConstant d) s k omega + dTwo M s k omega + dThree M s k omega + ENNReal.ofReal ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma))

The D-decomposition with the remainder absorbed. The deterministic remainder of exists_dDecomposition is replaced by the kicking lemma's own envelope c⋆^{−1}s^{−7/2}√γ, so that the only remaining obligation is the one the manuscript labels e.kick.Dees.Dees: a bound for the Cesàro average of `D₁

• D₂ + D₃`.

The smallness needed for the absorption is derived from the printed regime γ ≤ C^{−10}c⋆^{10} (via sqrt_mul_log_sq_le_cstar), never assumed; the standing c⋆ ≤ 3/2 is used in place of the unavailable c⋆ ≤ 1.