OmegaStream #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the Ω-level approximate antisymmetric stream of the kernel route #
Algsuperdiff/Section3/Provider/Corrector/SolenoidalApproximation.lean proves the
cutoff core of part (ii) of l.approximation.stationary.by.local under three
disclosed stream hypotheses hstreamSmooth, hstreamAnti, hstreamDiv, and
records in its module docstring that the Ω-level stream itself "is not
constructed in this file and does not yet exist in the repository".
This file constructs it, in the approximate form, by the elementary kernel
route. For a family g = (g_m) of smooth compactly supported scalar fields on
ℝᵈ and a stationary square-integrable X : Ω → ℝᵈ, put
S_{im} := A_{g_m} X_i − A_{g_i} X_m (kernelStream),
where A_κ is the mollification along the translation action of
Algsuperdiff/Section3/Provider/Corrector/Mollification.lean. Three facts, all
elementary:
Sis antisymmetric by construction (streamRealization_kernelStream_neg), its realizations are smooth (contDiff_streamRealization_kernelStream), and it is a stationary square-integrable field (stronglyMeasurable_kernelStream,memLp_two_kernelStream);the row divergence of its realization is, at every point of space and with no error term, the realization of an explicit
Ω-level field (streamDivergence_kernelStream):Σ_m ∂_m S_{im} = A_{Σ_m ∂_m g_m} X_i − Σ_m A_{∂_m g_i} X_m;the second, "cross", term vanishes almost surely for a field in the stationary solenoidal subspace (
mollifyDiv_ae_eq_zero). This is the only place where solenoidality is used, and the proof is a duality: the adjoint ofA_κisA_{κ(−·)}(integral_mul_mollify_eq), so pairingΣ_m A_{∂_m g_i} X_magainst a test scalarφproduces−E[⟪X, ∇A_{g_hat_i}φ⟫], which vanishes because mollified gradients lie in the stationary potential subspace (toLp_mollifyGrad_mem_stationaryPotentialSubspace) andXis orthogonal to it. Takingφto be the cross term itself givesE[|cross|²] = 0.
Choosing g so that Σ_m ∂_m g_m = χ_1 − χ_2 — which the explicit telescoping
kernel of Algsuperdiff/Section3/Provider/Corrector/DivergenceKernel.lean does
for any two product densities — the stream divergence becomes A_{χ_1} X − A_{χ_2} X almost surely, so
‖div S − X‖_{L²(Ω)} ≤ ‖A_{χ_1} X − X‖_{L²(Ω)} + ‖A_{χ_2} X‖_{L²(Ω)},
the first term small by the approximate-identity layer of
Algsuperdiff/Section3/Provider/Corrector/MollifierConvergence.lean and the
second small by the decorrelation layer of
Algsuperdiff/Section3/Provider/Corrector/MollifiedDecorrelation.lean. That
last step, and the discharge of both legs at the fresh shell, are carried out in
Algsuperdiff/Section3/Provider/Corrector/OmegaStreamAssembly.lean; this file
stops at the exact divergence identity and the almost-sure identification of its
right-hand side (kernelStreamDiv_ae_eq).
No resolvent, no Newtonian potential, no Newton theorem and no ergodic theorem is used.
What is not proved here. The divergence identity produced is the
ε-approximate one: the stream reproduces an Ω-level field D exactly, and
D is within a controlled L²(Ω) distance of X, but D ≠ X. The consumer
exists_isSolenoidalZeroNormalTraceOn_limsup_le_of_stationaryStream asks for the
exact hypothesis hstreamDiv, so the output of this file does not discharge
that hypothesis verbatim; see the note on
exists_kernelStream_integral_normSq_le in
Algsuperdiff/Section3/Provider/Corrector/OmegaStreamAssembly.lean.
Disclosure. Nothing in this file realizes any source node. It supplies the
approximate form of the representation leg disclosed by
SolenoidalApproximation.lean; it does not prove part (ii) of
l.approximation.stationary.by.local, and it claims no node status.
The reflected kernel #
The reflected kernel y ↦ κ (-y). It is the adjoint kernel of the
mollification A_κ on L²(Ω) (integral_mul_mollify_eq).
Equations
Instances For
Reflection reverses the sign of a partial derivative.
Elementary algebra of the mollification kernel #
Negating the kernel negates the mollification.
Splitting a kernel that is a pointwise difference.
Euclidean-vector fields assembled from scalars #
A Euclidean-vector stationary field assembled from its d scalar
coordinates.
Equations
- Algsuperdiff.Section3.Provider.Corrector.vecPack ψ ω = HCPolySupport.HilbertVec.ofVec fun (i : Fin d) => ψ i ω
Instances For
The mollified horizontal divergence and its vanishing #
The mollified horizontal divergence Σ_m A_{∂_m κ} X_m. It is the cross
term of the row divergence of kernelStream.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The adjoint of mollification is mollification by the reflected kernel.
The proof is the change of variables y ↦ -y on ℝᵈ together with the
translation invariance of μ; no integration by parts is used.
The pairing identity for the mollified divergence: its L²(Ω) adjoint is
minus the mollified gradient at the reflected kernel.
The cross term vanishes. For a field in the stationary solenoidal subspace the mollified horizontal divergence is almost surely zero. This is the only use of solenoidality in the construction of the stream.
The kernel stream and its realizations #
Smoothness of a mollified realization, for an arbitrary smooth compactly supported kernel.
A mollified realization as an honest convolution integral.
Kernel additivity of the mollified realization, at every point of space.
The kernel stream S_{im} = A_{g_m} X_i − A_{g_i} X_m, in the column
convention of Algsuperdiff.Section3.Provider.Corrector.streamRealization: the
value S ω m is the m-th column, so the entry S_{im} is (S ω m) i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel stream is antisymmetric, for every sample, by construction.
The realizations of the kernel stream are smooth.
The coordinate derivative of a mollified realization falls on the kernel.
The single coordinate derivative of an entry of the kernel stream.
The Ω-level row divergence of the kernel stream: the smoothing of X
by the divergence of g, minus the cross term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The exact divergence identity. At every point of space the row
divergence of the realization of the kernel stream is the realization of the
Ω-level field kernelStreamDiv. There is no error term here: the whole
approximation is carried by the distance between kernelStreamDiv and X.
Measurability and square integrability of the kernel stream #
The kernel stream is a measurable stationary field.
The kernel stream is square integrable.
The row divergence is the two-scale smoothing of the field. Almost
surely the Ω-level row divergence of the kernel stream is A_{κ₁} X − A_{κ₂} X:
the cross term is killed by solenoidality and the remaining kernel splits.