IncrementLinftyNorm

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

Exact stream-increment Linfinity norm

This module defines the literal pointwise supremum of the matrix operator norm of a finite stream increment on an origin cube. It then transports the already-proved measurable small- and large-cube envelopes to that exact norm.

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

The literal L∞ norm of k_m-k_n on the open origin cube cu_l, with a zero member adjoined so the defining supremum is nonempty and nonnegative.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_finiteShellIncrement_le_streamIncrementLinftyNorm {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) ≤ streamIncrementLinftyNorm l n m omega

The literal norm dominates every point value on its defining cube.

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

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

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLinftyNorm_eq_localCubeControl {d : ℕ} (l n m : ℤ) (omega : Cutoff.ShellSeq d) : streamIncrementLinftyNorm l n m omega = Cutoff.localCubeControl l (shellIncrement omega n m)

The direct open-cube supremum is exactly the already-measurable local control of the genuine shell-field increment.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_streamIncrementLinftyNorm {d : ℕ} (l n m : ℤ) : Measurable fun (omega : Cutoff.ShellSeq d) => streamIncrementLinftyNorm l n m omega

The literal stream-increment supremum is a measurable random variable on the canonical shell-sequence carrier.

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

Exact small-cube squared-norm transport from the proved measurable envelope.

theorem Algsuperdiff.Section3.Provider.Stream.streamIncrementLinftyNorm_sq_isBigOWith_largeCube {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) => streamIncrementLinftyNorm l n m omega ^ 2) (largeCubeLinftyConst d * (↑l - ↑n) * min M.gamma⁻¹ (↑m - ↑n) * 3 ^ (2 * M.gamma * ↑m))

Exact large-cube squared-norm transport from the proved covering envelope.

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

The exact small-cube squared norm satisfies the Appendix-literal one-sided Orlicz relation, including measurability and positive scale.

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

The exact large-cube squared norm satisfies the Appendix-literal one-sided Orlicz relation, including measurability and positive scale.