NeumannUpperBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the Neumann upper bound of the corrector-limit proof #
ABK26, Lemma l.corrector.limit, Step 3, proves
limsup_{K→∞} E[ ‖∇w_N^{(K)}‖²_{L²(cu_K)} ] ≤ E[|∇w|²],
the display e.upper.bound.neumann.corrector.limit.
This file proves that display, in the ε-form and in the printed limsup
form. It is the exact mirror of
Algsuperdiff/Section3/Provider/Corrector/DirichletLowerBound.lean: the
Dirichlet class H¹₀(cu_K) is replaced by the Neumann class H¹(cu_K)
(CoarseGraining's IsPotentialOn together with the natural boundary condition
IsSolenoidalZeroNormalTraceOn (∇w_N + f)), and part (i) of
l.approximation.stationary.by.local is replaced by part (ii).
The route #
The manuscript reorganizes the testing identities, applies Hölder to the cross
term ⨍ (j − j_{K,L}) · ∇w_N, and then absorbs E[‖∇w_N‖²]^{1/2} by Young's
inequality. As in the Dirichlet half we use instead the variational form of
the same step, which keeps every estimate at a fixed sample and therefore needs
no Cauchy-Schwarz inequality on the product Ω × cu_K. Writing N = ∇w_N^{(K)}, F = f, J = j_{K,L} at a fixed realization, the two weak
formulations give
⨍ (N + F) · N = 0 (the natural boundary condition tested against N ∈ H¹) and
⨍ J · N = 0 (J ∈ L²_{sol,0}(cu_K) tested against the same N),
hence ⨍ (J − F) · N = ⨍ |N|², and expanding 0 ≤ ⨍ |(J − F) − N|² yields
⨍ |∇w_N^{(K)}|² ≤ ⨍ |j_{K,L} − f|².
This is the Neumann companion of the Dirichlet flux comparison
⨍|f|² − ⨍|∇v_{K,L} + f|² ≤ ⨍|∇w_D^{(K)}|²
(Algsuperdiff/Section3/Provider/Corrector/CubeComparison.lean): in both cases
the competitor enters only through its flux. Since j = f + ∇w, the
right-hand side is ⨍ |∇w + (j_{K,L} − j)|², and a pointwise Young split
against the approximation error finishes the fixed-cube estimate
E[ ⨍ |∇w_N^{(K)}|² ] ≤ (1+δ) E[|∇w|²] + (1+δ⁻¹) E[ ‖j_{K,L} − j‖²_{L²(cu_K)} ],
which is the paper's display with (1−δ)⁻¹, (4δ)⁻¹ replaced by (1+δ), (1+δ⁻¹). Consequently the absorption lemma
Algsuperdiff/Section3/Provider/Corrector/YoungAbsorption.lean is not used:
the self-improving inequality never arises on this route. The two routes give
the same conclusion, and this one needs strictly less measure theory — exactly
the divergence already recorded in the Dirichlet half.
What is consumed, and how #
Part (ii) of l.approximation.stationary.by.local is available in
Algsuperdiff/Section3/Provider/Corrector/SolenoidalApproximation.lean. We
consume it through its concrete witness family localStreamApprox rather
than through the existential
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream, because
the existential's admissibility clause IsSolenoidalZeroNormalTraceOn carries
no per-sample square integrability of the error j_{K,L} − j (CoarseGraining's
predicate is orthogonality to ∇H¹(cu_K) and nothing else), whereas the Young
split above needs it. The concrete family supplies it as
ae_memLp_localStreamApprox_sub. Nothing is assumed: the admissibility, the
integrability and the error estimate are all produced by that file from the
same three disclosed stream hypotheses.
Disclosure. The results below are conditional on the Ω-level stream S
entering through hSm, hS, hstreamSmooth, hstreamAnti, hstreamDiv,
whose shapes are copied verbatim from
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream. That
stream is not constructed here and does not yet exist in the repository (the
representation leg, to be supplied by the construction). Nothing in this file
realizes a source node, and neither e.upper.bound.neumann.corrector.limit nor
e.corrector.limit is assumed anywhere: the conclusion is proved, not
disclosed.
Elementary carrier lemmas #
Left additivity of the Euclidean dot product under subtraction.
Promotion to the Euclidean Hilbert carrier commutes with subtraction.
Square integrability of a potential field, i.e. of the gradient of an
H¹(U) function. This is the Neumann counterpart of
Algsuperdiff.Section3.Provider.Corrector.memVectorL2_of_isPotentialZeroTraceOn.
The cube average of a squared field is nonnegative.
The Step-3 comparison at a fixed realization #
Step 3 of l.corrector.limit at a fixed realization.
Let N be the gradient of the H¹(U) solution of -Δw = ∇·F with the natural
boundary condition, i.e. N is a potential field with N + F solenoidal with
vanishing normal trace, and let J be any admissible Neumann competitor,
J ∈ L²_{sol,0}(U). Then
∫_U |N|² ≤ ∫_U |J - F|².
Equivalently, N + F is the projection of F-shifted admissible fluxes: the
Neumann energy is minimal among the fluxes of L²_{sol,0}(U). With
J = j_{K,L} and F = f the right-hand side is ∫_U |j_{K,L} - f|², which the
approximation lemma drives to ∫_U |∇w|².
The proof is the paper's, in variational form: the two weak formulations give
∫_U (J - F) · N = ∫_U |N|², and the conclusion is 0 ≤ ∫_U |(J - F) - N|².
Only the weak formulations and square integrability are used; no boundary
regularity, no approximation lemma and no probability.
The per-sample Young split of the Neumann energy #
The Step-3 comparison after the Young split, at a fixed sample.
For the Neumann gradient N on the cube, an admissible competitor
J ∈ L²_{sol,0}(cu_K), and every δ > 0,
⨍|N|² ≤ (1+δ) ⨍|∇w|² + (1+δ⁻¹) ⨍|J - j|²,
where j = ∇w + f is the stationary flux and all fields are the spatial
realizations at the sample ω. This is the manuscript's Step 3 with the Hölder
step and the subsequent absorption replaced by a pointwise Young inequality; see
the module docstring.
The expected Neumann energy at a fixed scale #
The expected Step-3 comparison at a fixed cube. Integrating
cubeAverage_vecDot_self_le_young over the sample space and applying the
stationary transfer turns the realized cube average of |∇w|² into the
expectation E[|∇w|²].
hNint is the sample-integrability of the Neumann cube energy: it is what makes
the left-hand side the expectation of e.corrector.limit rather than the
Bochner junk value 0. It is the Neumann counterpart of the hDint
hypothesis of the Dirichlet half and is a regularity condition on the given
solution family, not a step of the proof.