SolenoidalApproximationEps #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: part (ii) of the local-approximation lemma for an approximate stream #
The cutoff core of part (ii) of l.approximation.stationary.by.local is proved
in Algsuperdiff/Section3/Provider/Corrector/SolenoidalApproximation.lean for a
field whose exact row divergence is the stream divergence. The Ω-level
streams that the repository can actually build represent the flux only up to an
L²(Ω) error: they come with an auxiliary stationary square-integrable field
D whose realization is the stream divergence at every point, together with a
tolerance E[|D − j|²] ≤ ε.
This file restates the cutoff core in that approximate form. Nothing of
SolenoidalApproximation.lean is re-proved: the competitor family is the same
localStreamApprox, instantiated at D — where the divergence identity holds
exactly, so its admissibility IsSolenoidalZeroNormalTraceOn is literally
isSolenoidalZeroNormalTraceOn_localStreamApprox — and the only new content is
the absorption of the L²(Ω) gap between D and the true flux j.
Why the gap is K-independent #
The error against the true flux splits as
j_{K,L} − j = (j_{K,L} − D) + (D − j),
and by the stationary transfer
(Algsuperdiff/Section3/Provider/Corrector/RealizationTransfer.lean,
integral_cubeAverage_normSq_realize)
E[ ‖realize (D − j)‖²_{L²(cu_K)} ] = E[ |D − j|² ]
for every cube K: the second term is a constant of K and therefore
passes through the limsup untouched. The resulting estimate is
limsup_K E[ ‖j_{K,L} − j‖²_{L²(cu_K)} ] ≤ 2 d 3^{−L} E[|D|²] + 2 E[|D − j|²].
The concrete-witness discipline #
CoarseGraining's IsSolenoidalZeroNormalTraceOn U g is orthogonality to
∇H¹(U) and carries no square integrability, so an existential witness of it
gives no per-sample L² control and ∫|·|² can silently be the Bochner junk
value 0. Exactly as in
Algsuperdiff/Section3/Provider/Corrector/NeumannUpperBound.lean, the consumer
below therefore uses the concrete family localStreamApprox Q L S D and the
per-sample membership ae_memLp_localStreamApprox_sub_of_approximateStream,
not the existential
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_approximateStream; the
existential is recorded because it is the printed form of part (ii), not
because anything downstream consumes it.
An elementary two-term split #
The competitor of an approximate stream #
The error of the competitor built from D against the true flux j is
jointly strongly measurable.
The two-term split of the approximate error at a fixed sample. On the
cube, the error of the competitor built from D against the true flux j costs
at most twice the exact error plus twice the realized D − j energy.
The expected error of the approximate competitor #
For almost every sample the error of the approximate competitor against the
true flux is square integrable on the cube. This is the per-sample L²
control that CoarseGraining's IsSolenoidalZeroNormalTraceOn does not carry.
Almost-sure square integrability of the realized gap D − j on the cube.
The unnormalized exact error is integrable in the sample. This is the
internal companion of integrable_cubeLpNorm_localStreamApprox_sub, recovered
from it by the normalization identity.
The squared normalized error of the approximate competitor is integrable in the sample.
The expected normalized error of the approximate competitor at a fixed
cube. The exact estimate of integral_cubeLpNorm_localStreamApprox_sub_le
at D plus the K-independent L²(Ω) gap E[|D − j|²], the latter by the
stationary transfer.
The Neumann upper bound for a field with approximate streams #
e.upper.bound.neumann.corrector.limit in the ε-form, for a flux
possessing approximate streams at every tolerance.
hstream is the only stream input, and it is an approximate representation:
for every tolerance η > 0 there is a stationary square-integrable
antisymmetric stream S with smooth realizations whose row divergence is the
realization of a stationary square-integrable D with E[|D − j|²] ≤ η. Its
shape is copied verbatim from
Algsuperdiff/Section3/Provider/Corrector/OmegaStreamAssembly.lean
(exists_freshShellStream).
hNint is the sample-integrability of the Neumann cube energies; it makes the
left-hand side the expectation of the display rather than a junk value.
The tolerance is chosen after the Young parameter and before the localization
scale, so nothing is circular: η depends only on ε and E[|∇w|²], L
depends on η and E[|j|²], and the cutoff-gradient term is killed by taking
K large at the fixed L.