Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Stream.CutoffL2Expectation

CutoffL2Expectation #

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

ABK26's e.km.L2.expectation #

The source display (ABK26) is

| E[ ‖k_m‖²_{L²(cu_l)} ] − ½ c⁺ γ⁻¹ 3^{2γm} | ≤ 2 c⁺ 3^{2γm} for every l ∈ ℤ.

Here ‖k_m‖²_{L²(cu_l)} is the volume-normalized square ⨍_{cu_l} ‖k_m(x)‖_F² dx, represented by Book.Ch02.average (Book.Ch02.cubeDomain (originCube d l)) of x ↦ matrixFrobeniusNormSq (cutoff m ω x), and c⁺ is the Frobenius origin-mass constant Algsuperdiff.Section3.Disorder.cstarPlus, normalized by E[‖j_0(0)‖_F²] = c⁺ log 3. This is the constant that the source's non-degeneracy input ⨍ j_k : j_k = c⁺ (log 3) 3^{2γk} refers to.

The proof is exactly the source's: the pointwise second moment is constant in x (integral_frobeniusMass_cutoff), so Fubini turns the cube average into that constant, and Kgamma_bounds (e.K.cgamma.ineq, 0 ≤ K_γ − γ⁻¹ ≤ 4) converts c⁺ K_γ 3^{2γm} / 2 into the source's ½ c⁺ γ⁻¹ 3^{2γm} with the stated error 2 c⁺ 3^{2γm}.

Main results #

References #

Measurability of the cutoff Frobenius mass #

source
theorem Algsuperdiff.Section3.Provider.Stream.measurable_frobeniusMass_cutoff {d : ℕ} (m : ℤ) (x : HCPolySupport.Vec d) :
Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x)

The Frobenius mass of the genuine cutoff at a fixed point is measurable in the sample.

source
theorem Algsuperdiff.Section3.Provider.Stream.continuous_frobeniusMass_cutoff {d : ℕ} (m : ℤ) (omega : Cutoff.CutoffSample d) :
Continuous fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x)

The Frobenius mass of the genuine cutoff is continuous in the point.

source
theorem Algsuperdiff.Section3.Provider.Stream.measurable_uncurry_frobeniusMass_cutoff {d : ℕ} (m : ℤ) :
Measurable (Function.uncurry fun (x : HCPolySupport.Vec d) (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x))

Carathéodory joint measurability of the cutoff Frobenius mass in the point and the sample: it is continuous in the point and measurable in the sample.

Pointwise integrability #

source
theorem Algsuperdiff.Section3.Provider.Stream.integrable_frobeniusMass_cutoff {d : ℕ} (M : ABKModel d) (ell m : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) :
MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.cutoff m omega).toFun x)) ↑(Cutoff.cutoffSampleLaw M)

The Frobenius mass of the genuine cutoff at a point of an origin cube is integrable, being dominated by the proved cutoff envelope of that cube.

The cube average #

source
theorem Algsuperdiff.Section3.Provider.Stream.integral_average_frobeniusMass_cutoff {d : ℕ} (M : ABKModel d) (l m : ℤ) :
∫ (omega : Cutoff.CutoffSample d), HCPolySupport.Book.Ch02.average (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d l)) fun (x : HCPolySupport.Vec 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)

The exact expectation of the volume-normalized L² mass of k_m on any origin cube. Since the pointwise second moment is independent of the base point, Fubini reduces the cube average to that constant.

The increment mean term of e.km.kn.L2.bound #

source
theorem Algsuperdiff.Section3.Provider.Stream.continuous_frobeniusMass_finiteShellIncrement {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) :
Continuous fun (x : HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.finiteShellIncrement omega n m).toFun x)

The Frobenius mass of a finite stream increment is continuous in the point.

source
theorem Algsuperdiff.Section3.Provider.Stream.measurable_frobeniusMass_finiteShellIncrement {d : ℕ} (n m : ℤ) (x : HCPolySupport.Vec d) :
Measurable fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.finiteShellIncrement omega n m).toFun x)

The Frobenius mass of a finite stream increment at a fixed point is measurable in the sample.

source
theorem Algsuperdiff.Section3.Provider.Stream.measurable_uncurry_frobeniusMass_finiteShellIncrement {d : ℕ} (n m : ℤ) :
Measurable (Function.uncurry fun (x : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.finiteShellIncrement omega n m).toFun x))

Carathéodory joint measurability for the finite stream increment.

source
theorem Algsuperdiff.Section3.Provider.Stream.integrable_frobeniusMass_finiteShellIncrement {d : ℕ} (M : ABKModel d) (n m : ℤ) (x : HCPolySupport.Vec d) :
MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((Cutoff.finiteShellIncrement omega n m).toFun x)) ↑M.P

The Frobenius mass of a finite stream increment is integrable: it is a finite sum of squares of L² shell entries.

source
theorem Algsuperdiff.Section3.Provider.Stream.integral_average_frobeniusMass_finiteShellIncrement {d : ℕ} (M : ABKModel d) (l n m : ℤ) :
∫ (omega : Cutoff.ShellSeq d), HCPolySupport.Book.Ch02.average (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d l)) fun (x : HCPolySupport.Vec 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)

The exact expectation of the volume-normalized L² mass of the stream increment k_m - k_n on any origin cube. This is the deterministic main term of ABK26's e.km.kn.L2.bound; the source's remaining O_{Γ₁} term is a fluctuation statement, not part of this expectation.