ShellSecondMoment

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

The exact second moment of a single shell

ABK26 uses, in the proof of its stream L² displays, the non-degeneracy normalization

⨍_{cu_l} j_k(x) : j_k(x) dx = c⁺ (log 3) 3^{2γk} + O_{Γ₁}(...),

whose deterministic part is the pointwise identity

E[ ‖j_k(x)‖_F² ] = 3^{2γk} c⁺ log 3 for every x ∈ ℝ^d.

This module proves that identity together with the integrability and mean-zero statements it rests on. Here c⁺ is Algsuperdiff.Section3.Disorder.cstarPlus, characterized by originFrobeniusMass M = c⁺ log 3 with originFrobeniusMass M = E[‖j_0(0)‖_F²].

The proof is the source's: the frozen marginal scaling law e.diff.law.shift (ShellLawPrefix.marginal_scaling) turns shell k at x into 3^{γk} j_0(3^{-k} x), the frozen (J1) stationarity moves the base point 3^{-k} x to the origin, and the resulting expectation is by definition originFrobeniusMass. No independence is used here.

Main results

• map_shellFrobeniusMass_eq: the exact law transport for the shell Frobenius mass.
• integral_shellFrobeniusMass: E[‖j_k(x)‖_F²] = 3^{2γk} c⁺ log 3.
• integrable_shellFrobeniusMass: its integrability.
• integral_shell_entry_at_point_eq_zero: (J1) mean zero, transported to shell k and an arbitrary base point. (Provider/Stream/TranslatedTransport.lean proves the same statement under the name integral_shell_entry_eq_zero; the two are interchangeable.)
• memLp_two_shell_entry: every scalar entry of a shell value lies in L².

References

• ABK26, e.km.L2.expectation.
• ABK26, e.km.kn.L2.bound.
• ABK26 ((J4) and the non-degeneracy constant).

Elementary Frobenius facts

theorem Algsuperdiff.Section3.Provider.Stream.sq_entry_le_matrixFrobeniusNormSq {d : ℕ} (A : HCPolySupport.Mat d) (i l : Fin d) : A i l ^ 2 ≤ HCPolySupport.Book.Ch02.matrixFrobeniusNormSq A

Each squared entry is dominated by the full Frobenius mass.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_shellFrobeniusMass {d : ℕ} (x : HCPolySupport.Vec d) : Measurable fun (j : Frozen.Assumptions.ShellField d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑j).1 x)

The Frobenius mass of a shell value at a fixed point is a measurable observable of the shell.

Law transport for the shell Frobenius mass

theorem Algsuperdiff.Section3.Provider.Stream.map_shellFrobeniusMass_eq {d : ℕ} (M : ABKModel d) (k : ℤ) (x : HCPolySupport.Vec d) : MeasureTheory.Measure.map (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑(omega k)).1 x)) ↑M.P = MeasureTheory.Measure.map (fun (j : Frozen.Assumptions.ShellField d) => 3 ^ (2 * M.gamma * ↑k) * HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑j).1 0)) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

The law of the shell-k Frobenius mass at any point x equals the law of 3^{2γk} times the zero-shell Frobenius mass at the origin. This combines the frozen marginal scaling law with the frozen (J1) stationarity.

The zero-shell Frobenius mass

theorem Algsuperdiff.Section3.Provider.Stream.integrable_zeroShellFrobeniusMass {d : ℕ} (M : ABKModel d) : MeasureTheory.Integrable (fun (j : Frozen.Assumptions.ShellField d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑j).1 0)) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

The zero-shell Frobenius mass at the origin is integrable, by the frozen (J2) Gaussian tail.

theorem Algsuperdiff.Section3.Provider.Stream.integral_zeroShellFrobeniusMass {d : ℕ} (M : ABKModel d) : ∫ (j : Frozen.Assumptions.ShellField d), HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑j).1 0) ∂↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) = Disorder.cstarPlus M * Real.log 3

The zero-shell Frobenius mass at the origin is exactly c⁺ log 3.

The shell second moment

theorem Algsuperdiff.Section3.Provider.Stream.integrable_shellFrobeniusMass {d : ℕ} (M : ABKModel d) (k : ℤ) (x : HCPolySupport.Vec d) : MeasureTheory.Integrable (fun (omega : Cutoff.ShellSeq d) => HCPolySupport.Book.Ch02.matrixFrobeniusNormSq ((↑(omega k)).1 x)) ↑M.P

The Frobenius mass of shell k at a point is integrable.

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

The exact shell second-moment identity behind ABK26's non-degeneracy normalization: for every scale k and every point x,

E[ ‖j_k(x)‖_F² ] = 3^{2γk} c⁺ log 3.

Mean zero away from the origin

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

ABK26's "j_k is mean zero" at an arbitrary base point and an arbitrary scale. This is the frozen (J1) mean-zero field, transported through the frozen marginal scaling law.

Duplication note: Algsuperdiff.Section3.Provider.Stream.integral_shell_entry_eq_zero, in Provider/Stream/TranslatedTransport.lean, is the same statement with the same proof. A distinct name is used here so that both files can coexist.

theorem Algsuperdiff.Section3.Provider.Stream.memLp_two_shell_entry {d : ℕ} (M : ABKModel d) (k : ℤ) (x : HCPolySupport.Vec d) (i l : Fin d) : MeasureTheory.MemLp (fun (omega : Cutoff.ShellSeq d) => (↑(omega k)).1 x i l) 2 ↑M.P

Every scalar entry of a shell value lies in L²: this is the exact second-moment bound supplied by integrable_shellFrobeniusMass.