LargeCubeLinfty

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

The large-cube L∞ bound: ABK26's e.km.kn.Linfty

ABK26 upgrades the small-cube estimate e.km.kn.Linfty.smallcube to the large cube cu_l: for n < m ≤ l,

‖k_m - k_n‖²_{L∞(cu_l)} ≤ O_{Γ₁}(C (l-n) min{γ^{-1}, m-n} 3^{2γm}),

by covering cu_l with translated copies of the small cube and applying the maximum lemma l.maximums.Gamma.s, which costs the amplitude factor (log N)^{1/2} with N the number of copies.

As in the small-cube layer, the statement is split into a deterministic part and a probabilistic part, because the finite increment k_m - k_n = ∑_{k ∈ (n,m]} j_k is not itself a shell and so carries no localCubeControl gauge.

• matrixOperatorNorm_finiteShellIncrement_le_largeCubeSupBound is the deterministic part: at every point of cu_l the increment is dominated by the single random variable largeCubeSupBound l n m, the maximum of the translated small-cube bounds over the covering family.
• isBigOWith_gammaSigma_one_largeCubeSupBound_sq is the source display for the square of that random variable.

Composing the two gives the source display for every realization: the left-hand side of e.km.kn.Linfty is the essential supremum over cu_l of the squared matrix norm of the increment, which is at most largeCubeSupBound l n m ^ 2 pointwise on cu_l.

The covering family is explicit: the shifts are the lattice points of 3^{n-1} ℤ^d with coordinates bounded by 3^{(l-n+1)^+}, and each translated open cube has scale n. Rounding each coordinate to the nearest lattice point moves it by at most 3^{n-1}/2 < 3^n/2, so the translated open cubes really do cover the whole of cu_l, with no boundary exception. The count is N = (2·3^{l-n+1} + 1)^d, so log N ≤ 3 d (l-n) log 3, which is the source's (l-n) factor with an explicit dimensional constant.

Deviations from the source, all absorbed by its C(d):

• the covering lattice has spacing 3^{n-1} rather than 3^n, which is what makes the open cover exact; this multiplies N by 3^d and is absorbed by the constant;
• the amplitude factor is (3 max{1, log N})^{1/2} rather than (log N)^{1/2}, from the proved cardinality-free maximum lemma.

Main definitions

• Algsuperdiff.Section3.Provider.Stream.translatedIncrementSupBound
• Algsuperdiff.Section3.Provider.Stream.subcubeShifts
• Algsuperdiff.Section3.Provider.Stream.largeCubeSupBound
• Algsuperdiff.Section3.Provider.Stream.largeCubeLinftyConst

Main results

Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_largeCubeSupBound

• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeSupBound
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_one_largeCubeSupBound_sq

References

• ABK26, e.km.kn.Linfty.
• ABK26, e.km.kn.Linfty.smallcube.
• ABK26, Lemma l.maximums.Gamma.s.

The stream increment at an arbitrary base point

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_incrementAt_entry {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (z : HCPolySupport.Vec d) (i l : Fin d) : HCPolySupport.IndependentSums.IsBigO (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => ∑ k ∈ Finset.Ioc n m, (↑(omega k)).1 z i l) (geometricConcentrationConst * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))

ABK26's e.k.ell.upscales, entrywise at an arbitrary base point z: for n < m and every matrix entry,

∑_{k = n+1}^m j_k(z)_{il} = O_{Γ₂}(C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}),

with an amplitude that does not depend on z.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_incrementAt {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun z)) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * (↑d ^ 2 * (geometricConcentrationConst * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))))

ABK26's e.k.ell.upscales at an arbitrary base point z:

|(k_m - k_n)(z)| ≤ O_{Γ₂}(C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}),

with |·| the exact Euclidean matrix operator norm. This is the translated form of isBigOWith_gammaSigma_originIncrement; the amplitude is the same, which is where the stationarity half of (J1) enters through isBigO_gammaSigma_shell_entry.

The small-cube bound on a translated cube

noncomputable def Algsuperdiff.Section3.Provider.Stream.translateShellSeq {d : ℕ} (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : Cutoff.ShellSeq d

The shell sequence translated by a fixed vector.

Equations

• Algsuperdiff.Section3.Provider.Stream.translateShellSeq z omega k = Algsuperdiff.Frozen.Assumptions.ShellField.translate z (omega k)

noncomputable def Algsuperdiff.Section3.Provider.Stream.translatedIncrementSupBound {d : ℕ} (z : HCPolySupport.Vec d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : ℝ

The random variable dominating ‖k_m - k_n‖_{L∞(z + cu_n)}: the small-cube bound incrementSupBound of the translated shell sequence.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.finiteShellIncrement_translateShellSeq {d : ℕ} (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) (n m : ℤ) (x : HCPolySupport.Vec d) : (Cutoff.finiteShellIncrement (translateShellSeq z omega) n m).toFun x = (Cutoff.finiteShellIncrement omega n m).toFun (x + z)

Translating the shell sequence translates the finite stream increment.

theorem Algsuperdiff.Section3.Provider.Stream.translatedIncrementSupBound_eq {d : ℕ} (z : HCPolySupport.Vec d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : translatedIncrementSupBound z n m omega = HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun z) + ↑d ^ 2 * √↑d * (3 ^ n / 2) * ∑ k ∈ Finset.Ioc n m, localCubeDerivNorm n (Frozen.Assumptions.ShellField.translate z (omega k))

The explicit form of the translated small-cube bound: the increment value at the base point z plus the geometric factor times the summed first-derivative gauges on the translated cube.

theorem Algsuperdiff.Section3.Provider.Stream.incrementSupBound_nonneg {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ incrementSupBound n m omega

The small-cube bound is nonnegative.

theorem Algsuperdiff.Section3.Provider.Stream.translatedIncrementSupBound_nonneg {d : ℕ} (z : HCPolySupport.Vec d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ translatedIncrementSupBound z n m omega

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_translatedIncrementSupBound {d : ℕ} (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) (n m : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.translateSet z (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun x) ≤ translatedIncrementSupBound z n m omega

The deterministic half of ABK26's e.k.ell.upscales.infty on a translated cube: at every point of z + cu_n the finite stream increment is dominated by translatedIncrementSupBound z n m.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_matrixOperatorNorm_finiteShellIncrement {d : ℕ} (n m : ℤ) (z : HCPolySupport.Vec d) : Measurable fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun z)

The value of the finite stream increment at a fixed point is a measurable random variable.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_translatedIncrementSupBound {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (translatedIncrementSupBound z n m) (streamLinftyConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))

The probabilistic half of ABK26's e.k.ell.upscales.infty on a translated cube, at the same amplitude as at the origin.

A finite cover of the large cube by translated small cubes

def Algsuperdiff.Section3.Provider.Stream.subcubeRadius (n l : ℤ) : ℕ

The per-coordinate lattice radius of the covering family: the shifts range over the lattice 3^{n-1} ℤ^d with integer coordinates bounded by 3^{(l-n+1)^+}.

Equations

• Algsuperdiff.Section3.Provider.Stream.subcubeRadius n l = 3 ^ (l - n + 1).toNat

def Algsuperdiff.Section3.Provider.Stream.subcubeShifts (d : ℕ) (n l : ℤ) : Finset (Fin d → ℤ)

The finite index set of lattice shifts covering cu_l by translates of cu_n.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Stream.subcubeCenter {d : ℕ} (n : ℤ) (p : Fin d → ℤ) : HCPolySupport.Vec d

The lattice point of 3^{n-1} ℤ^d attached to an index.

Equations

• Algsuperdiff.Section3.Provider.Stream.subcubeCenter n p i = 3 ^ (n - 1) * ↑(p i)

theorem Algsuperdiff.Section3.Provider.Stream.subcubeShifts_nonempty (d : ℕ) (n l : ℤ) : (subcubeShifts d n l).Nonempty

theorem Algsuperdiff.Section3.Provider.Stream.card_subcubeShifts (d : ℕ) (n l : ℤ) : (subcubeShifts d n l).card = (2 * subcubeRadius n l + 1) ^ d

theorem Algsuperdiff.Section3.Provider.Stream.exists_subcubeShift_mem {d : ℕ} (n l : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d l)) : ∃ p ∈ subcubeShifts d n l, x ∈ HCPolySupport.translateSet (subcubeCenter n p) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))

The covering property: every point of the open cube cu_l lies in one of the translated open cubes z + cu_n of the family. Rounding each coordinate to the nearest point of the lattice 3^{n-1} ℤ^d moves it by at most 3^{n-1}/2, which is strictly less than the half-side 3^n/2, so the open cubes already cover cu_l.

The maximum over the cover

noncomputable def Algsuperdiff.Section3.Provider.Stream.largeCubeSupBound {d : ℕ} (l n m : ℤ) (omega : Cutoff.ShellSeq d) : ℝ

The single random variable dominating ‖k_m - k_n‖_{L∞(cu_l)}: the maximum of the translated small-cube bounds over the covering family.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.largeCubeSupBound_nonneg {d : ℕ} (l n m : ℤ) (omega : Cutoff.ShellSeq d) : 0 ≤ largeCubeSupBound l n m omega

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_largeCubeSupBound {d : ℕ} (omega : Cutoff.ShellSeq d) (l n m : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d l)) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((Cutoff.finiteShellIncrement omega n m).toFun x) ≤ largeCubeSupBound l n m omega

The deterministic half of ABK26's e.km.kn.Linfty: at every point of cu_l the finite stream increment is dominated by largeCubeSupBound l n m.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeSupBound {d : ℕ} (M : ABKModel d) {l n m : ℤ} (hnm : n < m) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (largeCubeSupBound l n m) ((3 * max 1 (Real.log ↑(subcubeShifts d n l).card)) ^ 2⁻¹ * (streamLinftyConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m)))

The maximum over the cover, with the amplitude factor supplied by the proved cardinality-free maximum lemma.

The source display

noncomputable def Algsuperdiff.Section3.Provider.Stream.largeCubeLogConst : ℝ

The universal factor produced by the maximum over the cover.

Equations

• Algsuperdiff.Section3.Provider.Stream.largeCubeLogConst = 3 * (1 + 3 * Real.log 3)

noncomputable def Algsuperdiff.Section3.Provider.Stream.largeCubeLinftyConst (d : ℕ) : ℝ

The explicit dimensional constant of ABK26's e.km.kn.Linfty.

Equations

• Algsuperdiff.Section3.Provider.Stream.largeCubeLinftyConst d = Algsuperdiff.Section3.Provider.Stream.largeCubeLogConst * ↑d * Algsuperdiff.Section3.Provider.Stream.streamLinftyConst d ^ 2

theorem Algsuperdiff.Section3.Provider.Stream.largeCubeLogConst_pos : 0 < largeCubeLogConst

theorem Algsuperdiff.Section3.Provider.Stream.largeCubeLinftyConst_pos {d : ℕ} (hd : 0 < d) : 0 < largeCubeLinftyConst d

theorem Algsuperdiff.Section3.Provider.Stream.three_mul_max_one_log_card_subcubeShifts_le (d : ℕ) {n l : ℤ} (hd : 1 ≤ d) (hnl : n < l) : 3 * max 1 (Real.log ↑(subcubeShifts d n l).card) ≤ largeCubeLogConst * ↑d * (↑l - ↑n)

The count of the covering family is (2·3^{l-n+1} + 1)^d, so the amplitude factor of the maximum lemma is at most C(d) (l-n). This is the source's (l-n) factor, with an explicit dimensional constant.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_one_largeCubeSupBound_sq {d : ℕ} (M : ABKModel d) {l n m : ℤ} (hnm : n < m) (hml : m ≤ l) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.ShellSeq d) => largeCubeSupBound l n m omega ^ 2) (largeCubeLinftyConst d * (↑l - ↑n) * min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m))

ABK26's e.km.kn.Linfty:

‖k_m - k_n‖²_{L∞(cu_l)} ≤ O_{Γ₁}(C (l-n) min{γ^{-1}, m-n} 3^{2γm}).

The left-hand side is represented, as in the proved small-cube layer, by the random variable largeCubeSupBound l n m, which dominates the matrix operator norm of k_m - k_n at every point of cu_l by matrixOperatorNorm_finiteShellIncrement_le_largeCubeSupBound. The tail exponent moves from σ = 2 to σ = 1 through the proved power rule e.powerofGammasigma at p = 2, exactly as in the small-cube display.