TailSqrt

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The Orlicz square root and the two-term witness upgrade

This module supplies the model-free probabilistic step of ABK26's derivation of Proposition p.tail.bounds from Proposition p.cg.ellipticity.bounds: the sentence

Taking square roots, and specializing to sigma = 1/4 and s >= 4 gamma, we get e.tail.bounds

Nothing in this file mentions the model, the cutoff, or the coarse-grained ellipticity constants; it operates on an abstract nonnegative random variable whose square has a three-term one-sided bound.

The four moves

1. The square root of a Gamma_sigma tail (isBigOWith_gammaSigma_sqrt). X <= O_{Gamma_sigma}(A) with X >= 0 gives sqrt X <= O_{Gamma_{2 sigma}}(sqrt A). This is the p = 1/2 case of the Appendix power rule e.powerofGammasigma, already proved as Provider.Orlicz.isBigOWith_gammaSigma_rpow_iff_of_nonneg; the index arithmetic is sigma / (1/2) = 2 sigma. This is where the manuscript's sigma = 1/4 specialization lives: the heavy leg of e.cg.ellip.upper sits at Gamma_{(1 - sigma)/3}, which at sigma = 1/4 is Gamma_{1/4}, and 2 * (1/4) = 1/2 is the Gamma_{1/2} of e.tail.bounds. The Gamma_1 middle leg of e.cg.ellip.upper becomes the Gamma_2 middle of e.tail.bounds by the same rule at 2 * 1 = 2.

2. The merge of two heavy legs (isBigOWith_gammaSigma_add_of_nonneg). The manuscript's ell^2 display has three terms, but e.cg.ellip.lower and e.cg.ellip.upper contribute two heavy terms, at Gamma_{(1 - sigma)/2} and Gamma_{(1 - sigma)/3} respectively. The manuscript merges them silently. The merge is not free: two Gamma_sigma tails at scales A and B sum to a Gamma_sigma tail at scale 2 (3 max{1, log 2})^{1/sigma} max{A, B}, by the Appendix maximum lemma l.maximums.Gamma.s.

3. The deterministic half (sqrt_le_add_of_sq_le_add_add): the pointwise subadditivity sqrt (D + Y + Z) <= sqrt D + sqrt Y + sqrt Z.

4. The witness upgrade (isTwoTermBigOWith_of_ae_le). ABK26's relations X <= O_{Psi_1}(A_1) + O_{Psi_2}(A_2) are formalized with a pointwise domination forall omega, X omega <= Y omega + Z omega (Probability.IsTwoTermBigOWithWitnesses), while a Section 3 observable may be known to satisfy the corresponding bound only almost everywhere (for instance when the bound itself is only an a.e. statement). Modifying the two witnesses on the (measurable, null) set where the almost-everywhere inequality fails removes the mismatch without changing either tail. On the centered cube the two observables reduce pointwise to the same literal, so the same witness transports there with no null-set surgery. Off centre, the translate identity lambdaSq_cutoff_translateCutoffSample is a pathwise equality read at a different sample, so no definitional identification bridges it. Since the observable bodies are their literals clamped at 0, however, the off-centre observable is its literal on the source range, and the pathwise covariance applies to it verbatim. Composed with the law invariance Cutoff.map_translateCutoffSample_cutoffSampleLaw, this transports the whole IsLowerIntegerFamilyOrliczWithWitness package to every translate, with the witness composed with the translation (Provider/BadEvents/ObservableSwapPayoff.lean). The transport is thus a consequence of covariance plus stationarity, not a definitional accident. Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds is proved, so its centered instance is available to a downstream assembly; this helper still exposes that instance conditionally, and the Lambda (upper) leg has no proved translate covariance. The lemma covers the two-term single-index case only.

Main results

• isBigOWith_of_ae_eq --- Gamma-tails are invariant under almost-everywhere modification of the random variable.
• isBigOWith_max_zero --- clamping a witness at 0 preserves its tail.
• isBigOWith_gammaSigma_sqrt --- the Orlicz square root.
• isBigOWith_gammaSigma_add_of_nonneg --- the merge of two Gamma_sigma legs.
• isTwoTermBigOWith_of_ae_le --- the witness upgrade.
• sqrt_le_add_of_sq_le_add_add --- the deterministic half.
• isDeterministicShiftTwoTermOneSidedOrlicz_of_sq_le --- the packaged square-root step: an almost-everywhere three-term bound on X ^ 2 becomes the source's two-term one-sided relation for X.

References

• ABK26, p.tail.bounds; its derivation.
• ABK26, e.powerofGammasigma; l.maximums.Gamma.s; the Appendix tail conventions.

Almost-everywhere invariance and clamping

theorem Algsuperdiff.Section3.Provider.Tail.isBigOWith_of_ae_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {X Y : Ω → ℝ} {A : ℝ} (hXY : X =ᵐ[μ] Y) (hX : HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ Y A

A one-sided weak-Orlicz tail only sees the random variable through its almost-everywhere class.

theorem Algsuperdiff.Section3.Provider.Tail.isBigOWith_max_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ : ℝ → ℝ} {Y : Ω → ℝ} {A : ℝ} (hA : 0 < A) (hY : HCPolySupport.IndependentSums.IsBigOWith μ Ψ Y A) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ (fun (ω : Ω) => max 0 (Y ω)) A

Clamping a witness below at 0 does not change its one-sided tail, as long as the scale is positive.

theorem Algsuperdiff.Section3.Provider.Tail.positivePart_pow_integrable_and_integral_le_of_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : Ω → ℝ} {A σ : ℝ} (p : ℕ) (hp : 1 ≤ p) (hσ : 0 < σ) (hA : 0 < A) (hYm : AEMeasurable (fun (ω : Ω) => max 0 (Y ω)) μ) (hY : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) Y A) : MeasureTheory.Integrable (fun (ω : Ω) => max 0 (Y ω) ^ p) μ ∧ ∫ (ω : Ω), max 0 (Y ω) ^ p ∂μ ≤ (HCPolySupport.IndependentSums.gammaMomentConst σ * ↑p ^ σ⁻¹ * A) ^ p

A clipped one-sided Gamma tail controls every positive natural-power moment.

theorem Algsuperdiff.Section3.Provider.Tail.pow_integrable_and_integral_le_of_twoTerm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {A B σ τ : ℝ} (p : ℕ) (hp : 1 ≤ p) (hσ : 0 < σ) (hτ : 0 < τ) (hXnonneg : ∀ (ω : Ω), 0 ≤ X ω) (h : Probability.IsTwoTermBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (HCPolySupport.IndependentSums.gammaSigma τ) X A B) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ p) μ ∧ ∫ (ω : Ω), X ω ^ p ∂μ ≤ 2 ^ (p - 1) * ((HCPolySupport.IndependentSums.gammaMomentConst σ * ↑p ^ σ⁻¹ * A) ^ p + (HCPolySupport.IndependentSums.gammaMomentConst τ * ↑p ^ τ⁻¹ * B) ^ p)

Two one-sided Gamma tails bound moments of a nonnegative dominated variable, with the natural-power split constant and each tail's original scale.

The Orlicz square root

theorem Algsuperdiff.Section3.Provider.Tail.isBigOWith_gammaSigma_sqrt {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {A σ : ℝ} (hA : 0 ≤ A) (hXnn : ∀ (ω : Ω), 0 ≤ X ω) (hX : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) X A) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma (2 * σ)) (fun (ω : Ω) => √(X ω)) √A

The Orlicz square root. From X <= O_{Gamma_sigma}(A) for a nonnegative X and a nonnegative scale A, sqrt X <= O_{Gamma_{2 sigma}}(sqrt A).

This is the p = 1/2 instance of e.powerofGammasigma: the index arithmetic of Provider.Orlicz.isBigOWith_gammaSigma_rpow_iff_of_nonneg is sigma / (1/2) = 2 sigma, and x ^ (1/2 : R) = sqrt x.

The merge of two heavy legs

theorem Algsuperdiff.Section3.Provider.Tail.isBigOWith_gammaSigma_add_of_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Y Z : Ω → ℝ} {A B σ : ℝ} (hσ : 0 < σ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hY : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) Y A) (hZ : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) Z B) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => Y ω + Z ω) (2 * ((3 * max 1 (Real.log 2)) ^ σ⁻¹ * max A B))

The merge of two Gamma_sigma legs. The sum of two random variables with Gamma_sigma tails at scales A and B has a Gamma_sigma tail at scale 2 (3 max{1, log 2})^{1/sigma} max{A, B}.

This is the step the manuscript performs silently between the two heavy terms of e.cg.ellip.lower and e.cg.ellip.upper and the single heavy term of the ell^2 display. The constant is the Appendix maximum lemma's, applied to Y + Z <= 2 max{Y, Z}.

The witness upgrade

theorem Algsuperdiff.Section3.Provider.Tail.isTwoTermBigOWith_of_ae_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ₁ Ψ₂ : ℝ → ℝ} {X Y Z : Ω → ℝ} {A₁ A₂ : ℝ} (hΨ₁ : Probability.IsAdmissibleTail Ψ₁) (hΨ₂ : Probability.IsAdmissibleTail Ψ₂) (hA₁ : 0 < A₁) (hA₂ : 0 < A₂) (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hle : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ Y ω + Z ω) (hYt : HCPolySupport.IndependentSums.IsBigOWith μ Ψ₁ Y A₁) (hZt : HCPolySupport.IndependentSums.IsBigOWith μ Ψ₂ Z A₂) : Probability.IsTwoTermBigOWith μ Ψ₁ Ψ₂ X A₁ A₂

The witness upgrade. An almost-everywhere two-term domination becomes the source's pointwise one, by modifying the two witnesses on the measurable null set where the inequality fails. Neither tail changes, because a tail is an almost-everywhere invariant (isBigOWith_of_ae_eq).

The Section 3 observables are measurable representatives of their literal manuscript definitions, so every identification of an observable with an analytic quantity is only almost-everywhere; without this lemma no such identification can transport a Probability.IsTwoTermBigOWith conclusion.

The deterministic half

theorem Algsuperdiff.Section3.Provider.Tail.sqrt_le_add_of_sq_le_add_add {x D Y Z : ℝ} (hx : 0 ≤ x) (hD : 0 ≤ D) (hY : 0 ≤ Y) (hZ : 0 ≤ Z) (hle : x ^ 2 ≤ D + Y + Z) : x ≤ √D + √Y + √Z

The deterministic half of the square-root step: a three-term bound on a square becomes a three-term bound on the root, with no constant.

The packaged square-root step

theorem Algsuperdiff.Section3.Provider.Tail.isDeterministicShiftTwoTermOneSidedOrlicz_of_sq_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X Y Z : Ω → ℝ} {D A₁ A₂ σ₁ σ₂ b B₁ B₂ : ℝ} (hσ₁ : 0 < σ₁) (hσ₂ : 0 < σ₂) (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hXnn : ∀ (ω : Ω), 0 ≤ X ω) (hYnn : ∀ (ω : Ω), 0 ≤ Y ω) (hZnn : ∀ (ω : Ω), 0 ≤ Z ω) (hD : 0 ≤ D) (hA₁ : 0 ≤ A₁) (hA₂ : 0 ≤ A₂) (hsq : ∀ᵐ (ω : Ω) ∂μ, X ω ^ 2 ≤ D + Y ω + Z ω) (hYt : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ₁) Y A₁) (hZt : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ₂) Z A₂) (hb : √D ≤ b) (hB₁ : √A₁ ≤ B₁) (hB₁pos : 0 < B₁) (hB₂ : √A₂ ≤ B₂) (hB₂pos : 0 < B₂) : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz μ (HCPolySupport.IndependentSums.gammaSigma (2 * σ₁)) (HCPolySupport.IndependentSums.gammaSigma (2 * σ₂)) X b B₁ B₂

The packaged square-root step.

If a nonnegative measurable X satisfies, almost everywhere, a three-term bound on its square

X ^ 2 <= D + Y + Z

with Y <= O_{Gamma_{sigma_1}}(A_1) and Z <= O_{Gamma_{sigma_2}}(A_2) nonnegative witnesses, then X satisfies the source's two-term one-sided relation

X <= b + O_{Gamma_{2 sigma_1}}(B_1) + O_{Gamma_{2 sigma_2}}(B_2)

for any deterministic shift b >= sqrt D and any positive scales B_1 >= sqrt A_1, B_2 >= sqrt A_2.