Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Proportion.SeriesTail

SeriesTail #

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

Two weak-Orlicz devices Β§4.1 needs and the ambient library does not have #

ABK26, Β§4.1, l.good.scales.ratio.lambda, the 𝒴 tail. The score field

𝒴_n := Ξ³^{-4} Ξ£_{k=-∞}^{n} 3^{-ΒΌΞ³(n-k)} max_{z ∈ 3^{k-2}β„€^d ∩ (β–‘_nβˆ–β–‘_{n-1})} (…)_+

is an infinite weighted sum of finite maxima, and the manuscript asserts an π’ͺ_{Ξ“_{1/3}} bound for it. Two generic devices are needed:

  1. isBigOWith_fmax β€” the union-bound (e.maxy.bound) lift of a Ξ“_Οƒ tail through a finite maximum, with the penalty c constrained only by log(#S) ≀ c^Οƒ βˆ’ 1. The ambient library's isBigOWith_gammaSigma_finset_sup' is not usable here: it requires 2 ≀ S.card and a nonempty S, while the Β§4.1 lattice annuli must be allowed to be empty (they are, at the degenerate indices), and it uses Finset.sup' rather than a 0-floored maximum.

  2. isBigOWith_wsum β€” the countable generalized triangle inequality: a weighted series of nonnegative atoms with individual Ξ“_Οƒ tails and summable weighted scales has a Ξ“_Οƒ tail at the scale gammaTriangleConst Οƒ Β· Ξ£_j c_j a_j. The ambient library has no tsum-level triangle inequality and no monotone-limit stability for Ξ“_Οƒ tails; both were checked exhaustively. The device supplied here is the monotone-limit one: the tail event of the series is the increasing union of the tail events of the partial sums, and continuity from below (Monotone.measure_iUnion) turns the uniform finite-sum bound into the series bound. Nothing is assumed about pointwise convergence: the series is formed in ℝβ‰₯0∞, where it always exists, and .toReal sends the divergent sample points to 0, which only helps the upper tail.

Scope #

Provider material: carrier-neutral local helpers over an abstract probability space. Every hypothesis is data about an abstract family; no ABK carrier, model or standing assumption appears. No sorry, no custom axioms, no set_option maxHeartbeats.

References #

1. The 0-floored finite maximum #

source
def Algsuperdiff.Section4.Provider.Proportion.fmax {iota : Type u_2} (S : Finset iota) (f : iota β†’ ℝ) :
ℝ

The 0-floored maximum of f over a Finset. Total (no nonemptiness side condition) and nonnegative, matching the sign convention of the manuscript's lattice maxima, all of whose entries are positive parts.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.fmax_nonneg {iota : Type u_2} (S : Finset iota) (f : iota β†’ ℝ) :
    0 ≀ fmax S f
    source
    @[simp]
    theorem Algsuperdiff.Section4.Provider.Proportion.fmax_empty {iota : Type u_2} (f : iota β†’ ℝ) :
    fmax βˆ… f = 0
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.le_fmax {iota : Type u_2} {S : Finset iota} {f : iota β†’ ℝ} {i : iota} (hi : i ∈ S) :
    f i ≀ fmax S f
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.fmax_le {iota : Type u_2} {S : Finset iota} {f : iota β†’ ℝ} {b : ℝ} (hb : 0 ≀ b) (h : βˆ€ i ∈ S, f i ≀ b) :
    fmax S f ≀ b
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.exists_lt_of_lt_fmax {iota : Type u_2} {S : Finset iota} {f : iota β†’ ℝ} {b : ℝ} (hb : 0 ≀ b) (h : b < fmax S f) :
    βˆƒ i ∈ S, b < f i

    The converse reading of the 0-floored maximum. Above a nonnegative level the maximum is attained by a genuine member; this is the direction the union bound consumes, and the nonnegativity of the level is necessary (fmax βˆ… f = 0).

    source
    theorem Algsuperdiff.Section4.Provider.Proportion.fmax_insert {iota : Type u_2} [DecidableEq iota] (i : iota) (S : Finset iota) (f : iota β†’ ℝ) :
    fmax (insert i S) f = max (max (f i) 0) (fmax S f)
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.measurable_fmax {Omega : Type u_1} [MeasurableSpace Omega] {iota : Type u_2} (S : Finset iota) {f : iota β†’ Omega β†’ ℝ} (hf : βˆ€ (i : iota), Measurable (f i)) :
    Measurable fun (omega : Omega) => fmax S fun (i : iota) => f i omega

    2. The union-bound lift of a Ξ“_Οƒ tail through a finite maximum #

    source
    theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_fmax {Omega : Type u_1} [MeasurableSpace Omega] {iota : Type u_2} {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (S : Finset iota) {X : iota β†’ Omega β†’ ℝ} {A c sigma : ℝ} (hsigma : 0 < sigma) (hA : 0 ≀ A) (hc : 1 ≀ c) (hcard : Real.log ↑S.card ≀ c ^ sigma - 1) (hX : βˆ€ i ∈ S, HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (X i) A) :
    HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Omega) => fmax S fun (i : iota) => X i omega) (c * A)

    e.maxy.bound at an abstract finite index set.

    If every member of a finite family has a Ξ“_Οƒ upper tail at the common scale A β‰₯ 0, then their 0-floored maximum has one at the scale c Β· A, for any c β‰₯ 1 with log(#S) ≀ c^Οƒ βˆ’ 1.

    No nonemptiness and no lower bound on #S is required: at S = βˆ… the maximum is 0 and the bound is vacuous.

    3. The ℝβ‰₯0∞-formed weighted series #

    source
    noncomputable def Algsuperdiff.Section4.Provider.Proportion.wsumE {Omega : Type u_1} (T : β„• β†’ Omega β†’ ℝ) (c : β„• β†’ ℝ) (omega : Omega) :
    ENNReal

    The weighted series of a sequence of nonnegative atoms, formed in ℝβ‰₯0∞. Total: no summability side condition, and no junk-value hazard, because ℝβ‰₯0∞ sums always exist.

    Equations
    Instances For
      source
      noncomputable def Algsuperdiff.Section4.Provider.Proportion.wsum {Omega : Type u_1} (T : β„• β†’ Omega β†’ ℝ) (c : β„• β†’ ℝ) (omega : Omega) :
      ℝ

      The real-valued weighted series; at the sample points where the ℝβ‰₯0∞ sum is infinite this is 0, which only strengthens every upper-tail statement made about it.

      Equations
      Instances For
        source
        theorem Algsuperdiff.Section4.Provider.Proportion.wsum_nonneg {Omega : Type u_1} (T : β„• β†’ Omega β†’ ℝ) (c : β„• β†’ ℝ) (omega : Omega) :
        0 ≀ wsum T c omega
        source
        theorem Algsuperdiff.Section4.Provider.Proportion.le_wsumE {Omega : Type u_1} (T : β„• β†’ Omega β†’ ℝ) (c : β„• β†’ ℝ) (omega : Omega) (j : β„•) :
        ENNReal.ofReal (c j * T j omega) ≀ wsumE T c omega

        Every single term is below the series β€” unconditionally, in ℝβ‰₯0∞.

        source
        def Algsuperdiff.Section4.Provider.Proportion.wpartial {Omega : Type u_1} (T : β„• β†’ Omega β†’ ℝ) (c : β„• β†’ ℝ) (N : β„•) (omega : Omega) :
        ℝ

        The partial sums of the weighted series.

        Equations
        Instances For
          source
          theorem Algsuperdiff.Section4.Provider.Proportion.wsumE_eq_iSup {Omega : Type u_1} {T : β„• β†’ Omega β†’ ℝ} {c : β„• β†’ ℝ} (hT0 : βˆ€ (j : β„•) (omega : Omega), 0 ≀ T j omega) (hc : βˆ€ (j : β„•), 0 ≀ c j) (omega : Omega) :
          wsumE T c omega = ⨆ (N : β„•), ENNReal.ofReal (wpartial T c N omega)

          The countable generalized triangle inequality #

          source
          theorem Algsuperdiff.Section4.Provider.Proportion.isBigOWith_wsum {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {T : β„• β†’ Omega β†’ ℝ} {c a : β„• β†’ ℝ} {sigma : ℝ} (hsigma : 0 < sigma) (hT0 : βˆ€ (j : β„•) (omega : Omega), 0 ≀ T j omega) (hTm : βˆ€ (j : β„•), Measurable (T j)) (hc : βˆ€ (j : β„•), 0 < c j) (ha : βˆ€ (j : β„•), 0 < a j) (hsum : Summable fun (j : β„•) => c j * a j) (hT : βˆ€ (j : β„•), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (T j) (a j)) :
          HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (wsum T c) (HCPolySupport.IndependentSums.gammaTriangleConst sigma * βˆ‘' (j : β„•), c j * a j)

          The countable generalized triangle inequality for Ξ“_Οƒ upper tails.

          For nonnegative measurable atoms T_j with T_j ≀ π’ͺ_{Ξ“_Οƒ}(a_j), positive weights c_j, and Ξ£_j c_j a_j < ∞,

          Ξ£_j c_j T_j ≀ π’ͺ_{Ξ“_Οƒ} ( gammaTriangleConst Οƒ Β· Ξ£_j c_j a_j ) ,

          the series being the total ℝβ‰₯0∞ one.

          The proof is the monotone-limit device: the tail event of the series is the increasing union of the tail events of the partial sums (in ℝβ‰₯0∞, so the divergent sample points are handled by .toReal = 0, which lies below every positive level), the partial sums obey the finite triangle inequality at the N-uniform scale, and continuity from below closes it.

          source
          theorem Algsuperdiff.Section4.Provider.Proportion.measurable_wsum {Omega : Type u_1} [MeasurableSpace Omega] {T : β„• β†’ Omega β†’ ℝ} {c : β„• β†’ ℝ} (hTm : βˆ€ (j : β„•), Measurable (T j)) :
          Measurable (wsum T c)

          Measurability of the weighted series. The ℝβ‰₯0∞ sum of measurable nonnegative terms is measurable, and .toReal is measurable.