Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.Stream.MomentBoostedLowPowerBernstein

MomentBoostedLowPowerBernstein #

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

Internal two-regime Bernstein spine for the low-power large-cube route #

This module records the finite-family estimate used before the concave p / 2 power in the 1 <= p <= 2 branch. It starts from centered unit Gamma_1 summands, invokes only CoarseGraining's small-tilt moment/MGF lemma, and keeps the quadratic and linear Chernoff regimes separate. The two terms are needed by the later concave-power transport; collapsing them first to a Gamma_1 tail would lose the required square-root spatial gain.

source
noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinBase :
ℝ

The fixed first-moment MGF coefficient in the low-power Bernstein route.

Equations
Instances For
    source
    theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinBase_pos :
    0 < momentBoostedBernsteinBase
    source
    theorem Algsuperdiff.Section3.Provider.Stream.one_le_momentBoostedBernsteinBase :
    1 ≤ momentBoostedBernsteinBase
    source
    noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinQuadratic :
    ℝ

    The quadratic denominator in the raw finite-family Bernstein tail.

    Equations
    Instances For
      source
      theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinQuadratic_pos :
      0 < momentBoostedBernsteinQuadratic
      source
      noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinLinear :
      ℝ

      The linear denominator in the raw finite-family Bernstein tail.

      Equations
      Instances For
        source
        theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinLinear_pos :
        0 < momentBoostedBernsteinLinear
        source
        theorem Algsuperdiff.Section3.Provider.Stream.measureReal_upperTailEvent_finset_sum_le_momentBoostedBernstein {Omega : Type u_1} {iota : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : iota → Omega → ℝ} {s : Finset iota} {a : ℝ} (h_indep : ProbabilityTheory.iIndepFun X mu) (h_meas : ∀ (i : iota), Measurable (X i)) (hs : s.Nonempty) (ha : 0 ≤ a) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma 1) (X i) 1) (hmean : ∀ i ∈ s, ∫ (omega : Omega), X i omega ∂mu = 0) :
        mu.real (HCPolySupport.IndependentSums.upperTailEvent (fun (omega : Omega) => ∑ i ∈ s, X i omega) a) ≤ Real.exp (-a ^ 2 / (momentBoostedBernsteinQuadratic * ↑s.card)) + Real.exp (-a / momentBoostedBernsteinLinear)

        Raw one-sided Bernstein concentration. A centered independent finite family with unit two-sided Gamma_1 control obeys the displayed quadratic plus linear tail. The statement is internal infrastructure: all its hypotheses are discharged by the colored descendant application below the source-facing surface.