ShellSumLayerDilation

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

The per-layer dilation 3^{2γk} of e.perturb.assumption

ShellSumLayerFlip.lean reduces the shell-sum corrector energy to the diagonal sum Σ_{k ∈ (n,m]} ‖P 𝐟_k‖² on the layer carrier, and ShellSumLayerZeroEnergy.lean evaluates the k = 0 term as c⋆ (log 3). This module supplies the missing per-layer factor: for every k,

‖P 𝐟_k‖ = 3^{γk} ‖P 𝐟_0‖, hence ‖P 𝐟_k‖² = 3^{2γk} ‖P 𝐟_0‖².

The route

The transport is carried by the triadic dilation of a value path

pathScale γ k f = 3^{γk} · f(3^{-k} ·),

which is ShellField.triadicScale γ k read on the compact-open carrier (pathScale_valuePath, a definitional identity). Two facts about it are used.

• map_pathScale_shellSumValuePathLaw — it pushes the layer-0 path law onto the layer-k path law. This is exactly e.diff.law.shift, i.e. the frozen ShellLawPrefix.marginal_scaling, and no independence is used: the statement is about one marginal at a time.
• pathScale_vadd — it is equivariant only up to the dilation c = 3^k of the acting group, Ψ (x +ᵥ f) = (3^k • x) +ᵥ Ψ f. This is why the ordinary naturality of StationaryCarrierTransport.lean does not apply and the dilating naturality of ShellSumScaledTransport.lean is needed.

The reduction of the joint projection to a marginal one is the already proved naturality along the equivariant coordinate factor map F ↦ F k (measurePreserving_seqPathCoord), the same device by which ShellSumLayerZeroEnergy.lean evaluates the k = 0 layer.

What is supplied

• pathScale, pathScale_apply, continuous_pathScale, measurable_pathScale, pathScale_valuePath, pathScale_vadd.
• shellSumValuePathLaw_pred_self — the one-layer block law is the valuePath pushforward of the shell marginal.
• map_pathScale_shellSumValuePathLaw, measurePreserving_pathScale.
• valuePathForcing_pathScale, carrierTransport_pathScale_shellSumForcingL2.
• norm_stationaryPotentialProjection_layerForcingL2 and its square norm_sq_stationaryPotentialProjection_layerForcingL2 — the per-layer dilation.

The triadic dilation on the value-path carrier

def Algsuperdiff.Section3.Provider.Corrector.dilationMap {d : ℕ} (r : ℝ) : C(HCPolySupport.Vec d, HCPolySupport.Vec d)

The spatial dilation x ↦ r • x, as a continuous map.

Equations

• Algsuperdiff.Section3.Provider.Corrector.dilationMap r = { toFun := fun (x : HCPolySupport.Vec d) => r • x, continuous_toFun := ⋯ }

noncomputable def Algsuperdiff.Section3.Provider.Corrector.pathScale {d : ℕ} (gamma : ℝ) (k : ℤ) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : C(HCPolySupport.Vec d, HCPolySupport.Mat d)

The triadic dilation of a value path, f ↦ 3^{γk} f(3^{-k} ·). This is ShellField.triadicScale γ k read on the compact-open carrier.

Equations

• Algsuperdiff.Section3.Provider.Corrector.pathScale gamma k f = 3 ^ (gamma * ↑k) • f.comp (Algsuperdiff.Section3.Provider.Corrector.dilationMap (3 ^ k)⁻¹)

@[simp]

theorem Algsuperdiff.Section3.Provider.Corrector.pathScale_apply {d : ℕ} (gamma : ℝ) (k : ℤ) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) (x : HCPolySupport.Vec d) : (pathScale gamma k f) x = 3 ^ (gamma * ↑k) • f ((3 ^ k)⁻¹ • x)

theorem Algsuperdiff.Section3.Provider.Corrector.continuous_pathScale {d : ℕ} (gamma : ℝ) (k : ℤ) : Continuous (pathScale gamma k)

theorem Algsuperdiff.Section3.Provider.Corrector.measurable_pathScale {d : ℕ} (gamma : ℝ) (k : ℤ) : Measurable (pathScale gamma k)

theorem Algsuperdiff.Section3.Provider.Corrector.pathScale_valuePath {d : ℕ} (gamma : ℝ) (k : ℤ) (j : Frozen.Assumptions.ShellField d) : pathScale gamma k j.valuePath = (Frozen.Assumptions.ShellField.triadicScale gamma k j).valuePath

The dilation of a value path is the value path of the dilated shell field. Both sides are the same term.

theorem Algsuperdiff.Section3.Provider.Corrector.pathScale_vadd {d : ℕ} (gamma : ℝ) (k : ℤ) (z : HCPolySupport.Vec d) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : pathScale gamma k (z +ᵥ f) = 3 ^ k • z +ᵥ pathScale gamma k f

The dilation is equivariant up to the dilation 3^k of the acting group. This is the reason StationaryCarrierTransport.lean does not apply and ShellSumScaledTransport.lean does.

The layer laws and the dilation between them

theorem Algsuperdiff.Section3.Provider.Corrector.shellSumValuePathLaw_pred_self {d : ℕ} (M : ABKModel d) (k : ℤ) : ↑(shellSumValuePathLaw M.P (k - 1) k) = MeasureTheory.Measure.map Frozen.Assumptions.ShellField.valuePath ↑(Frozen.Assumptions.ShellField.shellMarginalLaw M.P k)

The one-layer block law (k-1, k] is the valuePath pushforward of the k-th shell marginal.

theorem Algsuperdiff.Section3.Provider.Corrector.map_pathScale_shellSumValuePathLaw {d : ℕ} (M : ABKModel d) (k : ℤ) : MeasureTheory.Measure.map (pathScale M.gamma k) ↑(shellSumValuePathLaw M.P (0 - 1) 0) = ↑(shellSumValuePathLaw M.P (k - 1) k)

The triadic dilation pushes the layer-0 law onto the layer-k law. The only input is e.diff.law.shift, i.e. the frozen ShellLawPrefix.marginal_scaling; no independence enters.

theorem Algsuperdiff.Section3.Provider.Corrector.measurePreserving_pathScale {d : ℕ} (M : ABKModel d) (k : ℤ) : MeasureTheory.MeasurePreserving (pathScale M.gamma k) ↑(shellSumValuePathLaw M.P (0 - 1) 0) ↑(shellSumValuePathLaw M.P (k - 1) k)

The forcing under the dilation

theorem Algsuperdiff.Section3.Provider.Corrector.valuePathForcing_pathScale {d : ℕ} (gamma : ℝ) (k : ℤ) (e : HCPolySupport.Vec d) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : valuePathForcing e (pathScale gamma k f) = 3 ^ (gamma * ↑k) • valuePathForcing e f

The dilation multiplies the path forcing by 3^{γk}: the forcing only sees the value at the origin, which the spatial dilation fixes.

theorem Algsuperdiff.Section3.Provider.Corrector.carrierTransport_pathScale_shellSumForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : (carrierTransport (HCPolySupport.HilbertVec d) ⋯) (shellSumForcingL2 M e (k - 1) k) = 3 ^ (M.gamma * ↑k) • shellSumForcingL2 M e (0 - 1) 0

theorem Algsuperdiff.Section3.Provider.Corrector.norm_stationaryPotentialProjection_shellSumForcingL2_layer {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : ‖Probability.Stationary.stationaryPotentialProjection (shellSumForcingL2 M e (k - 1) k)‖ = 3 ^ (M.gamma * ↑k) * ‖Probability.Stationary.stationaryPotentialProjection (shellSumForcingL2 M e (0 - 1) 0)‖

The layer-k marginal corrector energy is 3^{2γk} times the layer-0 one, in norm form. The dilating naturality of ShellSumScaledTransport.lean is applied at c = 3^k.

From the joint layer carrier to the single-layer marginal

theorem Algsuperdiff.Section3.Provider.Corrector.carrierTransport_seqPathCoord_shellSumForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : (carrierTransport (HCPolySupport.HilbertVec d) ⋯) (shellSumForcingL2 M e (k - 1) k) = layerForcingL2 M e k

theorem Algsuperdiff.Section3.Provider.Corrector.norm_stationaryPotentialProjection_layerForcingL2_eq_shellSum {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e k)‖ = ‖Probability.Stationary.stationaryPotentialProjection (shellSumForcingL2 M e (k - 1) k)‖

The layer-k corrector energy on the joint layer carrier is the corrector energy of the layer-k marginal. This is the naturality of the stationary potential projection along the equivariant coordinate factor map, exactly as in the k = 0 case of ShellSumLayerZeroEnergy.lean.

The per-layer dilation of e.perturb.assumption

theorem Algsuperdiff.Section3.Provider.Corrector.norm_stationaryPotentialProjection_layerForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e k)‖ = 3 ^ (M.gamma * ↑k) * ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e 0)‖

The per-layer dilation, in norm form. No normalization of e is assumed.

theorem Algsuperdiff.Section3.Provider.Corrector.norm_sq_stationaryPotentialProjection_layerForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (k : ℤ) : ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e k)‖ ^ 2 = 3 ^ (2 * M.gamma * ↑k) * ‖Probability.Stationary.stationaryPotentialProjection (layerForcingL2 M e 0)‖ ^ 2

The per-layer factor 3^{2γk} of e.perturb.assumption.