ShellSumLayerCarrier

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

The layer carrier: resolving the shell-sum corrector into its layers

The shell-sum law of ShellSumCarrierLaw.lean lives on C(Vec d, Mat d), the law of the sum k_m − k_n = Σ_{k ∈ (n,m]} 𝐣_k. That carrier has forgotten the individual layers, so the layer decomposition of e.perturb.assumption cannot even be stated there.

This module introduces the layer carrier ℤ → C(Vec d, Mat d) — the whole sequence of shell value paths — carrying the diagonal translation action, and transports the shell-sum corrector energy onto it. The transport is StationaryCarrierTransport.lean's naturality of the stationary potential projection along an equivariant factor map, applied to the summation map

seqPathSum n m : (ℤ → C(Vec d, Mat d)) → C(Vec d, Mat d), F ↦ Σ_{k ∈ (n,m]} F k,

which is equivariant and pushes the layer law onto the shell-sum law. Under the transport the shell-sum forcing becomes the sum of the layer forcings, and the projection is linear, so the corrector energy becomes the norm-square of a finite sum of layer correctors. Splitting that norm-square into diagonal and cross terms is e.perturb.assumption's layer decomposition; the cross terms are killed in ShellSumLayerFlip.lean.

What is supplied

• seqPathLaw — the law of the whole sequence of shell value paths, with its translation-invariance instance (input: Cutoff.sequenceLaw_stationary, i.e. (J1) + e.diff.law.shift, exactly as for the shell-sum law).
• measurePreserving_seqPathSum, measurePreserving_seqPathCoord — the two equivariant factor maps onto the shell-sum law and onto the single-shell law.
• layerForcing, layerForcingL2 — the layer-k forcing 𝐣_k(0) e on the layer carrier, and its L² class.
• carrierTransport_shellSumForcingL2 — the transported shell-sum forcing is the sum of the layer forcings.
• norm_shellSumPotentialCorrector_eq — the layer decomposition of the corrector: the shell-sum corrector energy equals the norm-square of Σ_{k ∈ (n,m]} P 𝐟_k on the layer carrier.

The layer carrier and its law

def Algsuperdiff.Section3.Provider.Corrector.seqValuePath {d : ℕ} (omega : Cutoff.ShellSeq d) : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The whole sequence of shell value paths.

Equations

• Algsuperdiff.Section3.Provider.Corrector.seqValuePath omega k = (omega k).valuePath

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_seqValuePath {d : ℕ} : Measurable seqValuePath

noncomputable def Algsuperdiff.Section3.Provider.Corrector.seqPathLaw {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → Frozen.Assumptions.ShellField d)) : MeasureTheory.ProbabilityMeasure (ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d))

The layer law. The joint law of all shell value paths.

Equations

• Algsuperdiff.Section3.Provider.Corrector.seqPathLaw P = P.map Algsuperdiff.Section3.Provider.Corrector.seqValuePath

theorem Algsuperdiff.Section3.Provider.Corrector.seqPathLaw_toMeasure {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → Frozen.Assumptions.ShellField d)) : ↑(seqPathLaw P) = MeasureTheory.Measure.map seqValuePath ↑P

theorem Algsuperdiff.Section3.Provider.Corrector.seqValuePath_translateSequence {d : ℕ} (z : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : seqValuePath (Frozen.Assumptions.ShellField.translateSequence z omega) = z +ᵥ seqValuePath omega

The layer carrier is equivariant for the diagonal translation action.

theorem Algsuperdiff.Section3.Provider.Corrector.map_vadd_seqPathLaw {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) : MeasureTheory.Measure.map (fun (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => z +ᵥ F) ↑(seqPathLaw M.P) = ↑(seqPathLaw M.P)

The layer law is translation invariant. The only input is Cutoff.sequenceLaw_stationary; no invariance is assumed on the target law.

instance Algsuperdiff.Section3.Provider.Corrector.vaddInvariantMeasure_seqPathLaw {d : ℕ} (M : ABKModel d) : MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) (ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ↑(seqPathLaw M.P)

The summation factor map

def Algsuperdiff.Section3.Provider.Corrector.seqPathSum {d : ℕ} (n m : ℤ) (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The block summation map: the layer carrier maps onto the shell-sum carrier by summing the layers of the block (n, m].

Equations

• Algsuperdiff.Section3.Provider.Corrector.seqPathSum n m F = ∑ k ∈ Finset.Ioc n m, F k

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_seqPathSum {d : ℕ} (n m : ℤ) : Measurable (seqPathSum n m)

theorem Algsuperdiff.Section3.Provider.Corrector.seqPathSum_vadd {d : ℕ} (n m : ℤ) (z : HCPolySupport.Vec d) (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : seqPathSum n m (z +ᵥ F) = z +ᵥ seqPathSum n m F

theorem Algsuperdiff.Section3.Provider.Corrector.measurePreserving_seqPathSum {d : ℕ} (M : ABKModel d) (n m : ℤ) : MeasureTheory.MeasurePreserving (seqPathSum n m) ↑(seqPathLaw M.P) ↑(shellSumValuePathLaw M.P n m)

The summation map pushes the layer law onto the shell-sum law.

The coordinate factor maps

theorem Algsuperdiff.Section3.Provider.Corrector.shellSumValuePath_pred_self {d : ℕ} (k : ℤ) (omega : Cutoff.ShellSeq d) : shellSumValuePath (k - 1) k omega = (omega k).valuePath

The block (k-1, k] is the single layer k.

theorem Algsuperdiff.Section3.Provider.Corrector.measurePreserving_seqPathCoord {d : ℕ} (M : ABKModel d) (k : ℤ) : MeasureTheory.MeasurePreserving (fun (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => F k) ↑(seqPathLaw M.P) ↑(shellSumValuePathLaw M.P (k - 1) k)

Reading a single layer pushes the layer law onto that layer's law, which is the shell-sum law of the one-element block (k-1, k].

The layer forcings

def Algsuperdiff.Section3.Provider.Corrector.layerForcing {d : ℕ} (e : HCPolySupport.Vec d) (k : ℤ) (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : HCPolySupport.HilbertVec d

The layer-k forcing 𝐣_k(0) e, read on the layer carrier.

Equations

• Algsuperdiff.Section3.Provider.Corrector.layerForcing e k F = Algsuperdiff.Section3.Provider.Corrector.valuePathForcing e (F k)

theorem Algsuperdiff.Section3.Provider.Corrector.memLp_two_layerForcing {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : MeasureTheory.MemLp (layerForcing e k) 2 ↑(seqPathLaw M.P)

noncomputable def Algsuperdiff.Section3.Provider.Corrector.layerForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : ↥(Probability.Stationary.VectorL2 d ↑(seqPathLaw M.P))

The layer-k forcing as an element of the stationary L² layer of the layer carrier.

Equations

• Algsuperdiff.Section3.Provider.Corrector.layerForcingL2 M e k = MeasureTheory.MemLp.toLp (Algsuperdiff.Section3.Provider.Corrector.layerForcing e k) ⋯

theorem Algsuperdiff.Section3.Provider.Corrector.valuePathForcing_comp_seqPathSum {d : ℕ} (e : HCPolySupport.Vec d) (n m : ℤ) : valuePathForcing e ∘ seqPathSum n m = fun (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => ∑ k ∈ Finset.Ioc n m, layerForcing e k F

The shell-sum forcing, transported to the layer carrier, is the pointwise sum of the layer forcings.

theorem Algsuperdiff.Section3.Provider.Corrector.carrierTransport_shellSumForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : (carrierTransport (HCPolySupport.HilbertVec d) ⋯) (shellSumForcingL2 M e n m) = ∑ k ∈ Finset.Ioc n m, layerForcingL2 M e k

The transported shell-sum forcing is the sum of the layer forcings.

The layer decomposition of the corrector

theorem Algsuperdiff.Section3.Provider.Corrector.norm_shellSumPotentialCorrector_eq {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : ‖shellSumPotentialCorrector M e n m‖ = ‖∑ k ∈ Finset.Ioc n m, Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e k)‖

The shell-sum corrector energy, resolved into layers.

The L²(Ω) norm of the canonical shell-sum corrector equals the norm of Σ_{k ∈ (n,m]} P 𝐟_k computed on the layer carrier, where P is the stationary potential projection there. This is the exact point at which e.perturb.assumption's layer decomposition becomes available: on the shell-sum carrier the individual layers are not measurable, on the layer carrier they are, and the two projected energies agree because the summation map is an equivariant factor map.