IncrementDerivativeBounds

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

The stream-increment derivative bound of ABK26

This module proves ABK26's e.nabla.km.kn.infty: for n < m,

‖∇(k_m - k_n)‖_{L∞(cu_n)} + 3^n ‖∇²(k_m - k_n)‖_{L∞(cu_n)} ≤ O_{Γ₂}(^{(γ-1)n}).

Following the source, the proof sums the single-shell estimate e.nabla.jk.O over the shells k ∈ (n, m] with the generalized triangle inequality e.Gamma.sigma.triangle, and then evaluates the resulting geometric series.

Two components are supplied separately.

• The probabilistic content is isBigOWith_gammaSigma_shellDerivGaugeSum_Ioc: the finite sum ∑_{k ∈ (n,m]} (‖∇j_k‖_{L∞(cu_n)} + 3^n ‖∇²j_k‖_{L∞(cu_n)}) obeys the stated Γ₂ bound with the explicit constant Homogenization.IndependentSums.gammaTriangleConst 2 in place of the source's C.
• The deterministic content is matrixDerivativeNorm_sum_deriv_le_sum_localCubeDerivNorm and its second-derivative and combined analogues: the derivatives of the increment k_m - k_n = ∑_{k ∈ (n,m]} j_k are the corresponding finite sums of shell derivatives, and their exact induced norms are dominated pointwise on cu_n by the summed gauges. Composing the two gives the source display for any realization of the increment.

The geometric series is summed with the explicit constant 1: for γ ≤ 1/4 the ratio 3^{γ-1} is at most 3^{-3/4} ≤ 1/2, so ∑_{k ∈ (n,m]} 3^{(γ-1)k} ≤ 3^{(γ-1)n}.

References

• ABK26, e.nabla.km.kn.infty.
• ABK26, l.Gamma.sigma.triangle.

The decreasing geometric sum

theorem Algsuperdiff.Section3.Provider.Stream.rpow_three_gamma_sub_one_le_half {gamma : ℝ} (hquarter : gamma ≤ 1 / 4) : Real.rpow 3 (gamma - 1) ≤ 1 / 2

For γ ≤ 1/4 the geometric ratio of the derivative amplitudes is at most one half.

theorem Algsuperdiff.Section3.Provider.Stream.sum_Ioc_rpow_gamma_sub_one_le {gamma : ℝ} (hquarter : gamma ≤ 1 / 4) {n m : ℤ} (hnm : n ≤ m) : ∑ k ∈ Finset.Ioc n m, Real.rpow 3 ((gamma - 1) * ↑k) ≤ Real.rpow 3 ((gamma - 1) * ↑n)

The geometric sum appearing in ABK26's e.nabla.km.kn.infty. Since γ ≤ 1/4 forces the ratio 3^{γ-1} below one half, the sum over (n, m] is bounded by its formal continuation with constant 1.

The summed Γ₂ estimate

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivGaugeSum_Ioc {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => ∑ k ∈ Finset.Ioc n m, (localCubeDerivNorm n (omega k) + 3 ^ n * localCubeSecondDerivNorm n (omega k))) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * Real.rpow 3 ((M.gamma - 1) * ↑n))

ABK26's e.nabla.km.kn.infty in the form produced by the source proof: the finite sum over the shells k ∈ (n, m] of the derivative gauges on the small cube cu_n obeys a Γ₂ bound with amplitude 3^{(γ-1)n}. The constant is CoarseGraining's explicit triangle constant gammaTriangleConst 2, standing for the source's C.

The deterministic increment bridge

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_finset_sum_le {d : ℕ} (s : Finset ℤ) (D : ℤ → Frozen.Assumptions.ShellField.MatrixDerivative d) : Frozen.Assumptions.ShellField.matrixDerivativeNorm (∑ k ∈ s, D k) ≤ ∑ k ∈ s, Frozen.Assumptions.ShellField.matrixDerivativeNorm (D k)

The exact induced first-derivative norm is subadditive over finite sums.

theorem Algsuperdiff.Section3.Provider.Stream.matrixDerivativeNorm_sum_deriv_le_sum_localCubeDerivNorm {d : ℕ} (ell : ℤ) (s : Finset ℤ) (omega : Cutoff.ShellSeq d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : Frozen.Assumptions.ShellField.matrixDerivativeNorm (∑ k ∈ s, (omega k).deriv x) ≤ ∑ k ∈ s, localCubeDerivNorm ell (omega k)

The first derivative of a finite shell increment is dominated on cu_ell by the summed first-derivative gauges.