TruncatedScaleTriangle #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The truncated Γ_σ scale triangle and the geometric-weight tail closure #
ABK26, l.Gamma.sigma.triangle at the scale sum: the step that turns
per-layer one-sided tails W j ≤ O_{Γ_σ}(B j) into a single tail on the
geometrically weighted layer sum ∑'_j 3^{−sj} W j. It is the one generic input
the l.minimal.scale.sep Step-1 head and the Step-3 below-window legs still
need after the window/geometric arithmetic of
Algsuperdiff.Probability.GeometricSums and
Algsuperdiff.Probability.WindowAmplitudes.
Why a truncated triangle #
The countable triangle in its naive form asks for a genuine pointwise sum
HasSum (fun j => X j ω) (S ω) at every ω. The layer families of the kicking
lemma do not provide one: an individual sample may be large at infinitely many
layers, so no per-ω summability is available before the tails are known. The
route taken here — the one the source itself takes — replaces the pointwise
limit by
- the uniform finite triangle on the partial sums
W N = ∑_{L<N} X L(one amplitude, valid for everyN), and - an eventual domination of the target variable by those partial sums, shifted
by a deterministic gap
g ≥ 0:c < S ω → ∀ᶠ N, c < W N ω + g.
The conclusion is one-sided (an IsBigOWith, i.e. an upper-tail estimate),
which is exactly what the consumers use.
No measurability in the limit passage #
measureReal_upperTail_of_uniform_partial needs no measurability at all: the
eventual domination puts the target tail event inside the increasing union of the
sets U N = {ω | ∀ n ≥ N, W n ω > A t}, each of which sits inside the N-th
partial-sum tail event, and mathlib's continuity from below
(Monotone.measure_iUnion) holds for arbitrary — not necessarily measurable —
sets. Measurability re-enters only through the finite triangle input of
isBigOWith_gammaSigma_scaleTriangle, which is CoarseGraining's
isBigO_finset_sum_of_isBigO_gammaSigma and asks for it on the summands.
Main results #
Algsuperdiff.Probability.measureReal_upperTail_of_uniform_partialAlgsuperdiff.Probability.isBigOWith_gammaSigma_of_uniform_partialAlgsuperdiff.Probability.isBigOWith_gammaSigma_scaleTriangleAlgsuperdiff.Probability.partialSum_eventually_gt_of_nonnegAlgsuperdiff.Probability.weightedTsum_isBigOWith_perLayer— the per-layer amplitude closure, the form the Step-1 head and the Step-3 below-window legs consume (their amplitude hypotheses areAlgsuperdiff.Probability.summable_weight_step3HeadAmpandAlgsuperdiff.Probability.tsum_weight_step3HeadAmp_le).Algsuperdiff.Probability.weightedTsum_isBigOWith— the constant-amplitude corollary at the geometric closure constantgeomTailConst s.
References #
- ABK26,
l.Gamma.sigma.triangleand the scale summation of its Appendix; - ABK26,
l.minimal.scale.sepStep 1 and Step 3, the two consumers.
Truncated one-sided triangle — raw tail form. Suppose
- every partial-sum surrogate
W Nobeys the same upper-tail boundμ.real {A t < W N} ≤ exp(−t^σ)fort ≥ 1(the finite triangle, uniformly inN); Sis eventually dominated at every threshold:c < S ω → ∀ᶠ N, c < W N ω + g.
Then μ.real {A t + g < S} ≤ exp(−t^σ) for every t ≥ 1.
No pointwise summability of ∑_N (W (N+1) − W N) is required — W is an
arbitrary family — and no measurability of W N or of S either: the passage
to the limit is the purely set-theoretic continuity from below on the increasing
family {ω | ∀ n ≥ N, A t < W n ω}.
Truncated one-sided triangle — IsBigOWith form. With the uniform bound
packaged as W N ≤ O_{Γ_σ}(A) for every N and a deterministic gap g ≥ 0, the
eventually dominated variable satisfies S ≤ O_{Γ_σ}(A + g).
The scale is A + g, not A, because the gap enters the threshold additively;
the conversion uses A t + g ≤ (A + g) t for t ≥ 1.
The truncated countable scale triangle (l.Gamma.sigma.triangle at the
scale sum). Per-layer variables X L = O_{Γ_σ}(K L) with summable positive
scales K have partial sums obeying the finite triangle at the N-independent
amplitude gammaTriangleConst σ · ∑'_L K L; if a variable S is eventually
dominated by those partial sums shifted by a deterministic gap g ≥ 0, then
S ≤ O_{Γ_σ}(gammaTriangleConst σ · ∑'_L K L + g) (one-sided).
No pointwise summability of ∑_L X L ω is assumed, and S is not required
to be measurable. Measurability of the summands is CoarseGraining's
requirement in isBigO_finset_sum_of_isBigO_gammaSigma, whose amplitude is the
only one available uniformly in the truncation level.
The partial-sum domination of a nonnegative series #
For a nonnegative series every c below the tsum is eventually beaten by
the partial sums — including the non-summable case, where the tsum is the junk
value 0 and the partial sums are nonnegative. This is the domination input of
the one-sided truncated triangle when the target variable is the series.
The geometric-weight one-sided closure #
The geometric-weight one-sided tail closure amplitudes. Per-layer one-sided
tails W j ≤ O_{Γ_σ}(B j) on nonnegative measurable layers close to a Γ_σ
tail on the geometrically weighted layer series at the amplitude
gammaTriangleConst σ · ∑'_j 3^{−sj} B j.
The amplitude sequence is not required to be uniform, which is what the
Step-1 head and the Step-3 below-window legs need (their per-layer amplitude
grows like √j; see Algsuperdiff.Probability.step3HeadAmp). Only the weighted
amplitudes must be summable — no pointwise summability of the layer series is
assumed.
The geometric-weight one-sided tail closure, uniform amplitude. The
constant-amplitude case B j := B of weightedTsum_isBigOWith_perLayer, with
the geometric series summed: the closure amplitude is
gammaTriangleConst σ · geomTailConst s · B, where
geomTailConst s = (1 − 3^{−s})⁻¹ by definition. No pointwise summability of the
layer series is assumed.