SolenoidalApproximation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the cutoff core of the solenoidal half of the local-approximation lemma #
This file builds the local approximants of part (ii) of
l.approximation.stationary.by.local and proves the approximation estimate
(ii) Solenoidal approximation. For every
L ∈ ℕthere exists a family{j_{K,L}}_{K ∈ ℕ}withj_{K,L} ∈ L²_{sol,0}(cu_K)such thatlimsup_{K→∞} E[ ‖j_{K,L} − j‖²_{L²(cu_K)} ] ≤ C 3^{−L} E[|j|²].
The proof is the structural mirror of the potential half
(Algsuperdiff/Section3/Provider/Corrector/PotentialApproximation.lean): the
same cutoff η_{K,L}, the same boundary strip Σ_{K,L}, the same
e.boundary.strip.volume bookkeeping and the same 3^{2(L−K)} crush of the
second error term. Only the competitor changes: the paper sets
j_{K,L,i} := Σ_m ∂_m ( η_{K,L} (S_{im} − (S_{im})_{cu_K}) )
for an antisymmetric stream tensor S with j_i = Σ_m ∂_m S_{im}, and expands
j_{K,L} − j = (η_{K,L} − 1) j + Σ_m (S_{im} − (S_{im})_{cu_K}) ∂_m η_{K,L}
The membership
j_{K,L} ∈ L²_{sol,0}(cu_K) and this error display are supplied unconditionally
by Algsuperdiff/Section3/Provider/Corrector/SolenoidalStream.lean
(isSolenoidalZeroNormalTraceOn_cutoffStream,
streamDivergence_cutoffStream_apply); what is proved here is the analytic
estimate on the two error terms.
The stream is a disclosed input. Exactly as part (i) is proved here for a
stationary square-integrable primitive φ before being lifted to the whole
potential subspace in
Algsuperdiff/Section3/Provider/Corrector/ApproximationAssembly.lean, part (ii)
is proved here for a stationary square-integrable stream S, entered as three
explicitly named hypotheses hstreamSmooth, hstreamAnti, hstreamDiv. The
Ω-level stream itself is not constructed in this file and does not yet exist in
the repository; the assembling theorem
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream is therefore
conditional and claims no node status. What is not assumed anywhere below
is the conclusion: neither the approximation estimate nor membership in
L²_{sol,0}(cu_K) appears as a hypothesis.
For a stationary square-integrable stream no cube average has to be subtracted
and no sublinearity input is used: the paper's (S)_{cu_K} is taken to be 0
and the second error term is bounded by ‖∇η_{K,L}‖²_∞ E[|S|²] ≍ 3^{2(L−K)} E[|S|²], which already tends to 0 as K → ∞ at fixed L because E[|S|²]
is finite. The representation leg — the existence of such an S — is the hard
input recorded, and it is precisely what is disclosed rather than proved here.
A vanishing-invariant-part condition is therefore necessary. Here it is not
a separate assumption: it is carried by hstreamDiv together with the
stationarity and square integrability of S, which force E[j] = 0 and hence
are unsatisfiable for a nonzero constant j. The mechanism is the one
displayed: pairing the divergence identity with a compactly supported test
function and using ∫ ∂_m ψ = 0 kills the mean. The implication is stated but
not proved in this file; what is proved is its shadow at the competitors,
setIntegral_coord_localStreamApprox_eq_zero. See the note on
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream.
Disclosure. Nothing in this file realizes any source node. The main theorem is conditional on an Ω-level antisymmetric stream that the repository does not yet provide.
Coordinatewise sums in the Euclidean carrier #
Coordinates of a finite sum in HilbertVec d. The usual Pi lemma does not
fire on PiLp, whose algebraic operations are wrapped.
The stream tensor and its realization #
The spatial realization of an Ω-level stream tensor, in the index shape
(i, m) ↦ (x ↦ S_{im}(x)) consumed by
Algsuperdiff.Section3.Provider.Corrector.streamDivergence.
The Ω-level carrier is Ω → (Fin d → HilbertVec d): the value S ω m is the
m-th column of the stream matrix, so the entry S_{im} of ABK26 is (S ω m) i. This presentation keeps the paper's remainder Σ_m (∂_m η) S_{im} a finite
sum of scalar multiples of vectors of the Euclidean carrier, with no
coordinatewise repackaging.
Equations
Instances For
The local approximant and its error #
The paper's remainder r_{K,L} of ABK26, i.e. the field x ↦ (Σ_m (∂_m η_{K,L})(x) S_{im}(x))_i, written as a finite combination of the columns of the
stream.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The paper's local competitor
j_{K,L,i} = Σ_m ∂_m ( η_{K,L} (S_{im} − (S_{im})_{cu_K}) ), expanded by the
product rule with the cube average taken to be 0. It is defined by this
formula for every sample, so that it is jointly measurable without any
smoothness assumption; whenever the realization of S really is a smooth
antisymmetric stream for the realization of j it is an element of
L²_{sol,0}(cu_K) (isSolenoidalZeroNormalTraceOn_localStreamApprox).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The error decomposition of part (ii), in the shape of the potential
display: j_{K,L} − j = (η_{K,L} − 1) j + r_{K,L}.
Each coordinate derivative of the localization cutoff is bounded by the
gradient bound C(d) 3^{L−K}.
The gradient leg of the error bound. The paper's remainder obeys
|r_{K,L}| ≤ d ‖∇η_{K,L}‖_∞ |S| pointwise, which is the solenoidal analogue of
the second display of ABK26.
The competitor is admissible: j_{K,L} ∈ L²_{sol,0}(cu_K), by
isSolenoidalZeroNormalTraceOn_cutoffStream at the cube average 0.
The three hypotheses are the disclosed per-sample stream data: smoothness,
antisymmetry S_{im} = −S_{mi}, and the representation j_i = Σ_m ∂_m S_{im}.
Pointwise error bound. On the cube the local approximation error is controlled by the boundary strip and by the stream, exactly as in the two displays of ABK26 transported to part (ii).
Measurability of the competitor #
The paper's remainder is strongly measurable in space, for every sample.
The paper's remainder is jointly strongly measurable in the sample and in space.
The approximation error is a strongly measurable field for every sample.
The approximation error is jointly strongly measurable.
The expected error at a fixed cube #
The expected squared error over a fixed cube, before normalization.
For almost every sample the local approximation error is square integrable on the cube.
The expected normalized error at a fixed cube. This is the paper's
displayed estimate before the limit K → ∞, with the strip constant C = d and
with the second term carrying the cutoff gradient bound.
The squared normalized error is integrable in the sample. Carrying this
clause in the existential below is what prevents a vacuous witness family whose
error is not integrable, on which the Bochner integral would degenerate to 0
(the part-(i) convention of ApproximationAssembly.lean).