Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Stream.CutoffSecondMoment

CutoffSecondMoment #

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

The pointwise second moment of the stream matrix k_m #

ABK26 computes, in the proof of e.km.kn.L2.bound,

⨍ j_k(x) : j_{k'}(x) dx = 0 in expectation for k ≠ k'

from independence and mean zero, and then sums the diagonal terms with the exact normalization E[‖j_k(x)‖_F²] = c⁺ (log 3) 3^{2γk} of ShellSecondMoment. This module carries out that computation and then sends n → -∞, which is how the source obtains the estimates for k_m itself ("note that we can obtain estimates for k_m by sending n → -∞").

Route for the infinite-sum/expectation interchange #

The lower-infinite sum is exchanged with the expectation by dominated convergence, not by a bare tsum manipulation. On the public carrier CutoffSample the proved envelope cutoffLocalControl ell m dominates every entry of every finite lower truncation and of the limit (abs_cutoff_entry_le_cutoffLocalControl), and all of its natural moments are finite (integrable_cutoffLocalControl_pow). Hence (d²) · (cutoffLocalControl ell m)² is an integrable dominating function for the whole approximating sequence, and no new carrier A is required.

Main results #

References #

Pointwise algebra of the Frobenius mass #

source
theorem Algsuperdiff.Section3.Provider.Stream.matrixFrobeniusNormSq_le_of_abs_entry_le {d : ℕ} {A : HCPolySupport.Mat d} {C : ℝ} (h : ∀ (i l : Fin d), |A i l| ≤ C) :
HCPolySupport.Book.Ch02.matrixFrobeniusNormSq A ≤ ↑d ^ 2 * C ^ 2

A uniform entry bound gives a Frobenius mass bound.

Measurability helpers #

The pairwise Frobenius pairing of two shells #

source
def Algsuperdiff.Section3.Provider.Stream.shellPairing {d : ℕ} (x : HCPolySupport.Vec d) (k k' : ℤ) (omega : Cutoff.ShellSeq d) :
ℝ

The Frobenius pairing j_k(x) : j_{k'}(x) as a real observable.

Equations
Instances For

    The finite orthogonal expansion #

    source
    theorem Algsuperdiff.Section3.Provider.Stream.integral_frobeniusMass_shellFinsetSum {d : ℕ} (M : ABKModel d) (s : Finset ℤ) (x : HCPolySupport.Vec d) :
    ∫ (omega : Cutoff.ShellSeq d), HCPolySupport.Book.Ch02.matrixFrobeniusNormSq (∑ k ∈ s, (↑(omega k)).1 x) ∂↑M.P = ∑ k ∈ s, 3 ^ (2 * M.gamma * ↑k) * (Disorder.cstarPlus M * Real.log 3)

    The exact second moment of a finite sum of shells at one point: independence and mean zero kill every off-diagonal term, and the diagonal is summed by the c⁺ normalization. This is the deterministic content of the first two lines of ABK26's e.km.kn.L2.bound computation.

    source
    theorem Algsuperdiff.Section3.Provider.Stream.integral_frobeniusMass_finiteShellIncrement {d : ℕ} (M : ABKModel d) (n m : ℤ) (x : HCPolySupport.Vec d) :
    ∫ (omega : Cutoff.ShellSeq d), HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.finiteShellIncrement omega n m).toFun x) ∂↑M.P = ∑ k ∈ Finset.Ioc n m, 3 ^ (2 * M.gamma * ↑k) * (Disorder.cstarPlus M * Real.log 3)

    ABK26's exact second moment for the stream increment k_m - k_n.

    Transport to the public cutoff carrier #

    source
    theorem Algsuperdiff.Section3.Provider.Stream.integral_cutoffSampleLaw_comp_val {d : ℕ} (M : ABKModel d) {f : Cutoff.ShellSeq d → ℝ} (hf : Measurable f) :
    ∫ (omega : Cutoff.CutoffSample d), f ↑omega ∂↑(Cutoff.cutoffSampleLaw M) = ∫ (omega : Cutoff.ShellSeq d), f omega ∂↑M.P

    Integrals of shell-sequence observables are unchanged by the passage to the full-measure cutoff carrier.

    The lower-infinite limit #

    source
    theorem Algsuperdiff.Section3.Provider.Stream.exists_mem_openCubeSet_originCube {d : ℕ} (x : HCPolySupport.Vec d) :
    ∃ (ell : ℤ), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)

    Every point of ℝ^d lies in some origin-centred open triadic cube.

    This restates the private helper exists_mem_openOriginCube of Section3/Cutoff/Limit.lean, which is not exported; the proof is the same elementary Archimedean argument.

    source
    theorem Algsuperdiff.Section3.Provider.Stream.integral_frobeniusMass_cutoff {d : ℕ} (M : ABKModel d) (m : ℤ) (x : HCPolySupport.Vec d) :
    ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x) ∂↑(Cutoff.cutoffSampleLaw M) = Disorder.cstarPlus M * Kgamma M.gamma / 2 * 3 ^ (2 * M.gamma * ↑m)

    ABK26's stream second moment at a single point, obtained from the finite increments by sending n → -∞:

    E[ ‖k_m(x)‖_F² ] = c⁺ K_γ 3^{2γm} / 2.

    The interchange of the lower-infinite sum with the expectation is by dominated convergence against d² (cutoffLocalControl ell m)².