IncrementLinfty

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

The small-cube L∞ stream bound: ABK26's e.k.ell.upscales.infty

ABK26 upgrades the value estimate at the origin to a uniform estimate on the whole cube cu_n:

‖k_m - k_n‖_{L∞(cu_n)} ≤ √d 3^n ‖∇(k_m - k_n)‖_{L∞(cu_n)} + |(k_m - k_n)(0)| ≤ O_{Γ₂}(C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}),

which is the source's e.km.kn.Linfty.smallcube before squaring.

As in Algsuperdiff.Section3.Provider.Stream.IncrementDerivativeBounds, 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_incrementSupBound is the deterministic mean-value bridge: at every point of cu_n the increment is dominated by the single random variable incrementSupBound n m, built from the value at the origin and the summed first-derivative gauges.
• isBigOWith_gammaSigma_incrementSupBound is the probabilistic estimate for that random variable, at the source amplitude.

Composing the two gives the source display for every realization.

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

• the mean value theorem is applied to each of the d² matrix entries along the segment from 0 to x, and the entries are recombined through matrixOperatorNorm ≤ matrixOperatorNorm(centre) + ∑_{i,l} |·|; this costs a factor d² relative to the source's direct matrix-norm argument;
• the geometric factor is √d · 3^n / 2 rather than the source's √d · 3^n, because cu_n has half-side 3^n/2; this is a strengthening.

Main definitions

• Algsuperdiff.Section3.Provider.Stream.incrementSupBound

Main results

Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_incrementSupBound

• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_incrementSupBound

References

• ABK26, e.k.ell.upscales.infty.
• ABK26, e.km.kn.Linfty.smallcube.

Scaling of the exact Euclidean norms

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_smul_real {d : ℕ} (c : ℝ) (A : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.matrixOperatorNorm (c • A) = |c| * HCPolySupport.Book.Ch02.matrixOperatorNorm A

The exact Euclidean matrix operator norm is absolutely homogeneous.

theorem Algsuperdiff.Section3.Provider.Stream.vecNorm_smul_real {d : ℕ} (c : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm (c • x) = |c| * HCPolySupport.Book.Ch02.vecNorm x

The exact Euclidean vector norm is absolutely homogeneous.

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_apply_le_matrixDerivativeNorm_mul_vecNorm {d : ℕ} (D : Frozen.Assumptions.ShellField.MatrixDerivative d) (v : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.matrixOperatorNorm (D v) ≤ Frozen.Assumptions.ShellField.matrixDerivativeNorm D * HCPolySupport.Book.Ch02.vecNorm v

The exact induced first-derivative norm controls the matrix values at every input, with the Euclidean vector norm of the input as the factor.

Geometry of the origin cube

theorem Algsuperdiff.Section3.Provider.Stream.smul_mem_openCubeSet_originCube {d : ℕ} {n : ℤ} {x : HCPolySupport.Vec d} {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) : t • x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d n)

The origin cube is star-shaped about the origin.

theorem Algsuperdiff.Section3.Provider.Stream.vecNorm_le_of_mem_openCubeSet_originCube {d : ℕ} {n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) : HCPolySupport.Book.Ch02.vecNorm x ≤ √↑d * (3 ^ n / 2)

Points of the origin cube of scale n have Euclidean norm at most √d 3^n / 2.

The mean-value bridge

theorem Algsuperdiff.Section3.Provider.Stream.finiteShellIncrement_eq_sum {d : ℕ} (omega : Cutoff.ShellSeq d) (n m : ℤ) (x : HCPolySupport.Vec d) : (Cutoff.finiteShellIncrement omega n m).toFun x = ∑ k ∈ Finset.Ioc n m, (↑(omega k)).1 x

The finite stream increment evaluates to the finite sum of shell values.

theorem Algsuperdiff.Section3.Provider.Stream.abs_entry_sum_sub_origin_le {d : ℕ} (omega : Cutoff.ShellSeq d) (n m : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) (i l : Fin d) : |(∑ k ∈ Finset.Ioc n m, (↑(omega k)).1 x) i l - (∑ k ∈ Finset.Ioc n m, (↑(omega k)).1 0) i l| ≤ (∑ k ∈ Finset.Ioc n m, localCubeDerivNorm n (omega k)) * HCPolySupport.Book.Ch02.vecNorm x

The mean value theorem along the segment from the origin, applied to a single matrix entry of the finite stream increment.

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

The single random variable dominating ‖k_m - k_n‖_{L∞(cu_n)}: the value at the origin plus the geometric factor times the summed first-derivative gauges.

Equations

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

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

The deterministic half of ABK26's e.k.ell.upscales.infty: at every point of cu_n the finite stream increment is dominated by incrementSupBound.

The probabilistic estimate

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

The explicit dimensional constant of ABK26's e.k.ell.upscales.infty.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_shellDerivNormSum_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)) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * 3 ^ ((M.gamma - 1) * ↑n))

The summed first-derivative gauge estimate, with the second-derivative term discarded.

theorem Algsuperdiff.Section3.Provider.Stream.zpow_mul_rpow_gamma_sub_one (gamma : ℝ) (n : ℤ) : 3 ^ n * 3 ^ ((gamma - 1) * ↑n) = 3 ^ (gamma * ↑n)

Reassembling the geometric factor: 3^n · 3^{(γ-1)n} = 3^{γn}.

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_add_of_isBigO {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X Y : Omega → ℝ} {A B sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 < A) (hB : 0 < B) (hX : HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigma) X A) (hY : HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigma) Y B) (hXm : Measurable X) (hYm : Measurable Y) : HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Omega) => X omega + Y omega) (HCPolySupport.IndependentSums.gammaTriangleConst sigma * (A + B))

Two-term generalized triangle inequality for Γ_σ tails.

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

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

theorem Algsuperdiff.Section3.Provider.Stream.rpow_gamma_mul_le_min_mul {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) : 3 ^ (M.gamma * ↑n) ≤ min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m)

The lower-scale amplitude 3^{γn} is dominated by the source amplitude.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_streamEnvelope {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) {X D : Cutoff.ShellSeq d → ℝ} (hX0 : ∀ (omega : Cutoff.ShellSeq d), 0 ≤ X omega) (hD0 : ∀ (omega : Cutoff.ShellSeq d), 0 ≤ D omega) (hXm : Measurable X) (hDm : Measurable D) (hX : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) X (HCPolySupport.IndependentSums.gammaTriangleConst 2 * (↑d ^ 2 * (geometricConcentrationConst * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))))) (hD : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) D (HCPolySupport.IndependentSums.gammaTriangleConst 2 * 3 ^ ((M.gamma - 1) * ↑n))) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => X omega + ↑d ^ 2 * √↑d * (3 ^ n / 2) * D omega) (streamLinftyConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))

Combine measurable value and derivative envelopes at the stream scale.

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

The probabilistic half of ABK26's e.k.ell.upscales.infty:

incrementSupBound ≤ O_{Γ₂}(C(d) min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}).

Combined with matrixOperatorNorm_finiteShellIncrement_le_incrementSupBound, this is the source's ‖k_m - k_n‖_{L∞(cu_n)} ≤ O_{Γ₂}(C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}), that is, e.km.kn.Linfty.smallcube before squaring.

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

ABK26's e.km.kn.Linfty.smallcube:

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

This is the square of isBigOWith_gammaSigma_incrementSupBound, obtained from the proved power rule e.powerofGammasigma at p = 2, which moves the tail exponent from σ = 2 to σ = 1.