OriginConcentration

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

The stream increment at the origin: ABK26's e.k.ell.upscales

This module proves the first display in the concentration part of ABK26's stream increment lemma: for n < m,

|(k_m - k_n)(0)| ≤ O_{Γ₂}(C (∑_{k = n+1}^m 3^{2γk})^{1/2}) ≤ O_{Γ₂}(C min{γ^{-1/2}, (m-n)^{1/2}} 3^{γm}).

Following the source, the input is: the value display e.jk.O (isBigOWith_gammaSigma_localCubeControl_shell), the independence of the shells (the frozen prefix field independent), that j_k(0) is mean zero (the frozen (J1) field mean_zero, transported to shell k through the frozen marginal scaling law), and the concentration proposition. The ℓ²-aggregated amplitude is supplied by Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_two_sum_Ioc_geometric.

Two deviations from the source display are recorded explicitly.

• The source works with the matrix-valued random variable j_k(0) directly. Here the concentration proposition is applied to each of the d² scalar entries, which are independent across k and mean zero, and the entries are recombined into matrixOperatorNorm through matrixOperatorNorm ≤ matrixFrobeniusNorm ≤ ∑_{i,l} |·_{il}| and the generalized triangle inequality. This costs the explicit dimensional factor Γ-triangle-constant · d², which is absorbed by the source's C(d).
• The amplitude is stated in the final min form of the source display; the intermediate ℓ² form (∑ 3^{2γk})^{1/2} is not produced, since the source itself immediately replaces it by the min form via e.geo.part.sum.

Main results

• Algsuperdiff.Section3.Provider.Stream.integral_shell_origin_entry_eq_zero
• Algsuperdiff.Section3.Provider.Stream.iIndepFun_shell_origin_entry
• Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_originIncrement_entry
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_originIncrement

References

• ABK26, e.k.ell.upscales.
• ABK26, e.jk.O.
• ABK26, Proposition p.concentration.

Matrix entries as continuous linear functionals

def Algsuperdiff.Section3.Provider.Stream.matrixEntryCLM {d : ℕ} (i l : Fin d) : HCPolySupport.Mat d →L[ℝ] ℝ

Evaluation of a matrix entry, as a continuous linear functional for the elementwise matrix norm carried by the frozen shell field.

Equations

• Algsuperdiff.Section3.Provider.Stream.matrixEntryCLM i l = (Matrix.entryLinearMap ℝ ℝ i l).mkContinuous 1 ⋯

@[simp]

theorem Algsuperdiff.Section3.Provider.Stream.matrixEntryCLM_apply {d : ℕ} (i l : Fin d) (A : HCPolySupport.Mat d) : (matrixEntryCLM i l) A = A i l

Mean zero at the origin

theorem Algsuperdiff.Section3.Provider.Stream.integral_shellObservable_eq {d : ℕ} (M : ABKModel d) (k : ℤ) (F : Frozen.Assumptions.ShellField d → ℝ) (hF : Measurable F) : ∫ (omega : Cutoff.ShellSeq d), F (omega k) ∂↑M.P = ∫ (j : Frozen.Assumptions.ShellField d), F (Frozen.Assumptions.ShellField.triadicScale M.gamma k j) ∂↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

Transport of an integral of a real shell observable through the frozen marginal scaling law: the law of F(j_k) is the law of F(3^{γk} j_0(3^{-k} ·)).

theorem Algsuperdiff.Section3.Provider.Stream.integral_zeroShell_entry_eq_zero {d : ℕ} (M : ABKModel d) (x : HCPolySupport.Vec d) (i l : Fin d) : ∫ (j : Frozen.Assumptions.ShellField d), (↑j).1 x i l ∂↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) = 0

The frozen (J1) mean-zero assumption, read entrywise under the zero-shell law.

theorem Algsuperdiff.Section3.Provider.Stream.integral_shell_origin_entry_eq_zero {d : ℕ} (M : ABKModel d) (k : ℤ) (i l : Fin d) : ∫ (omega : Cutoff.ShellSeq d), (↑(omega k)).1 0 i l ∂↑M.P = 0

ABK26's "j_k(0) is mean zero", for every shell index and every matrix entry. This is the frozen (J1) mean-zero field transported to shell k through the frozen marginal scaling law.

The per-shell tail and independence at the origin

theorem Algsuperdiff.Section3.Provider.Stream.zero_mem_openCubeSet_originCube {d : ℕ} (k : ℤ) : 0 ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d k)

The origin lies in every origin-centred triadic cube.

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_shell_origin_entry {d : ℕ} (M : ABKModel d) (k : ℤ) (i l : Fin d) : HCPolySupport.IndependentSums.IsBigO (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.ShellSeq d) => (↑(omega k)).1 0 i l) (3 ^ (M.gamma * ↑k))

ABK26's e.jk.O at the origin, entrywise: |j_k(0)_{il}| ≤ O_{Γ₂}(3^{γk}).

theorem Algsuperdiff.Section3.Provider.Stream.iIndepFun_shell_origin_entry {d : ℕ} (M : ABKModel d) (i l : Fin d) : ProbabilityTheory.iIndepFun (fun (k : ℤ) (omega : Cutoff.ShellSeq d) => (↑(omega k)).1 0 i l) ↑M.P

The frozen shell independence, read on the scalar entries of the shell values at the origin.

The entrywise concentration estimate

theorem Algsuperdiff.Section3.Provider.Stream.isBigO_gammaSigma_originIncrement_entry {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (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 0 i l) (geometricConcentrationConst * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))

ABK26's e.k.ell.upscales, entrywise: for n < m and every matrix entry,

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

Recombining the entries

theorem Algsuperdiff.Section3.Provider.Stream.matrixOperatorNorm_le_sum_univ_abs_entry {d : ℕ} (A : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.matrixOperatorNorm A ≤ ∑ p : Fin d × Fin d, |A p.1 p.2|

The exact Euclidean operator norm of a matrix is dominated by the sum of the absolute values of its entries, indexed by pairs.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_matrixOperatorNorm {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (hd : 0 < d) {X : Omega → HCPolySupport.Mat d} {A : ℝ} (hA : 0 < A) (hentry : ∀ (i l : Fin d), HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Omega) => X omega i l) A) (hmeas : ∀ (i l : Fin d), Measurable fun (omega : Omega) => X omega i l) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Omega) => HCPolySupport.Book.Ch02.matrixOperatorNorm (X omega)) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * (↑d ^ 2 * A))

Entrywise Gaussian concentration controls the exact matrix operator norm.

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

ABK26's e.k.ell.upscales:

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

with |·| the exact Euclidean matrix operator norm and k_m - k_n the finite shell increment ∑_{k = n+1}^m j_k. The dimensional constant is explicit: the source's C(d) is chosen as Γ-triangle-constant · d² times the universal constant geometricConcentrationConst, the extra d² coming from recombining the d² scalar entries.