CutoffFrobeniusMass

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

Per-cube Frobenius masses of finite and genuine cutoffs

This module packages the volume-normalized squared Frobenius mass of a finite lower truncation and of the genuine lower-infinite cutoff on an arbitrary triadic cube. Both observables use the public CutoffSample carrier. The finite observable reads its underlying shell sequence through omega.1, so finite and limiting random variables have literally the same carrier.

For a fixed sample, the finite masses converge to the genuine mass. The canonical origin cover cubeOriginCoverScale Q puts every arbitrary cube in an origin-centred cube on which the proved lower-tail control applies. That control bounds every truncation, so spatial dominated convergence requires no extra containment or boundedness hypothesis.

Source and correction

• ABK26, obtains estimates for the genuine stream by sending the finite lower cutoff to minus infinity.
• ABK26, expands the volume-normalized squared Frobenius mass of finite stream increments.
• No disorder normalization constant occurs in the definitions or the deterministic convergence theorem below.

Main results

• finiteLowerCutoffFrobeniusMass and cutoffFrobeniusMass are the two per-cube observables on CutoffSample.
• cutoffFrobeniusMass_nonneg records the sign of the second.
• measurable_cutoffFrobeniusMass and stronglyMeasurable_setIntegral_cutoffFrobeniusMass make it available to the probabilistic consumers.
• tendsto_finiteLowerCutoffFrobeniusMass is pointwise convergence on every triadic cube.

noncomputable def Algsuperdiff.Section3.Provider.Stream.finiteLowerCutoffFrobeniusMass {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (q : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The volume-normalized squared Frobenius mass of a finite lower cutoff on an arbitrary triadic cube.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMass {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The volume-normalized squared Frobenius mass of the genuine lower-infinite cutoff on an arbitrary triadic cube.

Equations

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

theorem Algsuperdiff.Section3.Provider.Stream.cutoffFrobeniusMass_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffFrobeniusMass Q m omega

The genuine cutoff has nonnegative per-cube Frobenius mass.

theorem Algsuperdiff.Section3.Provider.Stream.measurable_cutoffFrobeniusMass {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) : Measurable fun (omega : Cutoff.CutoffSample d) => cutoffFrobeniusMass Q m omega

The genuine per-cube Frobenius mass is measurable on the public cutoff sample carrier.

theorem Algsuperdiff.Section3.Provider.Stream.tendsto_finiteLowerCutoffFrobeniusMass {d : ℕ} (Q : HCPolySupport.TriadicCube d) (m : ℤ) (omega : Cutoff.CutoffSample d) : Filter.Tendsto (fun (q : ℕ) => finiteLowerCutoffFrobeniusMass Q m q omega) Filter.atTop (nhds (cutoffFrobeniusMass Q m omega))

On every triadic cube and for every cutoff sample, the finite lower truncation masses converge to the genuine cutoff mass.