ShellSumEnergyDisplay

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

e.perturb.assumption: the fresh-shell corrector energy display

This module assembles the four proved halves into the printed display.

• the layer decomposition ShellSumLayerFlip.integral_normSq_shellSumCorrectorRepr_eq_sum ((J1) independence + (J3) negation, per ****);
• the k = 0 value ShellSumLayerZeroEnergy.norm_sq_stationaryPotentialProjection_layerForcingL2_zero ((J4), a.j.nondeg);
• the per-layer dilation ShellSumLayerDilation.norm_sq_stationaryPotentialProjection_layerForcingL2 (e.diff.law.shift, per ****);
• the corrector limit ShellSumConsumerTransport.tendsto_integral_cutoffSample_cubeAverage_of_weakSolutions (l.corrector.limit at the consumer's carrier).

What is supplied

• integral_normSq_shellSumCorrectorRepr_eq_display — at a unit direction, the shell-sum corrector energy is c⋆ (log 3) Σ_{k ∈ (n,m]} 3^{2γk}.
• shellSumForcingL2_smul, integral_normSq_shellSumCorrectorRepr_smul — the |e|² bilinearity: the corrector energy is quadratic in the direction.
• integral_normSq_shellSumCorrectorRepr_gauge_display — the printed display at the gauged direction c • e, |e| = 1: c² c⋆ (log 3) Σ_{k ∈ (n,m]} 3^{2γk}. The manuscript's gauge σ_{m-h}^{-1} is the scalar c, so the printed σ_{m-h}^{-2} is the factor c².
• tendsto_integral_cutoffSample_cubeAverage_display — the same, transported through the corrector limit to the consumer's carrier: both the Dirichlet and the Neumann localized cube energies converge, as K → ∞, to that value. This is e.perturb.assumption and e.perturb.assumption.two together.

The direction e is normalized by Book.Ch02.vecNorm e = 1, the manuscript's e ∈ ∂B_1; the gauge is free. No other binder is introduced: the corrector families enter only through the two weak formulations of e.def.w, and the two AEStronglyMeasurable typing binders are the ones the proved corrector limit already carries.

The display at a unit direction

theorem Algsuperdiff.Section3.Provider.Corrector.integral_normSq_shellSumCorrectorRepr_eq_display {d : ℕ} (M : ABKModel d) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) (n m : ℤ) : ∫ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖shellSumCorrectorRepr M e n m f‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m) = Disorder.cstar M * Real.log 3 * ∑ k ∈ Finset.Ioc n m, 3 ^ (2 * M.gamma * ↑k)

e.perturb.assumption at a unit direction, at the shell-sum carrier.

The corrector energy of the shell-sum forcing over the block (n, m] is c⋆ (log 3) Σ_{k ∈ (n,m]} 3^{2γk}. The three inputs are the layer decomposition, the k = 0 value c⋆ (log 3) of (J4), and the per-layer dilation 3^{2γk} of e.diff.law.shift.

The |e|² bilinearity

theorem Algsuperdiff.Section3.Provider.Corrector.shellSumForcingL2_smul {d : ℕ} (M : ABKModel d) (c : ℝ) (e : HCPolySupport.Vec d) (n m : ℤ) : shellSumForcingL2 M (c • e) n m = c • shellSumForcingL2 M e n m

The shell-sum forcing is linear in the direction.

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

The corrector energy is quadratic in the direction, the |e|² of e.perturb.assumption.

The gauged display

theorem Algsuperdiff.Section3.Provider.Corrector.integral_normSq_shellSumCorrectorRepr_gauge_display {d : ℕ} (M : ABKModel d) (c : ℝ) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) (n m : ℤ) : ∫ (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), ‖shellSumCorrectorRepr M (c • e) n m f‖ ^ 2 ∂↑(shellSumValuePathLaw M.P n m) = c ^ 2 * (Disorder.cstar M * Real.log 3 * ∑ k ∈ Finset.Ioc n m, 3 ^ (2 * M.gamma * ↑k))

e.perturb.assumption, the printed display.

At the gauged direction c • e with |e| = 1 the shell-sum corrector energy is c² c⋆ (log 3) Σ_{k ∈ (n,m]} 3^{2γk}. The manuscript's gauge is c = σ_{m-h}^{-1}, giving its σ_{m-h}^{-2}.

The display at the consumer's carrier

theorem Algsuperdiff.Section3.Provider.Corrector.tendsto_integral_cutoffSample_cubeAverage_display {d : ℕ} (M : ABKModel d) (c : ℝ) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) (n m : ℤ) (wD : (K : ℕ) → C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) (wN : (K : ℕ) → C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) (hDm : ∀ (K : ℕ), MeasureTheory.AEStronglyMeasurable (fun (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => HCPolySupport.cubeAverage (HCPolySupport.originCube d ↑K) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot ((wD K f).grad x) ((wD K f).grad x)) ↑(shellSumValuePathLaw M.P n m)) (hNm : ∀ (K : ℕ), MeasureTheory.AEStronglyMeasurable (fun (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)) => HCPolySupport.cubeAverage (HCPolySupport.originCube d ↑K) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot ((wN K f).toH1Function.grad x) ((wN K f).toH1Function.grad x)) ↑(shellSumValuePathLaw M.P n m)) (hD : ∀ (K : ℕ) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (wD K f) fun (x : HCPolySupport.Vec d) => -(realize (valuePathForcing (c • e)) f x).toVec) (hN : ∀ (K : ℕ) (f : C(HCPolySupport.Vec d, HCPolySupport.Mat d)), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (wN K f) fun (x : HCPolySupport.Vec d) => -(realize (valuePathForcing (c • e)) f x).toVec) : Filter.Tendsto (fun (K : ℕ) => ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.cubeAverage (HCPolySupport.originCube d ↑K) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot ((wD K (shellSumValuePath n m ↑omega)).grad x) ((wD K (shellSumValuePath n m ↑omega)).grad x) ∂↑(Cutoff.cutoffSampleLaw M)) Filter.atTop (nhds (c ^ 2 * (Disorder.cstar M * Real.log 3 * ∑ k ∈ Finset.Ioc n m, 3 ^ (2 * M.gamma * ↑k)))) ∧ Filter.Tendsto (fun (K : ℕ) => ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.cubeAverage (HCPolySupport.originCube d ↑K) fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot ((wN K (shellSumValuePath n m ↑omega)).toH1Function.grad x) ((wN K (shellSumValuePath n m ↑omega)).toH1Function.grad x) ∂↑(Cutoff.cutoffSampleLaw M)) Filter.atTop (nhds (c ^ 2 * (Disorder.cstar M * Real.log 3 * ∑ k ∈ Finset.Ioc n m, 3 ^ (2 * M.gamma * ↑k))))

e.perturb.assumption and e.perturb.assumption.two at the recurrence consumer's data.

Both localized cube energies -- the Dirichlet one and the Neumann one -- of the solutions of e.def.w at the gauged forcing -streamForcing c ω n m e converge, as the localization cube □_K exhausts space, to

c² c⋆ (log 3) Σ_{k ∈ (n,m]} 3^{2γk}.

The sample integral is taken over CutoffSample d against cutoffSampleLaw M, the carrier the recurrence consumer integrates over; the corrector families are indexed by the increment path, which is what e.def.w gives. The gauge enters as the scalar c of the direction c • e and needs no separate step (ShellSumConsumerTransport.toVec_realize_valuePathForcing_shellSumValuePath identifies the forcing here with the consumer's streamForcing c ω n m e).

The only binders are the frozen model, the shell pair, the unit direction, the two weak formulations of e.def.w, and the two AEStronglyMeasurable typing binders of the proved corrector limit.