StreamField #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The full stream matrix #
ABK26's stream matrix is the formal sum k(x) = Σ_{n ∈ ℤ} j_n(x), which does
not converge; the paper records that it is the differences k(x) - k(y) that
converge, and that only ∇ · k enters the generator, so the field is defined
modulo constants. This module builds the normalized representative
k(x) = Σ_{n ∈ ℤ} (j_n(x) - j_n(0)) ,
as an honest tsum over ℤ, on the carrier FullSample where both halves
converge locally uniformly: the descending half from the value gauges of the
cutoff carrier, the ascending half from the gradient gauges through the mean
value inequality.
Main definitions #
streamField ω— the normalized fieldk, matrix valued.
Main results #
streamField_skew,streamField_zero— antisymmetry and the normalization.streamField_eq_cutoff_add_upperTail— the identification with the cutoffs:k(x) - k_m(x) + k_m(0) = Σ_{n > m} (j_n(x) - j_n(0)).streamField_sub_cutoff_sub_eq— the same identity in subtractive form.
References #
- ABK26, the stream matrix and the remark that only differences converge.
1. Origin cubes of nonnegative scale exhaust the space #
2. The mean value bound on a cube #
The mean value inequality for one shell on an origin cube, in the
ambient norms, with the dimensional cost d of the conversion between the
ambient norm of the stored derivative and its exact Euclidean induced norm.
The entrywise form of the mean value bound.
3. Summability of the two halves on the carrier #
The ascending gradient series on the origin cube of scale ℓ is summable
with sum at most the carrier's constant, uniformly in the starting index.
The ascending gradient series on □_ℓ sums to at most the sample
constant.
The ascending gradient series on the origin cube of scale ℓ is summable
from any starting index: shifting the starting index changes the family by
finitely many terms.
The descending value series on any origin cube is summable, by the lower-tail condition already carried by the ambient carrier.
4. Summability of the normalized increments #
The ascending half, from any starting index, is summable.
The descending half is summable entrywise.
5. The field #
The normalized stream matrix k(x) = Σ_{n ∈ ℤ} (j_n(x) - j_n(0)).
The sum is over all of ℤ and is genuinely convergent on the carrier; the
normalization at the origin is the additive constant the source leaves free.
Equations
Instances For
The normalization: the field vanishes at the origin.
Antisymmetry: every shell is antisymmetric, hence so is the sum.
6. The identification with the cutoffs #
The cutoff identification. For every scale m, the normalized field is
the normalized m-th cutoff plus the tail of the ascending half:
k(x) = (k_m(x) - k_m(0)) + Σ_{n > m} (j_n(x) - j_n(0)).
The identification in the subtractive form of the source: the difference
between the field and its m-th cutoff, both normalized at the origin, is the
tail Σ_{n > m} (j_n(x) - j_n(0)).