StoppedMomentsProcess

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

The coordinate decomposition of the squared displacement

The stopped second moment of StoppedMoments.lean is proved one observable at a time, and the second moment of the whole displacement is obtained by summing it over the coordinate directions. This file records the decomposition that sum rests on: the squared norm is the sum of the squares of the coordinate observables, both on the state space and, for observables cut off by a common factor, on its one-point carrier.

Main results

• sum_quadraticObservable_basisVec — the coordinate decomposition of the squared norm.
• onePointRealExtension_sum_quadraticObservable — the same on the one-point carrier, for the cut-off observables.

References

• ABK26, Steps 1 and 3 of the superdiffusive displacement bounds of Section 5.4.

theorem Algsuperdiff.Section5.Provider.sum_quadraticObservable_basisVec {d : ℕ} (y : HCPolySupport.Vec d) : ∑ i : Fin d, quadraticObservable (HCPolySupport.basisVec i) y = HCPolySupport.vecNormSq y

The squared norm is the sum of the squares of the coordinate observables.

theorem Algsuperdiff.Section5.Provider.onePointRealExtension_sum_quadraticObservable {d : ℕ} (c : HCPolySupport.Vec d → ℝ) (z : OnePoint (HCPolySupport.Vec d)) : ∑ i : Fin d, DivergenceFormProcess.Form.onePointRealExtension (fun (y : HCPolySupport.Vec d) => c y * quadraticObservable (HCPolySupport.basisVec i) y) z = DivergenceFormProcess.Form.onePointRealExtension (fun (y : HCPolySupport.Vec d) => c y * HCPolySupport.vecNormSq y) z

The same decomposition for the coordinate observables cut off by a common factor, read on the one-point carrier.