LargeCubeW1Inf

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

The summed derivative-stream bound: ABK26's e.W.1.inf.bound

ABK26 states, for l, m, n ∈ ℤ with n ≤ min{m, l},

∑_{k = n+1}^m (3^k ‖∇j_k‖_{L∞(cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(cu_l)}) ≤ O_{Γ₂}(C (l-n)^{1/2} min{γ^{-1}, m-n} 3^{γm}).

The source proof has two regimes. For k < l the display e.W1inf.jL.bound.smaller covers cu_l by translates of cu_k and applies the maximum lemma l.maximums.Gamma.s to the single-shell derivative display e.nabla.jk.O, which costs the amplitude factor (log N)^{1/2} ≃ (l-k)^{1/2}. For k ≥ l the cube cu_l is contained in the own scale cube cu_k, so e.nabla.jk.O applies with no covering loss. The two regimes are then summed with the Γ₂ triangle inequality against the geometric series ∑_{k ∈ (n,m]} 3^{γk} ≤ C min{γ^{-1}, m-n} 3^{γm} (e.geo.part.sum).

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

• The covering family is the one proved for e.km.kn.Linfty (subcubeShifts), whose lattice spacing is 3^{k-1} rather than 3^k; this makes the open cover exact and multiplies the count by 3^d.
• The amplitude factor of the proved maximum lemma is (3 max{1, log N})^{1/2} rather than (log N)^{1/2}.
• Since the maximizing translate of the first-derivative norm need not be the maximizing translate of the second-derivative norm, the covering step is applied to each of the two gauges separately, costing a factor 2.
• The source hypothesis n ≤ l is not needed and is dropped: for l < n every shell in (n, m] is estimated in the own-scale regime and the corrected factor (1 ∨ (l-n))^{1/2} equals 1. The local proof is therefore strictly stronger than the (corrected) source statement on that side.

Main definitions

• Algsuperdiff.Section3.Provider.Stream.largeCubeDerivGauge: the source summand 3^k ‖∇j_k‖_{L∞(cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(cu_l)}.
• Algsuperdiff.Section3.Provider.Stream.shellDerivGaugeCover: the maximum of the translated own-scale derivative gauges over the covering family.

Main results

• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_lt: ABK26's e.W1inf.jL.bound.smaller.
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGaugeSum: ABK26's e.W.1.inf.bound, in its corrected form.

References

• ABK26, e.W.1.inf.bound.
• ABK26, e.W1inf.jL.bound.smaller.
• ABK26, e.nabla.jk.O.
• ABK26, l.maximums.Gamma.s.
• ABK26, e.geo.part.sum.

Elementary rewrites

The source summand

noncomputable def Algsuperdiff.Section3.Provider.Stream.largeCubeDerivGauge {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : ℝ

The summand of ABK26's e.W.1.inf.bound: 3^k ‖∇j_k‖_{L∞(cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(cu_l)}, read on the observation cube cu_l and at the shell index k.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.largeCubeDerivGauge_nonneg {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : 0 ≤ largeCubeDerivGauge l k j

theorem Algsuperdiff.Section3.Provider.Stream.measurable_largeCubeDerivGauge {d : ℕ} (l k : ℤ) : Measurable (largeCubeDerivGauge l k)

theorem Algsuperdiff.Section3.Provider.Stream.largeCubeDerivGauge_eq {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : largeCubeDerivGauge l k j = 3 ^ k * (localCubeDerivNorm l j + 3 ^ k * localCubeSecondDerivNorm l j)

The exact factorization of the summand through the own-scale gauge weight.

The covering maximum

noncomputable def Algsuperdiff.Section3.Provider.Stream.shellDerivGaugeCover {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : ℝ

The maximum, over the proved covering family of cu_l by translates of cu_k, of the translated own-scale derivative gauge ‖∇j‖_{L∞(z + cu_k)} + 3^k ‖∇²j‖_{L∞(z + cu_k)}.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.le_shellDerivGaugeCover {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) {p : Fin d → ℤ} (hp : p ∈ subcubeShifts d k l) : localCubeDerivNorm k (Frozen.Assumptions.ShellField.translate (subcubeCenter k p) j) + 3 ^ k * localCubeSecondDerivNorm k (Frozen.Assumptions.ShellField.translate (subcubeCenter k p) j) ≤ shellDerivGaugeCover l k j

theorem Algsuperdiff.Section3.Provider.Stream.shellDerivGaugeCover_nonneg {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : 0 ≤ shellDerivGaugeCover l k j

theorem Algsuperdiff.Section3.Provider.Stream.localCubeDerivNorm_le_shellDerivGaugeCover {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : localCubeDerivNorm l j ≤ shellDerivGaugeCover l k j

The covering bound for the first-derivative norm: every point of cu_l lies in one of the translated cubes z + cu_k, and the translated shell has the same derivative there.

theorem Algsuperdiff.Section3.Provider.Stream.three_zpow_mul_localCubeSecondDerivNorm_le_shellDerivGaugeCover {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : 3 ^ k * localCubeSecondDerivNorm l j ≤ shellDerivGaugeCover l k j

The covering bound for the weighted second-derivative norm.

theorem Algsuperdiff.Section3.Provider.Stream.largeCubeDerivGauge_le_two_mul_shellDerivGaugeCover {d : ℕ} (l k : ℤ) (j : Frozen.Assumptions.ShellField d) : largeCubeDerivGauge l k j ≤ 2 * 3 ^ k * shellDerivGaugeCover l k j

The deterministic half of e.W1inf.jL.bound.smaller: the source summand on cu_l is dominated by twice the weighted covering maximum.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivGaugeCover {d : ℕ} (M : ABKModel d) (l k : ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => shellDerivGaugeCover l k (omega k)) ((3 * max 1 (Real.log ↑(subcubeShifts d k l).card)) ^ 2⁻¹ * Real.rpow 3 ((M.gamma - 1) * ↑k))

The probabilistic half of e.W1inf.jL.bound.smaller: the covering maximum obeys the single-shell Γ₂ estimate e.nabla.jk.O with the amplitude factor supplied by the proved cardinality-free maximum lemma.

e.W1inf.jL.bound.smaller

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

The dimensional constant of ABK26's e.W1inf.jL.bound.smaller.

Equations

• Algsuperdiff.Section3.Provider.Stream.shellW1InfSmallerConst d = 2 * √(Algsuperdiff.Section3.Provider.Stream.largeCubeLogConst * ↑d)

theorem Algsuperdiff.Section3.Provider.Stream.shellW1InfSmallerConst_nonneg (d : ℕ) : 0 ≤ shellW1InfSmallerConst d

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge_lt {d : ℕ} (M : ABKModel d) {l k : ℤ} (hkl : k < l) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => largeCubeDerivGauge l k (omega k)) (shellW1InfSmallerConst d * √(↑l - ↑k) * 3 ^ (M.gamma * ↑k))

ABK26's e.W1inf.jL.bound.smaller: for k < l,

3^k ‖∇j_k‖_{L∞(cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(cu_l)} ≤ O_{Γ₂}(C (l-k)^{1/2} 3^{γk}),

with the explicit dimensional constant 2 √(largeCubeLogConst · d).

The uniform per-shell estimate

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

The dimensional constant covering both regimes of the source proof.

Equations

• Algsuperdiff.Section3.Provider.Stream.shellW1InfConst d = Algsuperdiff.Section3.Provider.Stream.shellW1InfSmallerConst d + 1

theorem Algsuperdiff.Section3.Provider.Stream.shellW1InfConst_pos (d : ℕ) : 0 < shellW1InfConst d

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGauge {d : ℕ} (M : ABKModel d) {l n k : ℤ} (hnk : n < k) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => largeCubeDerivGauge l k (omega k)) (shellW1InfConst d * √(max 1 (↑l - ↑n)) * 3 ^ (M.gamma * ↑k))

The per-shell estimate uniform in the two regimes of the source proof: for n < k the source summand on cu_l is O_{Γ₂}(C (1 ∨ (l-n))^{1/2} 3^{γk}).

For k < l this is e.W1inf.jL.bound.smaller together with l - k ≤ l - n; for l ≤ k it is e.nabla.jk.O on the smaller cube cu_l ⊆ cu_k, whose amplitude carries no covering factor at all.

e.W.1.inf.bound

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

The dimensional constant of ABK26's e.W.1.inf.bound.

Equations

• Algsuperdiff.Section3.Provider.Stream.streamW1InfSumConst d = HCPolySupport.IndependentSums.gammaTriangleConst 2 * Algsuperdiff.Section3.Provider.Stream.shellW1InfConst d * (7 / Real.log 3)

theorem Algsuperdiff.Section3.Provider.Stream.streamW1InfSumConst_pos (d : ℕ) : 0 < streamW1InfSumConst d

theorem Algsuperdiff.Section3.Provider.Stream.sum_Ioc_rpow_gamma_le {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n ≤ m) : ∑ k ∈ Finset.Ioc n m, 3 ^ (M.gamma * ↑k) ≤ 7 / Real.log 3 * min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (M.gamma * ↑m)

The geometric series of the source amplitudes: ∑_{k ∈ (n,m]} 3^{γk} ≤ (7 / log 3) min{γ^{-1}, m-n} 3^{γm}. This is e.geo.part.sum at the halved exponent.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_largeCubeDerivGaugeSum {d : ℕ} (M : ABKModel d) {l n m : ℤ} (hnm : n ≤ m) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => ∑ k ∈ Finset.Ioc n m, largeCubeDerivGauge l k (omega k)) (streamW1InfSumConst d * √(max 1 (↑l - ↑n)) * min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (M.gamma * ↑m))

ABK26's e.W.1.inf.bound, in its corrected form: for every n ≤ m,

∑_{k ∈ (n,m]} (3^k ‖∇j_k‖_{L∞(cu_l)} + 3^{2k} ‖∇²j_k‖_{L∞(cu_l)}) ≤ O_{Γ₂}(C (1 ∨ (l-n))^{1/2} min{γ^{-1}, m-n} 3^{γm}).

The source hypothesis n ≤ l is dropped: it is not needed, since for l < n every shell of the range is estimated on the cube cu_l ⊆ cu_k at its own scale.