ShellLawJ1

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

structure Algsuperdiff.Frozen.Assumptions.ShellLawJ1 (d : ℕ) (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : Prop

ABK26 (J1): the zero shell is integrable and mean-zero at every point, invariant in law under every real translation, and has range of dependence sqrt d for the integral-generated local sigma-fields F(U) of the governing homogenization-manuscript convention.

• integrable (x : HCPolySupport.Vec d) : MeasureTheory.Integrable (fun (F : ℤ → ShellField d) => (↑(F 0)).1 x) ↑P
• mean_zero (x : HCPolySupport.Vec d) : ∫ (F : ℤ → ShellField d), (↑(F 0)).1 x ∂↑P = 0
• stationary (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (ShellField.translate z) ↑(ShellField.zeroShellLaw P) = ↑(ShellField.zeroShellLaw P)
• range_dependence (U V : Set (HCPolySupport.Vec d)) : MeasurableSet U → MeasurableSet V → (∀ ⦃x y : HCPolySupport.Vec d⦄, x ∈ U → y ∈ V → √↑d ≤ HCPolySupport.Book.Ch02.vecNorm (x - y)) → ProbabilityTheory.Indep (ShellField.lihLocalSigma U) (ShellField.lihLocalSigma V) ↑(ShellField.zeroShellLaw P)