ShellSumCorrectorLimit

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

The corrector limit at the shell-sum carrier

ABK26, e.def.w, l.corrector.limit and e.perturb.assumption.

Algsuperdiff/Section3/Provider/Corrector/ShellSumCarrierLaw.lean puts the finite shell increment k_m - k_n = Σ_{k ∈ (n,m]} j_k on the compact-open carrier C(Vec d, Mat d) as the law shellSumValuePathLaw M.P n m, and supplies the stationarity instance, the L² layer of the forcing and the unconditional decorrelation bound

E[|A_κ 𝐣|²] ≤ ‖κ‖_∞ · |B_{√d·3^m+1}| · E[|𝐟|²]

at that law. Its header records that the Helmholtz splitting and the approximate-stream assembly at the shell-sum carrier remain open. This module closes both and runs the corrector limit there.

Nothing in the argument is new mathematics: every step is the fresh-shell step of ValuePathTransport.lean / OmegaStreamAssembly.lean / CorrectorLimitNode.lean with the single fresh shell replaced by the block (n, m], i.e. with the decorrelation radius √d + 1 replaced by the increment's own range √d · 3^m + 1. The value of the limit is not evaluated here; that is the shell decomposition and the per-shell dilation, and neither is claimed below.

What is supplied

• shellSumPotentialCorrector, shellSumFlux — the canonical source-sign Helmholtz splitting 𝐣 = 𝐟 + ∇w of the shell-sum forcing under shellSumValuePathLaw M.P n m, with the two subspace memberships (toLp_shellSumCorrectorRepr_mem, toLp_shellSumFlux_mem).
• exists_shellSumStream — the ε-approximate antisymmetric stream for that flux, at every tolerance.
• tendsto_integral_cubeAverage_dirichlet_neumann_shellSum — the corrector limit e.corrector.limit at the shell-sum carrier: both cube energies converge to E[|∇w|²].

Unlike the fresh-shell chain, no normalization of e is assumed anywhere: the L² layer memLp_two_valuePathForcing_shellSum of the shell-sum forcing holds at every direction, so no unit binder is needed and none is introduced.

The canonical Helmholtz splitting at the shell-sum law

noncomputable def Algsuperdiff.Section3.Provider.Corrector.shellSumForcingL2 {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : ↥(Probability.Stationary.VectorL2 d ↑(shellSumValuePathLaw M.P n m))

The shell-sum forcing as an element of the stationary L² layer of the continuous-path carrier under the shell-sum law.

Equations

• Algsuperdiff.Section3.Provider.Corrector.shellSumForcingL2 M e n m = MeasureTheory.MemLp.toLp (Algsuperdiff.Section3.Provider.Corrector.valuePathForcing e) ⋯

noncomputable def Algsuperdiff.Section3.Provider.Corrector.shellSumPotentialCorrector {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : ↥(Probability.Stationary.VectorL2 d ↑(shellSumValuePathLaw M.P n m))

The canonical source-sign potential corrector at the shell-sum law: the negative of the orthogonal projection of the shell-sum forcing onto the stationary potential subspace.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Corrector.shellSumCorrectorRepr {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.HilbertVec d

A strongly measurable representative of the canonical shell-sum corrector.

Equations

• Algsuperdiff.Section3.Provider.Corrector.shellSumCorrectorRepr M e n m = MeasureTheory.AEStronglyMeasurable.mk ↑↑(Algsuperdiff.Section3.Provider.Corrector.shellSumPotentialCorrector M e n m) ⋯

theorem Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_shellSumCorrectorRepr {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.StronglyMeasurable (shellSumCorrectorRepr M e n m)

theorem Algsuperdiff.Section3.Provider.Corrector.memLp_two_shellSumCorrectorRepr {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.MemLp (shellSumCorrectorRepr M e n m) 2 ↑(shellSumValuePathLaw M.P n m)

theorem Algsuperdiff.Section3.Provider.Corrector.toLp_shellSumCorrectorRepr {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.MemLp.toLp (shellSumCorrectorRepr M e n m) ⋯ = shellSumPotentialCorrector M e n m

noncomputable def Algsuperdiff.Section3.Provider.Corrector.shellSumFlux {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.HilbertVec d

The canonical stationary flux 𝐣 = 𝐟 + ∇w at the shell-sum law, as a strongly measurable field.

Equations

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

theorem Algsuperdiff.Section3.Provider.Corrector.shellSumFlux_apply {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) : shellSumFlux M e n m f = valuePathForcing e f + shellSumCorrectorRepr M e n m f

theorem Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_shellSumFlux {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.StronglyMeasurable (shellSumFlux M e n m)

theorem Algsuperdiff.Section3.Provider.Corrector.memLp_two_shellSumFlux {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.MemLp (shellSumFlux M e n m) 2 ↑(shellSumValuePathLaw M.P n m)

theorem Algsuperdiff.Section3.Provider.Corrector.toLp_shellSumCorrectorRepr_mem {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.MemLp.toLp (shellSumCorrectorRepr M e n m) ⋯ ∈ Probability.Stationary.stationaryPotentialSubspace

The canonical shell-sum corrector is stationary potential.

theorem Algsuperdiff.Section3.Provider.Corrector.toLp_shellSumFlux_mem {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) : MeasureTheory.MemLp.toLp (shellSumFlux M e n m) ⋯ ∈ Probability.Stationary.stationarySolenoidalSubspace

The canonical shell-sum flux is stationary solenoidal.

The approximate stream at the shell-sum carrier

theorem Algsuperdiff.Section3.Provider.Corrector.exists_scale_integral_normSq_mollify_productDensity_shellSumFlux_le {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) {t : ℝ} (ht : 0 < t) : ∃ (s : ℝ) (hs : 0 < s), ∫ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖mollify (productDensity d hs) (shellSumFlux M e n m) f‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m) ≤ t

The decorrelation leg at the product density, at the shell-sum carrier.

The shell-sum bound E[|A_κ 𝐣|²] ≤ ‖κ‖_∞ |B_{√d·3^m+1}| E[|𝐟|²] of ShellSumCarrierLaw.lean, applied to the product density of scale s whose sup norm is s^{-d}, is below any tolerance at a large enough scale. This is the fresh-shell exists_scale_integral_normSq_mollify_productDensity_valuePathFlux_le with the radius √d + 1 replaced by the increment's own range.

theorem Algsuperdiff.Section3.Provider.Corrector.exists_shellSumStream {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) {ε : ℝ} (hε : 0 < ε) : ∃ (S : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → Fin d → HCPolySupport.HilbertVec d) (D : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.HilbertVec d), MeasureTheory.StronglyMeasurable S ∧ MeasureTheory.MemLp S 2 ↑(shellSumValuePathLaw M.P n m) ∧ (∀ᵐ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), ∀ (i k : Fin d), ContDiff ℝ (↑⊤) (streamRealization S f i k)) ∧ (∀ᵐ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), ∀ (i k : Fin d), streamRealization S f k i = -streamRealization S f i k) ∧ (∀ᵐ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), ∀ (x : HCPolySupport.Vec d), streamDivergence (streamRealization S f) x = (realize D f x).toVec) ∧ MeasureTheory.StronglyMeasurable D ∧ MeasureTheory.MemLp D 2 ↑(shellSumValuePathLaw M.P n m) ∧ ∫ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖D f - shellSumFlux M e n m f‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m) ≤ ε

The Ω-level ε-approximate antisymmetric stream at the shell-sum carrier.

For every tolerance ε > 0 there is a stationary square-integrable field S whose realizations are smooth and antisymmetric and whose row divergence is, at every point of space, the realization of a stationary square-integrable field D with E[|D − 𝐣|²] ≤ ε, where 𝐣 = shellSumFlux M e n m.

This is exists_freshShellStream with the fresh shell replaced by the block (n, m]; the two error legs are the same, only the decorrelation radius changes.

The corrector limit at the shell-sum carrier

theorem Algsuperdiff.Section3.Provider.Corrector.tendsto_integral_cubeAverage_dirichlet_neumann_shellSum {d : ℕ} (M : ABKModel d) (e : HCPolySupport.Vec d) (n m : ℤ) {Dfam Nfam : ℕ → C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.Vec d → HCPolySupport.Vec d} (hDpot : ∀ (K : ℕ), ∀ᵐ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), HCPolySupport.IsPotentialZeroTraceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (Dfam K ω)) (hDsol : ∀ (K : ℕ), ∀ᵐ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), HCPolySupport.IsSolenoidalOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) fun (x : HCPolySupport.Vec d) => Dfam K ω x + (realize (valuePathForcing e) ω x).toVec) (hNpot : ∀ (K : ℕ), ∀ᵐ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), HCPolySupport.IsPotentialOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (Nfam K ω)) (hNsol : ∀ (K : ℕ), ∀ᵐ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) ∂↑(shellSumValuePathLaw M.P n m), HCPolySupport.IsSolenoidalZeroNormalTraceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) fun (x : HCPolySupport.Vec d) => Nfam K ω x + (realize (valuePathForcing e) ω x).toVec) : Filter.Tendsto (fun (K : ℕ) => ∫ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), HCPolySupport.cubeAverage (HCPolySupport.originCube d ↑K) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (Dfam K ω x) (Dfam K ω x) ∂↑(shellSumValuePathLaw M.P n m)) Filter.atTop (nhds (∫ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖shellSumCorrectorRepr M e n m ω‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m))) ∧ Filter.Tendsto (fun (K : ℕ) => ∫ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), HCPolySupport.cubeAverage (HCPolySupport.originCube d ↑K) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (Nfam K ω x) (Nfam K ω x) ∂↑(shellSumValuePathLaw M.P n m)) Filter.atTop (nhds (∫ (ω : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖shellSumCorrectorRepr M e n m ω‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m)))

l.corrector.limit at the shell-sum carrier (ABK26, at the forcing of e.def.w).

Let ∇w_{D,e}^{(K)} = Dfam K and ∇w_{N,e}^{(K)} = Nfam K be the gradients of the two solutions of e.corrector.limit.pde at the shell-sum forcing 𝐟 = valuePathForcing e under the law of k_m − k_n. Then both limits of e.corrector.limit exist and equal E[|∇w|²], the energy of the canonical Helmholtz corrector at that law.

There is no stream hypothesis, no tolerance, no localization scale, no integrability hypothesis and no normalization of e; the only binders are the frozen model, the shell pair and the two weak formulations.