G1AtomTails

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

The 𝒢₁ per-shell atom tails

ABK26's l.ratio.of.good.scales.for.k bounds the density of scales at which the event 𝒢₁(m; s, T) of d.good.event.for.lambda fails. Its two lanes feed the concentration proposition with two families of atoms:

• large waves (Step 1) X_k = 3^{(2-γ)k} ‖∇j_k‖_{W^{1,∞}(□_k)}, whose Γ₂ moment bound is e.G1scalecount.Xk.pedant.bound;
• small waves (Step 2) 3^{(2-γ)k} ‖j_k‖_{W^{2,∞}(z+□_k)} at a lattice centre z, whose squares carry the Γ₁ moment bound e.Xmk.pedant.bound.

This module produces both tails, uniformly in the shell index k and (for the second family) in the real centre z.

Where the tails come from, and the dimension bookkeeping the source omits

Here the cancellation is explicit and exact: the proved Section 3 realizations of the manuscript's own per-shell displays are

• e.jk.O isBigOWith_gammaSigma_localCubeControl_shell: ‖j_k‖_{L∞(□_k)} ≤ 𝒪_{Γ₂}(3^{γk}),

both with amplitude constant 1. Multiplying by 3^{(1-γ)k} and 3^{-γk} respectively makes both amplitudes 1, uniformly in k — which is exactly what the Appendix-D array of p.concentration.for.scales needs.

The anchor Algsuperdiff.Frozen.Section3.stream_derivative_sum_bound gives the same derivative statement at the one-shell window (l, n, m) = (k, k-1, k), at the strictly larger amplitude C · min(γ^{-1}, 1) · 3^{(γ-1)k}; it carries no Γ₂ statement for the value leg (its L^∞ clauses are stated for the square at Γ₁). The per-shell displays above are the manuscript's own cited inputs, so they are what is consumed here.

Carriers

The Section 3 displays live on Cutoff.ShellSeq d under M.P, while the Section 4 events live on Cutoff.CutoffSample d under Cutoff.cutoffSampleLaw. The transfer is the proved isBigOWith_cutoffSampleLaw_comp_val (the inclusion Subtype.val is a measurable embedding preserving the mass of every subset). The lattice centre is reached by isBigOWith_comp_translateCutoffSample, the proved real-translation invariance of the cutoff-sample law; no lattice restriction is used, so the per-centre tail holds at every z : Vec d.

References

• ABK26, d.good.event.for.lambda.
• ABK26, l.ratio.of.good.scales.for.k.
• ABK26, (e.jk.O, e.nabla.jk.O), (the gauges).

1. Reading one shell of a cutoff sample

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_shellCoord {d : ℕ} (k : ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => ↑omega k

The k-th shell of a cutoff sample, as a measurable map.

2. The two exponent identities

The manuscript's 3^{(2-γ)k} splits against the two proved amplitudes. Both identities are pure rpow arithmetic and are isolated so that no numeric tactic ever sees a transcendental atom.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_add_three (x y : ℝ) : Real.rpow 3 (x + y) = Real.rpow 3 x * Real.rpow 3 y

Real.rpow-form of the exponent addition law at base 3, stated so that rw matches the explicit Real.rpow spelling used throughout this file.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_intCast_three (k : ℤ) : Real.rpow 3 ↑k = 3 ^ k

Real.rpow-form of the integer-exponent identification at base 3.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_zero_three : Real.rpow 3 0 = 1

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_nonneg_three (x : ℝ) : 0 ≤ Real.rpow 3 x

Nonnegativity of Real.rpow 3, in the explicit Real.rpow spelling.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_pos_three (x : ℝ) : 0 < Real.rpow 3 x

Positivity of Real.rpow 3, in the explicit Real.rpow spelling.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_le_rpow_three {x y : ℝ} (h : x ≤ y) : Real.rpow 3 x ≤ Real.rpow 3 y

Monotonicity of Real.rpow 3 in the exponent, in the explicit spelling.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_def_three (y : ℝ) : Real.rpow 3 y = Real.exp (Real.log 3 * y)

The exponential form of Real.rpow 3, in the explicit spelling.

theorem Algsuperdiff.Section4.Provider.Proportion.rpow_neg_three (y : ℝ) : Real.rpow 3 (-y) = (Real.rpow 3 y)⁻¹

The negative-exponent law for Real.rpow 3, in the explicit spelling.

3. The deterministic gauge dominations

theorem Algsuperdiff.Section4.Provider.Proportion.three_rpow_mul_shellW1InfGradNorm_le {d : ℕ} (gamma : ℝ) (k : ℤ) (j : Frozen.Assumptions.ShellField d) : Real.rpow 3 ((2 - gamma) * ↑k) * Support.shellW1InfGradNorm k j ≤ Real.rpow 3 ((1 - gamma) * ↑k) * (Section3.Provider.Stream.localCubeDerivNorm k j + 3 ^ k * Section3.Provider.Stream.localCubeSecondDerivNorm k j)

The large-waves atom is dominated by the e.nabla.jk.O gauge. The volume-normalized gauge is a maximum of two legs, so it is below their sum, and the weight 3^{(2-γ)k} splits as 3^{(1-γ)k}·3^{k} — the exact form of the cancellation the source performs silently.

noncomputable def Algsuperdiff.Section4.Provider.Proportion.w2Gauge {d : ℕ} (k : ℤ) (j : Frozen.Assumptions.ShellField d) : ℝ

The ‖·‖_{W^{2,∞}(□_k)} gauge measured at the origin cube: the maximum of the first-order gauge and the normalized value leg. shellW2InfNormAt z k is this gauge applied to the translated field, by definition.

Equations

• Algsuperdiff.Section4.Provider.Proportion.w2Gauge k j = max (Algsuperdiff.Section4.Support.shellW1InfGradNorm k j) (3 ^ (-2 * k) * Algsuperdiff.Section3.Cutoff.localCubeControl k j)

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_w2Gauge {d : ℕ} (k : ℤ) : Measurable (w2Gauge k)

theorem Algsuperdiff.Section4.Provider.Proportion.three_rpow_mul_w2Gauge_le {d : ℕ} (gamma : ℝ) (k : ℤ) (j : Frozen.Assumptions.ShellField d) : Real.rpow 3 ((2 - gamma) * ↑k) * w2Gauge k j ≤ Real.rpow 3 ((1 - gamma) * ↑k) * (Section3.Provider.Stream.localCubeDerivNorm k j + 3 ^ k * Section3.Provider.Stream.localCubeSecondDerivNorm k j) + Real.rpow 3 (-(gamma * ↑k)) * Section3.Cutoff.localCubeControl k j

The small-waves atom is dominated by the sum of the two 𝒪_{Γ₂} gauges. The W^{2,∞} gauge is a maximum of three legs; the two derivative legs are the e.nabla.jk.O gauge at weight 3^{(1-γ)k} and the value leg is e.jk.O at weight 3^{-γk}.

4. The two normalized shell observables and their Γ₂ tails

Both are stated on Cutoff.ShellSeq d first (that is where the Section 3 displays live) and then transferred.

noncomputable def Algsuperdiff.Section4.Provider.Proportion.derivLeg {d : ℕ} (gamma : ℝ) (k : ℤ) (omega : Section3.Cutoff.ShellSeq d) : ℝ

The e.nabla.jk.O gauge at the shell's own scale, weighted so that its amplitude is 1.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Proportion.valueLeg {d : ℕ} (gamma : ℝ) (k : ℤ) (omega : Section3.Cutoff.ShellSeq d) : ℝ

The e.jk.O value leg, weighted so that its amplitude is 1.

Equations

• Algsuperdiff.Section4.Provider.Proportion.valueLeg gamma k omega = Real.rpow 3 (-(gamma * ↑k)) * Algsuperdiff.Section3.Cutoff.localCubeControl k (omega k)

5. The large-waves atom X_k

noncomputable def Algsuperdiff.Section4.Provider.Proportion.atomG1a {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The large-waves atom: X_k = 3^{(2-γ)k} ‖∇j_k‖_{W^{1,∞}(□_k)}, the score field of 𝒢₁'s first condition read at its own scale.

Equations

• Algsuperdiff.Section4.Provider.Proportion.atomG1a M k omega = Real.rpow 3 ((2 - M.gamma) * ↑k) * Algsuperdiff.Section4.Support.shellW1InfGradNorm k (↑omega k)

theorem Algsuperdiff.Section4.Provider.Proportion.atomG1a_nonneg {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ atomG1a M k omega

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_atomG1a {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) : Measurable (atomG1a M k)

theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_atomG1a {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (atomG1a M k) 1

e.G1scalecount.Xk.pedant.bound, in tail form. The large-waves atom has a Γ₂ upper tail at amplitude 1, uniformly in the shell index k. Only the manuscript's own per-shell display e.nabla.jk.O enters.

6. The small-waves atom at a real centre

noncomputable def Algsuperdiff.Section4.Provider.Proportion.atomG1bScale : ℝ

The Γ₂ amplitude of the small-waves atom: the two-term triangle constant against the two unit amplitudes of e.nabla.jk.O and e.jk.O.

Equations

• Algsuperdiff.Section4.Provider.Proportion.atomG1bScale = HCPolySupport.IndependentSums.gammaTriangleConst 2 * 2

theorem Algsuperdiff.Section4.Provider.Proportion.atomG1bScale_pos : 0 < atomG1bScale

noncomputable def Algsuperdiff.Section4.Provider.Proportion.atomG1b {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The small-waves atom, before squaring: 3^{(2-γ)k} ‖j_k‖_{W^{2,∞}(z+□_k)} at the centre z.

Equations

• Algsuperdiff.Section4.Provider.Proportion.atomG1b M k z omega = Real.rpow 3 ((2 - M.gamma) * ↑k) * Algsuperdiff.Section4.Support.shellW2InfNormAt z k (↑omega k)

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_atomG1b {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (z : HCPolySupport.Vec d) : Measurable (atomG1b M k z)

theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_atomG1b {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (atomG1b M k z) atomG1bScale

e.Xmk.pedant.bound, in tail form, before the squaring and the lattice maximum. The small-waves atom has a Γ₂ upper tail at the amplitude atomG1bScale, uniformly in the shell index k and in the real centre z. Uniformity in z is the proved real-translation invariance of the cutoff-sample law; no lattice restriction enters.