Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Tail.OneTermSqrt

OneTermSqrt #

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

A one-term square-root tail conversion #

This module supplies the model-free tail conversion used by the corrected Section 3.2 base-case argument. If a nonnegative observable satisfies

X ^ 2 <= D + Y

almost everywhere and Y has a one-sided Gamma_1 tail, taking square roots produces a Gamma_2 random leg. There are two useful local transformations. The unshifted form treats sqrt D as a second Gamma_2 leg and pays the explicit binary addition constant. The shifted form absorbs sqrt D into a deterministic shift and keeps the random square-root scale unchanged.

source
noncomputable def Algsuperdiff.Section3.Provider.Tail.gammaTwoAdditionConst :
ℝ

The exact binary-addition multiplier at Gamma_2.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.Tail.gammaTwoAdditionConst_pos :
    0 < gammaTwoAdditionConst

    The Gamma_2 binary-addition multiplier is positive.

    source
    theorem Algsuperdiff.Section3.Provider.Tail.isBigOWith_gammaSigma_const {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {sigma c A : ℝ} (hA : 0 ≤ A) (hc : c ≤ A) :
    HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (_omega : Omega) => c) A

    A deterministic constant bounded by a nonnegative scale has a one-sided Gamma_sigma tail at that scale.

    source
    theorem Algsuperdiff.Section3.Provider.Tail.isOneSidedOrlicz_gammaSigma_two_of_sq_le_add {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X Y : Omega → ℝ} {D A B : ℝ} (hX : Measurable X) (hXnn : ∀ (omega : Omega), 0 ≤ X omega) (hYnn : ∀ (omega : Omega), 0 ≤ Y omega) (hD : 0 ≤ D) (hA : 0 ≤ A) (hsq : ∀ᵐ (omega : Omega) ∂mu, X omega ^ 2 ≤ D + Y omega) (hYtail : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) Y A) (hDb : √D ≤ B) (hAb : √A ≤ B) (hBpos : 0 < B) :
    Probability.IsOneSidedOrlicz mu (HCPolySupport.IndependentSums.gammaSigma 2) X (gammaTwoAdditionConst * B)

    A one-random-leg square bound gives an unshifted one-sided Gamma_2 bound. Both square-root amplitudes are bounded by B, so their binary merge has the exact scale gammaTwoAdditionConst * B.

    source
    theorem Algsuperdiff.Section3.Provider.Tail.isDeterministicShiftOneSidedOrlicz_gammaSigma_two_of_sq_le_add {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X Y : Omega → ℝ} {D A b B : ℝ} (hX : Measurable X) (hXnn : ∀ (omega : Omega), 0 ≤ X omega) (hYnn : ∀ (omega : Omega), 0 ≤ Y omega) (hD : 0 ≤ D) (hA : 0 ≤ A) (hsq : ∀ᵐ (omega : Omega) ∂mu, X omega ^ 2 ≤ D + Y omega) (hYtail : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) Y A) (hDb : √D ≤ b) (hAb : √A ≤ B) (hBpos : 0 < B) :
    Probability.IsDeterministicShiftOneSidedOrlicz mu (HCPolySupport.IndependentSums.gammaSigma 2) X b B

    A one-random-leg square bound gives a deterministically shifted one-sided Gamma_2 bound. The deterministic square root is absorbed by b, so the random square-root scale B is retained without the binary-merge multiplier.