ShellSumLayerFlip

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

The cross terms of the layer decomposition vanish

ShellSumLayerCarrier.lean resolves the shell-sum corrector energy into

‖Σ_{k ∈ (n,m]} P 𝐟_k‖²

on the layer carrier, P the stationary potential projection.

This module carries out that argument.

The single-layer flip

Negating one layer preserves the joint law:

• each shell marginal is negation invariant — take the k-th marginal of the whole-sequence identity of (J3) (map_negate_shellMarginalLaw); this uses no independence;
• the joint law is the product of its marginals by (J1) independence, so a coordinatewise map preserves it as soon as each marginal is preserved (map_negateLayer), exactly the engine of Cutoff.sequenceLaw_stationary.

The flip is equivariant for the translation action, so its Koopman operator is a linear isometry that commutes with P (stationaryPotentialProjection_carrierTransport), and it negates 𝐟_k while fixing every 𝐟_l, l ≠ k. The pairing is therefore odd under it and vanishes.

What is supplied

• map_negate_shellMarginalLaw — (J3) at a single shell marginal.
• map_negateLayer — the single-layer flip preserves the sequence law.
• measurePreserving_flipLayer — the same on the layer carrier.
• flipKoopman_layerForcingL2 — the flip negates its own layer and fixes the others.
• inner_stationaryPotentialProjection_layerForcingL2_eq_zero — the cross-term kill.
• integral_normSq_shellSumCorrectorRepr_eq_sum — the layer decomposition of e.perturb.assumption: the shell-sum corrector energy is the sum over k ∈ (n,m] of the layer corrector energies.

(J3) at a single shell marginal

theorem Algsuperdiff.Section3.Provider.Corrector.map_negate_shellMarginalLaw {d : ℕ} (M : ABKModel d) (k : ℤ) : MeasureTheory.Measure.map Frozen.Assumptions.ShellField.negate ↑(Frozen.Assumptions.ShellField.shellMarginalLaw M.P k) = ↑(Frozen.Assumptions.ShellField.shellMarginalLaw M.P k)

Each shell marginal is negation invariant. This is the k-th marginal of the whole-sequence negation identity of (J3); no independence is used.

The single-layer flip on the sequence carrier

noncomputable def Algsuperdiff.Section3.Provider.Corrector.negateLayerField {d : ℕ} (k l : ℤ) (j : Frozen.Assumptions.ShellField d) : Frozen.Assumptions.ShellField d

Negate the shell field at index l exactly when l = k.

Equations

• Algsuperdiff.Section3.Provider.Corrector.negateLayerField k l j = if l = k then j.negate else j

theorem Algsuperdiff.Section3.Provider.Corrector.negateLayerField_self {d : ℕ} (k : ℤ) (j : Frozen.Assumptions.ShellField d) : negateLayerField k k j = j.negate

theorem Algsuperdiff.Section3.Provider.Corrector.negateLayerField_of_ne {d : ℕ} {k l : ℤ} (h : l ≠ k) (j : Frozen.Assumptions.ShellField d) : negateLayerField k l j = j

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_negateLayerField {d : ℕ} (k l : ℤ) : Measurable (negateLayerField k l)

noncomputable def Algsuperdiff.Section3.Provider.Corrector.negateLayer {d : ℕ} (k : ℤ) (omega : Cutoff.ShellSeq d) : Cutoff.ShellSeq d

Negate one layer of the shell sequence.

Equations

• Algsuperdiff.Section3.Provider.Corrector.negateLayer k omega l = Algsuperdiff.Section3.Provider.Corrector.negateLayerField k l (omega l)

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_negateLayer {d : ℕ} (k : ℤ) : Measurable (negateLayer k)

theorem Algsuperdiff.Section3.Provider.Corrector.map_negateLayer {d : ℕ} (M : ABKModel d) (k : ℤ) : MeasureTheory.Measure.map (negateLayer k) ↑M.P = ↑M.P

Negating a single layer preserves the joint sequence law.

(J1) independence turns the joint law into the product of its marginals, and (J3) makes every marginal negation invariant; a coordinatewise map therefore preserves the joint law. The engine is exactly the one used by Cutoff.sequenceLaw_stationary for translations.

The single-layer flip on the layer carrier

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

Negate one layer of the sequence of shell value paths.

Equations

• Algsuperdiff.Section3.Provider.Corrector.flipLayer k F l = if l = k then -F l else F l

theorem Algsuperdiff.Section3.Provider.Corrector.flipLayer_self {d : ℕ} (k : ℤ) (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : flipLayer k F k = -F k

theorem Algsuperdiff.Section3.Provider.Corrector.flipLayer_of_ne {d : ℕ} {k l : ℤ} (h : l ≠ k) (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : flipLayer k F l = F l

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_flipLayer {d : ℕ} (k : ℤ) : Measurable (flipLayer k)

theorem Algsuperdiff.Section3.Provider.Corrector.flipLayer_seqValuePath {d : ℕ} (k : ℤ) (omega : Cutoff.ShellSeq d) : flipLayer k (seqValuePath omega) = seqValuePath (negateLayer k omega)

theorem Algsuperdiff.Section3.Provider.Corrector.flipLayer_vadd {d : ℕ} (k : ℤ) (z : HCPolySupport.Vec d) (F : ℤ → C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : flipLayer k (z +ᵥ F) = z +ᵥ flipLayer k F

theorem Algsuperdiff.Section3.Provider.Corrector.measurePreserving_flipLayer {d : ℕ} (M : ABKModel d) (k : ℤ) : MeasureTheory.MeasurePreserving (flipLayer k) ↑(seqPathLaw M.P) ↑(seqPathLaw M.P)

The single-layer flip preserves the layer law.

The Koopman operator of the flip

noncomputable def Algsuperdiff.Section3.Provider.Corrector.flipKoopman {d : ℕ} (M : ABKModel d) (k : ℤ) : ↥(Probability.Stationary.VectorL2 d ↑(seqPathLaw M.P)) →L[ℝ] ↥(Probability.Stationary.VectorL2 d ↑(seqPathLaw M.P))

The Koopman isometry of the single-layer flip on the stationary L² layer.

Equations

• Algsuperdiff.Section3.Provider.Corrector.flipKoopman M k = Algsuperdiff.Section3.Provider.Corrector.carrierTransport (HCPolySupport.HilbertVec d) ⋯

theorem Algsuperdiff.Section3.Provider.Corrector.inner_flipKoopman {d : ℕ} (M : ABKModel d) (k : ℤ) (u v : ↥(Probability.Stationary.VectorL2 d ↑(seqPathLaw M.P))) : inner ℝ ((flipKoopman M k) u) ((flipKoopman M k) v) = inner ℝ u v

The flip Koopman operator preserves inner products.

theorem Algsuperdiff.Section3.Provider.Corrector.flipKoopman_stationaryPotentialProjection {d : ℕ} (M : ABKModel d) (k : ℤ) (G : ↥(Probability.Stationary.VectorL2 d ↑(seqPathLaw M.P))) : Probability.Stationary.stationaryPotentialProjection ((flipKoopman M k) G) = (flipKoopman M k) (Probability.Stationary.stationaryPotentialProjection G)

The flip Koopman operator commutes with the stationary potential projection: the flip is an equivariant measure-preserving self-map, so StationaryCarrierTransport's naturality applies.

theorem Algsuperdiff.Section3.Provider.Corrector.flipKoopman_layerForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k l : ℤ) : (flipKoopman M k) (layerForcingL2 M e l) = if l = k then -layerForcingL2 M e l else layerForcingL2 M e l

The flip negates the forcing of its own layer and fixes every other layer forcing.

The cross-term kill

theorem Algsuperdiff.Section3.Provider.Corrector.inner_stationaryPotentialProjection_layerForcingL2_eq_zero {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) {k l : ℤ} (hkl : l ≠ k) : inner ℝ (Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e k)) (Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e l)) = 0

The cross terms of the layer decomposition vanish.

For k ≠ l the pairing of the layer-k and layer-l correctors is zero. The argument is the single-layer flip: it is measure preserving by (J1) + (J3), it is equivariant, so its Koopman isometry commutes with the projection, and it negates exactly one of the two forcings.

The layer decomposition of the corrector energy

theorem Algsuperdiff.Section3.Provider.Corrector.integral_normSq_shellSumCorrectorRepr_eq_norm_sq {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : ∫ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖shellSumCorrectorRepr M e n m f‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m) = ‖shellSumPotentialCorrector M e n m‖ ^ 2

The L² norm square of the shell-sum corrector is the expectation of the squared Euclidean norm of its strongly measurable representative.

theorem Algsuperdiff.Section3.Provider.Corrector.integral_normSq_shellSumCorrectorRepr_eq_sum {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : ∫ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖shellSumCorrectorRepr M e n m f‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m) = ∑ k ∈ Finset.Ioc n m, ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e k)‖ ^ 2

The layer decomposition of e.perturb.assumption.

The corrector energy of the shell-sum forcing is the sum, over the layers of the block (n, m], of the layer corrector energies.

No normalization of e is assumed. The per-layer factor 3^{2γk} of e.perturb.assumption is not proved here.