OmegaStreamAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: assembling the Ω-level approximate stream at the fresh shell #
Algsuperdiff/Section3/Provider/Corrector/OmegaStream.lean builds the kernel
stream S_{im} = A_{g_m}X_i − A_{g_i}X_m and proves that its row divergence is,
at every point of space, the realization of the Ω-level field
kernelStreamDiv, which for a stationary solenoidal X equals A_{κ₁}X − A_{κ₂}X
almost surely. This file supplies the carrier-general ε-form of that
construction, its two-scale instantiation, the small-scale error leg and the
carrier instances the legs need.
What is assembled #
exists_kernelStream_integral_normSq_le— the carrier-generalε-form: with∫‖A_{κ₁}X − X‖² ≤ e₁and∫‖A_{κ₂}X‖² ≤ e₂the stream reproducesXup to2e₁ + 2e₂in squaredL²(Ω)norm.exists_twoScaleStream_integral_normSq_le— the same at the two product densities ofAlgsuperdiff/Section3/Provider/Corrector/MollifierScaling.lean, whose divergence kernel is the explicit telescoping field ofAlgsuperdiff/Section3/Provider/Corrector/DivergenceKernel.lean.exists_radius_integral_normSq_mollify_productDensity_sub_le— the small-scale leg, the approximate-identity estimate ofAlgsuperdiff/Section3/Provider/Corrector/MollifierConvergence.leantransported fromMollifier.ofRadiustoMollifier.ofProduct.
The matching large-scale leg and the shell instantiation are not here. They
are downstream, in
Algsuperdiff/Section3/Provider/Corrector/ShellSumCorrectorLimit.lean:
exists_scale_integral_normSq_mollify_productDensity_shellSumFlux_le is the
decorrelation bound at the product density, built on
Algsuperdiff/Section3/Provider/Corrector/ValuePathTransport.lean, and
exists_shellSumStream puts the two legs together --- for every tolerance
ε > 0 an antisymmetric stationary square-integrable stream with smooth
realizations whose row divergence reproduces the shell-sum flux shellSumFlux
to within ε in squared L²(Ω) norm.
The carrier instances #
The approximate-identity leg needs the strong continuity of the Koopman orbit
(Algsuperdiff.Probability.Stationary.continuous_koopman_orbit), which is
stated under [ Ω] [BorelSpace Ω] [ContinuousVAdd (Vec d) Ω] [IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop]. On the
continuous-path carrier C(Vec d, Mat d) all of these are available once Mat d is known to be second countable with a countably generated uniformity; those
two facts are recorded below as secondCountableTopology_mat and
isCountablyGenerated_uniformity_mat, each a transport of the corresponding
Pi instance through the type synonym Matrix (Fin d) (Fin d) ℝ = Fin d → Fin d → ℝ. They upgrade C(Vec d, Mat d) to a Polish space, and Mathlib's
MeasureTheory.Measure.InnerRegularCompactLTTop_of_polishSpace then supplies
the last instance for every measure on that carrier.
What is not proved #
The divergence identity delivered is the approximate one. The consumer
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream
(Algsuperdiff/Section3/Provider/Corrector/SolenoidalApproximation.lean) asks for
the exact hypothesis
hstreamDiv : ∀ᵐ ω, ∀ x, streamDivergence (streamRealization S ω) x = (realize j ω x).toVec,
and the output below satisfies that equality with an auxiliary field D in place
of j, together with ∫‖D − j‖² ≤ ε. The output therefore does not plug
into that theorem verbatim; see the note on
exists_kernelStream_integral_normSq_le for the exact restatement the consumer
would need.
Disclosure. Nothing in this file realizes any source node. It discharges the
two error legs of the approximate representation and instantiates it at the fresh
shell; it does not prove part (ii) of l.approximation.stationary.by.local, and
it claims no node status.
The approximate stream #
The Ω-level antisymmetric stream, in the approximate form.
For a stationary square-integrable field X in the stationary solenoidal
subspace and any family g of smooth compactly supported scalar fields whose
divergence is κ₁ − κ₂, the kernel stream S_{im} = A_{g_m}X_i − A_{g_i}X_m is a
stationary square-integrable antisymmetric field with smooth realizations whose
row divergence is, at every point of space, the realization of the Ω-level
field D, and D = A_{κ₁}X − A_{κ₂}X almost surely.
The first five conclusions are exactly the hypotheses hSm, hS,
hstreamSmooth, hstreamAnti of
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream; the sixth
is its hstreamDiv with D in place of X.
The Ω-level ε-approximate antisymmetric stream.
Same construction, with the two error legs entered numerically: if the smoothing
by κ₁ moves X by at most e₁ and the smoothing by κ₂ has energy at most
e₂, both in squared L²(Ω) norm, then the row divergence of the stream
reproduces X up to 2e₁ + 2e₂ in squared L²(Ω) norm.
This is the approximate form, not the exact one. What
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream consumes is
hstreamDiv : ∀ᵐ ω, ∀ x, streamDivergence (streamRealization S ω) x = (realize j ω x).toVec,
an equality. The conclusion below gives that equality with D in place of
j, together with ∫ ‖D − j‖² ≤ 2e₁ + 2e₂. To accept this output the consumer
would have to be restated with hstreamDiv replaced by the pair
(∀ᵐ ω, ∀ x, streamDivergence (streamRealization S ω) x = (realize D ω x).toVec)
and (∫ ω, ‖D ω − j ω‖² ∂μ ≤ e),
and its conclusion weakened by the resulting L²(cu_K) error, which is
(cubeVolume Q)⁻¹ ∫_{cu_K} ‖realize (D − j) ω‖² and integrates in ω to exactly
e by translation invariance. Nothing else in that proof uses hstreamDiv.
The two-scale instance #
The two-scale kernel family of
Algsuperdiff/Section3/Provider/Corrector/DivergenceKernel.lean, whose
divergence is the difference of the two product densities.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The divergence of the two-scale kernel family.
The two-scale ε-approximate antisymmetric stream.
The concrete instance of exists_kernelStream_integral_normSq_le at the two
product densities of scales r and s: the smoothing at the small scale r is
the approximate identity, the smoothing at the large scale s is the term killed
by decorrelation.
The small-scale leg #
The approximate-identity leg at the product density. This is
exists_radius_integral_normSq_mollify_sub_le of
Algsuperdiff/Section3/Provider/Corrector/MollifierConvergence.lean with
Mollifier.ofRadius replaced by Mollifier.ofProduct, whose density is the
tensor product used by the two-scale divergence kernel.
The carrier instances of the continuous-path space #
Mat d is second countable: the type synonym Matrix (Fin d) (Fin d) ℝ
carries the Pi topology.