GammaSigmaFiniteTriangle #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Measurability-free finite triangle inequality for O_{Γ_σ} #
ABK26, Lemma l.Gamma.sigma.triangle
(e.Gamma.sigma.triangle), in the finite case.
What this adds over CoarseGraining #
CoarseGraining already proves a finite generalized triangle inequality,
Homogenization.IndependentSums.isBigO_finset_sum_of_isBigO_gammaSigma, but it
carries two hypotheses that are painful downstream:
Measurable (X i)for every summand, and0 < a i(strict) for every scale.
The requirement is unnecessary. The finite triangle has a direct union-bound
proof: the tail event of the sum is contained in a finite union of the
summands' tail events, and MeasureTheory.measureReal_biUnion_finset_le holds
for completely arbitrary sets. This module gives that proof. No measurability
hypothesis appears anywhere below, and scales are only assumed nonnegative.
The constant #
For an N-term sum the scale produced here is (1 + log N)^{1/σ} · ∑ a_i.
This is both sharper and more explicit than CoarseGraining's
gammaTriangleConst σ (which is σ-dependent and enormous). The mechanism:
splitting the budget as a_i · (λ t) with λ = (1 + log N)^{1/σ} makes each
of the N summand tails at most exp(-(1 + log N) t^σ), and N · exp(-(1 + log N) t^σ) ≤ exp(-t^σ) exactly because t^σ ≥ 1.
Main results #
Algsuperdiff.Probability.isBigO_gammaSigma_finset_sum_of_nonneg_scalesAlgsuperdiff.Probability.isBigO_gammaSigma_add2'
References #
- ABK26, Lemma
l.Gamma.sigma.triangle.
Measurability-free finite generalized triangle inequality for the
stretched-exponential class Γ_σ (l.Gamma.sigma.triangle, finite case).
If X i = O_{Γ_σ}(a i) for each i in a nonempty finite index set s, with
nonnegative scales a i, then
∑_{i ∈ s} X i = O_{Γ_σ}( (1 + log #s)^{1/σ} · ∑_{i ∈ s} a i ).
Unlike CoarseGraining's isBigO_finset_sum_of_isBigO_gammaSigma, no
measurability of the summands is required — the proof is a pure union bound,
and measureReal_biUnion_finset_le needs no measurable sets.
Two-term measurability-free Γ_σ triangle inequality, constant
(1 + log 2)^{1/σ}.
Three-term measurability-free Γ_σ triangle inequality, constant
(1 + Real.log 3) ^ σ⁻¹.