TailGauge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The deterministic upper-tail gauges of the stream matrix #
ABK26 builds its stream matrix from the scale decomposition
k(x) = Σ_{n ∈ ℤ} j_n(x), a sum which does not converge; only the differences
k(x) - k(y) converge. The normalized field k(x) = Σ_n (j_n(x) - j_n(0))
does converge, and the two halves converge for different reasons:
- the descending half
n ≤ 0converges because‖j_n‖_{L^∞(□_ℓ)}is of order3^{γ n}, the content of the lower-tail condition already carried byAlgsuperdiff.Section3.Cutoff.CutoffSample; - the ascending half
n ≥ 0converges because‖∇ j_n‖_{L^∞(□_ℓ)}is of order3^{(γ-1) n}, so that|j_n(x) - j_n(0)| ≤ |x| ‖∇ j_n‖_{L^∞(□_ℓ)}is summable.
This module supplies the deterministic layer of the ascending half: the finite
partial sums of the volume-normalized gradient gauge ‖∇ j_k‖_{W^{1,∞}(y+□_n)}
of Algsuperdiff.Section4.Support.shellW1InfGradNorm on the cubes y + □_n,
the two bounded-partial-sum conditions built from them, their measurability, and
the summability and tail bounds they produce. It asserts nothing probabilistic.
The second condition is quantitative. A bare summability condition at each
scale gives no rate across scales, and hence no growth bound for the field; the
condition used here weighs scale ℓ by 3^{-ℓ} on the descending leg and by
3^{ℓ} on the ascending leg, which is exactly the weighting under which the
ℓ-th term has expectation of order 3^{(γ-1) ℓ}.
Main definitions #
lowerValuePartialSum ℓ q ω—Σ_{r < q} ‖j_{ℓ-r}‖_{L^∞(□_ℓ)}.upperGradPartialSum n y q ω—Σ_{r < q} ‖∇ j_{n+r}‖_{W^{1,∞}(y+□_n)}.UpperGradBounded n y ω— the partial sums of the second family are bounded.StreamGrowthBounded C ω— the weighted two-leg bound at rateC 3^{ℓ}.SharpTailBounded γ C ω— the two shell gauges obey their sharp scaling rates at every integer shell/cube crossover pair, with polynomial power one.
References #
- ABK26, the scale decomposition and the stream matrix.
1. The two partial-sum families #
The descending value partial sum on the origin cube of scale ℓ:
Σ_{r < q} ‖j_{ℓ-r}‖_{L^∞(□_ℓ)}. The cube scale and the top shell index
agree, which is the pairing under which the summand has expectation of order
3^{γ(ℓ-r)} (1+r)^{1/2}.
Equations
- Algsuperdiff.Section5.Field.lowerValuePartialSum ell q omega = ∑ r ∈ Finset.range q, Algsuperdiff.Section3.Cutoff.localCubeControl (↑ell) (↑omega (↑ell - ↑r))
Instances For
The ascending gradient partial sum on y + □_n:
Σ_{r < q} ‖∇ j_{n+r}‖_{W^{1,∞}(y+□_n)}, in the volume-normalized gauge of
Algsuperdiff.Section4.Support.shellW1InfGradNorm. Reindexed by k = n + r
this is the head of the tail sum Σ_{k ≥ n} of the large-scale event.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2. The two bounded-partial-sum conditions #
The ascending gradient series on y + □_n has bounded partial sums.
Equations
- Algsuperdiff.Section5.Field.UpperGradBounded n y omega = ∃ (C : ℕ), ∀ (q : ℕ), Algsuperdiff.Section5.Field.upperGradPartialSum n y q omega ≤ ↑C
Instances For
The quantitative two-leg condition at rate C: on every origin cube of
nonnegative scale ℓ, the descending value series and the ascending gradient
series obey
Σ_{r} ‖j_{ℓ-r}‖_{L^∞(□_ℓ)} + 3^{2ℓ} Σ_{r} ‖∇ j_{ℓ+r}‖_{W^{1,∞}(□_ℓ)} ≤ C 3^{ℓ} .
Both legs then contribute at most C 3^{ℓ} to the size of the normalized field
on □_ℓ: the first directly, the second after the mean value inequality on a
cube of diameter 3^{ℓ} and the volume normalization 3^{ℓ} of the gauge.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2a. The sharp two-sided shell rates #
The polynomial weight used by the sharp all-crossover event. Its exponent
is one; the additive 2 makes it uniformly positive.
Instances For
The derivative gauge at shell scale n, observed on the origin cube of
scale ell, normalized back from largeCubeDerivGauge to the manuscript's
W^{1,∞} rate. It equals the first-derivative norm plus 3^n times the
second-derivative norm.
Equations
- Algsuperdiff.Section5.Field.sharpGradientGauge ell n omega = 3 ^ (-n) * Algsuperdiff.Section3.Provider.Stream.largeCubeDerivGauge ell n (↑omega n)
Instances For
The sharp two-sided shell estimate with polynomial power one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Some natural-valued sample constant controls both sharp shell rates.
Equations
- Algsuperdiff.Section5.Field.SharpTailGood gamma omega = ∃ (C : ℕ), Algsuperdiff.Section5.Field.SharpTailBounded gamma C omega
Instances For
3. Summability and tail bounds #
The ascending leg of the quantitative condition, read at the origin cube:
the volume-normalized gradient series is bounded by C 3^{-ℓ}.
4. The ascending gradient sums in the raw gauge #
The ascending gradient sums on □_ℓ are bounded by the sample constant.
The volume normalization of the gauge divides out 3^{ℓ} on the first-derivative
leg, and the quantitative condition supplies the remaining 3^{ℓ}.