CutoffLimit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The full field as the limit of the normalized cutoff fields #
The truncated coefficient field of ABK26 is a_L = ν I + k_L with
k_L = Σ_{n ≤ L} j_n, and the untruncated field is a = ν I + k with
k(x) = Σ_{n ∈ ℤ} (j_n(x) - j_n(0)). The two are not related by a
convergent limit as they stand: the constant matrix k_L(0) = Σ_{n ≤ L} j_n(0)
grows with L. The object that does converge is the cutoff field normalized at
the origin,
ã_L(x) = a_L(x) - k_L(0) = ν I + (k_L(x) - k_L(0)) ,
whose distance to a on a cube is exactly the ascending tail
a(x) - ã_L(x) = k(x) - (k_L(x) - k_L(0)) = Σ_{n > L} ( j_n(x) - j_n(0) ) .
Since k_L(0) is a constant skew matrix, ã_L and a_L have the same
divergence-form weak solutions, so nothing is lost by the normalization.
On the sharp carrier the ascending shell gradients obey
‖∇ j_n‖_{L^∞(□_ℓ)} ≤ C 3^{(γ-1)n} (2 + |n| + |ℓ|), so the tail above is
bounded on □_ℓ by a geometric factor 3^{(γ-1)(L+1)} times a weight linear in
L, and tends to zero as L → ∞.
Main definitions #
normalizedCutoff L ω— the cutoff field normalized at the origin,k_L - k_L(0).normalizedCoefficientCutoff ν L ω— the coefficient fieldã_L.largeScaleRatio γ— the geometric ratio3^{γ-1}.largeScaleTailSum γ— the arithmetico-geometric constantΣ_{r ≥ 0} (r+1) 3^{(γ-1)r} = (1 - 3^{γ-1})^{-2}.cutoffLimitGap d γ C ℓ L— the explicit entrywise gap on□_ℓ.
Main results #
streamField_sub_normalizedCutoff_entry— the exact relation above.abs_streamField_sub_normalizedCutoff_le— the geometric bound at a point of□_ℓ.abs_streamCoefficient_sub_normalizedCoefficientCutoff_le_gap— the same for the coefficient fields, in the entrywise supremum form the energy estimate consumes.tendsto_cutoffLimitGap_atTop— the gap tends to zero asL → ∞.
References #
- ABK26, the stream matrix and the truncated fields
a_L; the proof of the homogenization theorem, where the equation is noted to be unchanged whena_Lis replaced bya_Lminus the average ofk_L - k_mon the cube.
1. The geometric ratio of the large-scale increments #
The geometric ratio 3^{γ-1} of the ascending shell gradient rate.
Equations
- Algsuperdiff.Section5.Field.largeScaleRatio gamma = Real.rpow 3 (gamma - 1)
Instances For
The arithmetico-geometric constant Σ_{r ≥ 0} (r+1) 3^{(γ-1)r} of the
ascending tail.
Equations
- Algsuperdiff.Section5.Field.largeScaleTailSum gamma = ∑' (r : ℕ), (↑r + 1) * Algsuperdiff.Section5.Field.largeScaleRatio gamma ^ r
Instances For
2. The normalized cutoff fields #
The cutoff field normalized at the origin, k_L - k_L(0).
Equations
- Algsuperdiff.Section5.Field.normalizedCutoff L omega x = (Algsuperdiff.Section3.Cutoff.cutoff L omega).toFun x - (Algsuperdiff.Section3.Cutoff.cutoff L omega).toFun 0
Instances For
The constant skew matrix by which the normalized cutoff differs from the cutoff.
The normalized coefficient cutoff ã_L = a_L - k_L(0) = ν I + (k_L - k_L(0)).
It has the same divergence-form weak solutions as a_L, because k_L(0) is a
constant skew matrix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The exact relation with the full field #
The exact relation between the full field and its normalized cutoffs:
their difference is the ascending tail Σ_{n > L} (j_n(x) - j_n(0)).
The same relation for the coefficient fields.
4. The geometric rate on an origin cube #
The explicit geometric bound on the entrywise distance between the full
field and its L-th normalized cutoff, at a point of the origin cube of scale
ℓ.
5. The gap on a cube, and its vanishing as L → ∞ #
The explicit geometric gap between the full field and its L-th
normalized cutoff, entrywise on the origin cube of scale ℓ. When γ < 1,
its closed form is
3 d C (2 + |L| + |ℓ|) · (3^ℓ / 2) · 3^{(γ-1)(L+1)} · (1 - 3^{γ-1})^{-2} .
Equations
- One or more equations did not get rendered due to their size.
Instances For
The entrywise geometric bound on the origin cube of scale ℓ.
The entrywise geometric bound for the coefficient fields. This is the
supremum distance ‖a - ã_L‖_∞ that the energy estimate consumes.
The gap vanishes as L → ∞: on every fixed cube the full field is the
uniform limit of its normalized cutoffs, at the geometric rate 3^{(γ-1)L}
times a weight linear in L.