CorrectorLimitFreshShell

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

Provider: the sandwich and the conclusion of the corrector-limit lemma

ABK26, Lemma l.corrector.limit. Step 4 combines

• the ordering e.ordering.corrector.limit, ‖∇w_D^{(K)}‖²_{L²(cu_K)} ≤ ‖∇w_N^{(K)}‖²_{L²(cu_K)}, proved at a fixed realization in Algsuperdiff/Section3/Provider/Corrector/CubeComparison.lean;
• the lower bound e.lower.bound.corrector.limit, proved unconditionally in Algsuperdiff/Section3/Provider/Corrector/DirichletLowerBound.lean;
• the upper bound e.upper.bound.neumann.corrector.limit, proved in Algsuperdiff/Section3/Provider/Corrector/NeumannUpperBound.lean,

into the displayed chain

E[|∇w|²] ≤ liminf_K E[‖∇w_D^{(K)}‖²] ≤ limsup_K E[‖∇w_N^{(K)}‖²] ≤ E[|∇w|²],

which gives e.corrector.limit: both limits exist and equal E[|∇w|²].

This file proves that, in the form "both sequences converge to E[|∇w|²]", which is the manuscript's assertion that "the limits below exist and" are equal.

The two cube problems as data

The lemma is stated for the solutions w_D^{(K)} ∈ H¹₀(cu_K) and w_N^{(K)} ∈ H¹(cu_K) of e.corrector.limit.pde. Accordingly their gradients enter below as given families Dfam, Nfam carrying exactly the weak formulations of that display — IsPotentialZeroTraceOn with IsSolenoidalOn (D + f) for the Dirichlet problem, IsPotentialOn with IsSolenoidalZeroNormalTraceOn (N + f) for the Neumann problem — together with the sample-integrability of their cube energies, which is the regularity making the expectations E[‖·‖²_{L²(cu_K)}] of the display well defined. Existence of the two cube solutions is not proved here; it is the hypothesis "let w_D^{(K)}, w_N^{(K)} be the solutions" of the lemma itself.

Disclosure. The assembling theorem tendsto_integral_cubeAverage_dirichlet_neumann_of_stationaryStream is on the disclosed Ω-level stream inputs hSm, hS, hstreamSmooth, hstreamAnti, hstreamDiv, whose shapes are copied verbatim from exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream. The stream is not constructed here and does not yet exist in this repository (to be supplied by the construction). Until it proves, nothing in this file realizes the source node l.corrector.limit at the fresh shell, and no node status is claimed. What is not assumed anywhere: the conclusion e.corrector.limit, either one-sided bound, and part (ii)'s conclusion.

The elementary squeeze

theorem Algsuperdiff.Section3.Provider.Corrector.tendsto_of_eventually_sandwich {u v : ℕ → ℝ} {M : ℝ} (huv : ∀ (K : ℕ), u K ≤ v K) (hlow : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (K : ℕ) in Filter.atTop, M - ε ≤ u K) (hhigh : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (K : ℕ) in Filter.atTop, v K ≤ M + ε) : Filter.Tendsto u Filter.atTop (nhds M) ∧ Filter.Tendsto v Filter.atTop (nhds M)

If u ≤ v pointwise and, for every ε > 0, eventually M - ε ≤ u and v ≤ M + ε, then both sequences converge to M. This is the numerical content of Step 4 of ABK26: the chain M ≤ liminf u ≤ limsup v ≤ M pins both limits.

Step 1 in expectation

theorem Algsuperdiff.Section3.Provider.Corrector.integral_cubeAverage_dirichlet_le_neumann {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [AddAction (HCPolySupport.Vec d) Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] [MeasurableConstVAdd (HCPolySupport.Vec d) Ω] [MeasurableVAdd₂ (HCPolySupport.Vec d) Ω] [MeasureTheory.VAddInvariantMeasure (HCPolySupport.Vec d) Ω μ] (Q : HCPolySupport.TriadicCube d) {f : Ω → HCPolySupport.HilbertVec d} (hfm : MeasureTheory.StronglyMeasurable f) (hf : MeasureTheory.MemLp f 2 μ) {Dω Nω : Ω → HCPolySupport.Vec d → HCPolySupport.Vec d} (hDpot : ∀ᵐ (ω : Ω) ∂μ, HCPolySupport.IsPotentialZeroTraceOn (HCPolySupport.openCubeSet Q) (Dω ω)) (hDsol : ∀ᵐ (ω : Ω) ∂μ, HCPolySupport.IsSolenoidalOn (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => Dω ω x + (realize f ω x).toVec) (hNpot : ∀ᵐ (ω : Ω) ∂μ, HCPolySupport.IsPotentialOn (HCPolySupport.openCubeSet Q) (Nω ω)) (hNsol : ∀ᵐ (ω : Ω) ∂μ, HCPolySupport.IsSolenoidalZeroNormalTraceOn (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => Nω ω x + (realize f ω x).toVec) (hNint : MeasureTheory.Integrable (fun (ω : Ω) => HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (Nω ω x) (Nω ω x)) μ) : ∫ (ω : Ω), HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (Dω ω x) (Dω ω x) ∂μ ≤ ∫ (ω : Ω), HCPolySupport.cubeAverage Q fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (Nω ω x) (Nω ω x) ∂μ

e.ordering.corrector.limit in expectation. Integrating the fixed-realization ordering setIntegral_vecDot_self_le_of_isSolenoidal over the sample space,

E[ ‖∇w_D^{(K)}‖²_{L²(cu_K)} ] ≤ E[ ‖∇w_N^{(K)}‖²_{L²(cu_K)} ].

Only the Neumann energy has to be integrable: the Dirichlet energy is nonnegative, so the inequality holds for the Bochner integral in either case.