StationaryValueProjection

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

Stationary projection on the CoarseGraining regular-coefficient carrier

This is the carrier-specific J4 bridge. It uses CoarseGraining's RegCoeffField d and its canonical sigma-algebra directly: no continuous-path replacement carrier is introduced. It pushes the canonical zero-shell marginal through forgetShell.

The real translation action on CoarseGraining's carrier

@[instance_reducible]

noncomputable instance Algsuperdiff.Frozen.Assumptions.ShellField.regCoeffFieldAddAction {d : ℕ} : AddAction (HCPolySupport.Vec d) (HCPolySupport.RegCoeffField d)

CoarseGraining's real translation maps form the manuscript action (z +ᵥ a)(x) = a(x + z).

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.regCoeffFieldAddAction = { vadd := HCPolySupport.translateReg, add_vadd := ⋯, zero_vadd := ⋯ }

instance Algsuperdiff.Frozen.Assumptions.ShellField.regCoeffFieldMeasurableConstVAdd {d : ℕ} : MeasurableConstVAdd (HCPolySupport.Vec d) (HCPolySupport.RegCoeffField d)

Only fixed-shift measurability is needed for the stationary Hilbert-space construction, and it is exactly CoarseGraining's proved translateReg measurability.

The CoarseGraining pushforward of the shell-zero law

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_zeroShellRegMap {d : ℕ} : Measurable (forgetShell ∘ fun (F : ℤ → ShellField d) => F 0)

Measurability of the literal shell-zero map into CoarseGraining's regular-field carrier.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellRegLaw {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : MeasureTheory.ProbabilityMeasure (HCPolySupport.RegCoeffField d)

The probability law of the regular coefficient field in shell zero. This is precisely map (forgetShell ∘ coord 0) P; its construction requires the proved measurable map above and therefore has no totalized-map fallback.

Equations

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

theorem Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellRegLaw_toMeasure_eq_map_forgetShell {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : ↑(zeroShellRegLaw P) = MeasureTheory.Measure.map forgetShell ↑(zeroShellLaw P)

The direct regular-field zero-shell law is exactly the measurable forgetShell pushforward of the literal zero-coordinate shell law.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.forgetShell_translateReg {d : ℕ} (z : HCPolySupport.Vec d) (j : ShellField d) : (translate z j).forgetShell = HCPolySupport.translateReg z j.forgetShell

The shell-field and CoarseGraining regular-field translation conventions agree literally: both send a(x) to a(x + z).

theorem Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellRegLaw_stationary_of_zeroShellLaw_stationary {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (hstationary : ∀ (z : HCPolySupport.Vec d), MeasureTheory.Measure.map (translate z) ↑(zeroShellLaw P) = ↑(zeroShellLaw P)) (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (HCPolySupport.translateReg z) ↑(zeroShellRegLaw P) = ↑(zeroShellRegLaw P)

Full real-translation invariance of the literal zero-shell law descends to the CoarseGraining regular-field pushforward. No stationarity hypothesis is added on the target law.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellRegLaw_vaddInvariant {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (hstationary : ∀ (z : HCPolySupport.Vec d), MeasureTheory.Measure.map (HCPolySupport.translateReg z) ↑(zeroShellRegLaw P) = ↑(zeroShellRegLaw P)) : MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) (HCPolySupport.RegCoeffField d) ↑(zeroShellRegLaw P)

Full real stationarity of the zero-shell law supplies the invariant measure structure used by the stationary projection.

The literal origin forcing and its L² projection

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.matVecMulLinear {d : ℕ} (e : HCPolySupport.Vec d) : HCPolySupport.Mat d →ₗ[ℝ] HCPolySupport.Vec d

Evaluate matrix-vector multiplication at a fixed vector as a linear map.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.matVecMulLinear e = { toFun := fun (A : HCPolySupport.Mat d) => HCPolySupport.matVecMul A e, map_add' := ⋯, map_smul' := ⋯ }

def Algsuperdiff.Frozen.Assumptions.ShellField.originForcing {d : ℕ} (e : HCPolySupport.Vec d) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.HilbertVec d

The literal matrix-vector forcing at the spatial origin, promoted to CoarseGraining's Euclidean Hilbert carrier.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.originForcing e a = HCPolySupport.HilbertVec.ofVec (HCPolySupport.matVecMul (a.toFun 0) e)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_originForcing {d : ℕ} (e : HCPolySupport.Vec d) : Measurable (originForcing e)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.norm_sq_originForcing {d : ℕ} (e : HCPolySupport.Vec d) (a : HCPolySupport.RegCoeffField d) : ‖originForcing e a‖ ^ 2 = HCPolySupport.vecDot (HCPolySupport.matVecMul (a.toFun 0) e) (HCPolySupport.matVecMul (a.toFun 0) e)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.norm_originForcing_le_matrixOperatorNorm {d : ℕ} (e : HCPolySupport.Vec d) (a : HCPolySupport.RegCoeffField d) (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : ‖originForcing e a‖ ≤ HCPolySupport.Book.Ch02.matrixOperatorNorm (a.toFun 0)

A unit input vector bounds the literal origin forcing by the Euclidean operator norm of the coefficient matrix at the origin.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.matrixOperatorNorm_zero_le_unitCubeValueNorm {d : ℕ} (j : ShellField d) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 0) ≤ j.unitCubeValueNorm

The value part of the J2 cube observable controls the coefficient matrix at the spatial origin.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.memLp_originForcing_of_j2_tail {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (htail : ∀ (t : ℝ), 1 ≤ t → ↑P {F : ℤ → ShellField d | t < j2Observable d (F 0)} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))) (e : HCPolySupport.Vec d) (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : MeasureTheory.MemLp (originForcing e) 2 ↑(zeroShellRegLaw P)

The literal strict J2 Gaussian tail supplies the L² integrability of the origin forcing required by the stationary projection. Measurability, nonnegativity, and domination are consequences, not hypotheses.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellForcingL2 {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (e : HCPolySupport.Vec d) (hmem : MeasureTheory.MemLp (originForcing e) 2 ↑(zeroShellRegLaw P)) : ↥(Probability.Stationary.VectorL2 d ↑(zeroShellRegLaw P))

The canonical L² element represented by the source's origin forcing.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellForcingL2 P e hmem = MeasureTheory.MemLp.toLp (Algsuperdiff.Frozen.Assumptions.ShellField.originForcing e) hmem

theorem Algsuperdiff.Frozen.Assumptions.ShellField.coeFn_zeroShellForcingL2 {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (e : HCPolySupport.Vec d) (hmem : MeasureTheory.MemLp (originForcing e) 2 ↑(zeroShellRegLaw P)) : ↑↑(zeroShellForcingL2 P e hmem) =ᵐ[↑(zeroShellRegLaw P)] originForcing e

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellPotentialSubspace {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (hstationary : ∀ (z : HCPolySupport.Vec d), MeasureTheory.Measure.map (HCPolySupport.translateReg z) ↑(zeroShellRegLaw P) = ↑(zeroShellRegLaw P)) : Submodule ℝ ↥(Probability.Stationary.VectorL2 d ↑(zeroShellRegLaw P))

The stationary potential subspace for the zero-shell regular-field law.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellPotentialSubspace P hstationary = Algsuperdiff.Probability.Stationary.stationaryPotentialSubspace

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellProjectedForcing {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (hstationary : ∀ (z : HCPolySupport.Vec d), MeasureTheory.Measure.map (HCPolySupport.translateReg z) ↑(zeroShellRegLaw P) = ↑(zeroShellRegLaw P)) (e : HCPolySupport.Vec d) (hmem : MeasureTheory.MemLp (originForcing e) 2 ↑(zeroShellRegLaw P)) : ↥(Probability.Stationary.VectorL2 d ↑(zeroShellRegLaw P))

The canonical potential part of the stationary origin forcing.

Equations

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

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellPotentialCorrector {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (hstationary : ∀ (z : HCPolySupport.Vec d), MeasureTheory.Measure.map (HCPolySupport.translateReg z) ↑(zeroShellRegLaw P) = ↑(zeroShellRegLaw P)) (e : HCPolySupport.Vec d) (hmem : MeasureTheory.MemLp (originForcing e) 2 ↑(zeroShellRegLaw P)) : ↥(Probability.Stationary.VectorL2 d ↑(zeroShellRegLaw P))

The canonical source-sign potential corrector. ABK26 solves -Δw = div F and requires F + ∇w to be stationary-solenoidal; therefore ∇w is the negative of the positive orthogonal projection of F onto the stationary potential subspace.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellPotentialCorrector P hstationary e hmem = -Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellProjectedForcing P hstationary e hmem