SolenoidalStream #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the antisymmetric-stream layer of l.approximation.stationary.by.local (ii) #
ABK26, proof of part (ii) of l.approximation.stationary.by.local, builds its
competitor as the row divergence of a cutoff antisymmetric tensor field,
j_{K,L,i} := Σ_m ∂_m ( η_{K,L} (S_{im} − (S_{im})_{cu_K}) ),
and then asserts in one sentence: "Since the matrix field
η_{K,L}(S − (S)_{cu_K}) is anti-symmetric and compactly supported in cu_K, we
have j_{K,L} ∈ L²_{sol,0}(cu_K)".
This file proves that sentence, unconditionally and at the level of an
arbitrary domain: isSolenoidalZeroNormalTraceOn_streamDivergence below. In
CoarseGraining's vocabulary L²_{sol,0}(U) is IsSolenoidalZeroNormalTraceOn U, i.e. exactly the manuscript's own definition L²_{sol,0}(U) = L²_{pot}(U)^⊥: orthogonality to ∇H¹(U). The proof is the double
integration by parts
Σ_{i,m} ∫_U ∂_m T_{im} ∂_i φ = − Σ_{i,m} ∫_U φ ∂_i ∂_m T_{im} = 0,
the last equality by Clairaut symmetry together with T_{im} = −T_{mi}. No
probability, no stationarity, no sublinearity and no ergodic-theoretic input
enters; the only hypotheses are smoothness, compact support inside U, and
antisymmetry.
The second half of the file records the converse constraint on the same space,
which is what fixes the hypotheses part (ii) can legitimately be stated under.
Testing IsSolenoidalZeroNormalTraceOn U g against the affine H¹(U) functions
gives ∫_U g_i = 0 for every coordinate
(setIntegral_coord_eq_zero_of_isSolenoidalZeroNormalTraceOn), hence every
member of L²_{sol,0}(U) is orthogonal to the constant fields and
∫_U |c − g|² ≥ |c|² |U| for every constant c
(setIntegral_normSq_const_sub_ge). Part (ii) therefore requires a hypothesis
on j beyond solenoidality; see the module docstring of
Algsuperdiff/Section3/Provider/Corrector/DirichletLowerBound.lean for the
status of the node.
Disclosure. Nothing in this file realizes any source node. It proves the membership step of part (ii) and an obstruction to part (ii); it does not prove part (ii), and it claims no node status.
Coordinate derivatives of a scalar field #
The m-th coordinate partial derivative of a scalar field on ℝᵈ.
Equations
Instances For
A coordinate derivative of a smooth field is smooth.
A coordinate derivative of a compactly supported field is compactly supported.
A coordinate derivative does not enlarge the closed support.
Clairaut symmetry in coordinate form #
The iterated coordinate derivative expressed through the second Fréchet derivative.
Clairaut symmetry: coordinate derivatives of a smooth field commute.
The row divergence of a matrix field #
The row divergence of a matrix field T = (T_{im}), i.e. the vector field
x ↦ (Σ_m ∂_m T_{im}(x))_i. This is the manuscript's j_{K,L} once T is the
cutoff antisymmetric stream tensor.
Equations
- Algsuperdiff.Section3.Provider.Corrector.streamDivergence T x i = ∑ m : Fin d, Algsuperdiff.Section3.Provider.Corrector.coordDeriv (T i m) m x
Instances For
Membership of the row divergence in L²_{sol,0}(U) #
Square integrability on U of a continuous compactly supported field.
The pairing of an L² coordinate against a continuous compactly supported
field is integrable.
The single integration by parts against an H¹(U) test function:
∫_U (∇φ)_i ∂_m T_{im} = − ∫_U φ ∂_i ∂_m T_{im}.
The membership step of l.approximation.stationary.by.local (ii).
If T = (T_{im}) is a smooth antisymmetric matrix field whose entries are
compactly supported inside U, then its row divergence
x ↦ (Σ_m ∂_m T_{im}(x))_i lies in L²_{sol,0}(U), i.e. it is orthogonal to
∇H¹(U).
Only smoothness, compact support in U and antisymmetry are used.
The cutoff stream tensor and its row divergence #
The manuscript's cutoff stream tensor η_{K,L}(S − (S)_{cu_K}), with the
cube averages entered as an arbitrary constant matrix c.
Equations
- Algsuperdiff.Section3.Provider.Corrector.cutoffStream η S c i m x = η x * (S i m x - c i m)
Instances For
The Leibniz rule for a coordinate derivative of a product.
The coordinate derivative ignores an additive constant.
The product-rule decomposition of the cutoff competitor. The row
divergence of the cutoff stream tensor splits into the cutoff of the row
divergence of S and the remainder built from ∇η.
The cutoff competitor is admissible: the row divergence of η (S − c)
lies in L²_{sol,0}(U) whenever η is smooth and compactly supported in U
and both S and c are antisymmetric. This is the manuscript's sentence in
ABK26, in the form in which part (ii) uses it.