MomentBoostedLowPowerColoring

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

Internal colored concave-power transport for the low-power route

This module transports the raw quadratic-plus-linear Bernstein tail through a finite range coloring and then through a concave power r in [1/2, 1]. Keeping both regimes before the power is exactly what preserves the card^{-1/2} gain at r = p / 2.

The proof is internal probability infrastructure. Its finite-family inputs are discharged by the stream-specific partition construction; it is not a source-facing substitute for the large-cube theorem.

noncomputable def Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerColorConst (q : ℝ) : ℝ

A dimensionless color factor for the two-regime low-power transport.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinQuadratic_one_le : 1 ≤ momentBoostedBernsteinQuadratic

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedBernsteinLinear_one_le : 1 ≤ momentBoostedBernsteinLinear

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerColorConst_pos {q : ℝ} (hq : 0 < q) : 0 < momentBoostedLowPowerColorConst q

theorem Algsuperdiff.Section3.Provider.Stream.one_le_momentBoostedLowPowerColorConst {q : ℝ} (hq : 1 ≤ q) : 1 ≤ momentBoostedLowPowerColorConst q

theorem Algsuperdiff.Section3.Provider.Stream.momentBoostedLowPowerColorConst_mono {q Q : ℝ} (hq : 0 ≤ q) (hqQ : q ≤ Q) : momentBoostedLowPowerColorConst q ≤ momentBoostedLowPowerColorConst Q

theorem Algsuperdiff.Section3.Provider.Stream.measureReal_upperTailEvent_finset_sum_le_momentBoostedColoredBernstein {Omega : Type u_1} {iota : Type u_2} {kappa : Type u_3} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] [DecidableEq kappa] {X : iota → Omega → ℝ} {s : Finset iota} {color : iota → kappa} {a : ℝ} (h_indep : ∀ b ∈ Finset.image color s, ProbabilityTheory.iIndepFun (fun (i : ↥({j ∈ s | color j = b})) => X ↑i) mu) (h_meas : ∀ (i : iota), Measurable (X i)) (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) (↑(Finset.image color s).card * a)) ≤ ↑(Finset.image color s).card * (Real.exp (-a ^ 2 / (momentBoostedBernsteinQuadratic * ↑s.card)) + Real.exp (-a / momentBoostedBernsteinLinear))

A finite-range coloring preserves the raw Bernstein two-regime tail.

theorem Algsuperdiff.Section3.Provider.Stream.sub_rpow_isBigOWith_gammaSigma_of_momentBoostedColoredBernstein {Omega : Type u_1} {iota : Type u_2} {kappa : Type u_3} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] [DecidableEq kappa] {X : iota → Omega → ℝ} {s : Finset iota} {color : iota → kappa} {Y Z : Omega → ℝ} {r H K : ℝ} (hs : s.Nonempty) (h_indep : ∀ b ∈ Finset.image color s, ProbabilityTheory.iIndepFun (fun (i : ↥({j ∈ s | color j = b})) => X ↑i) mu) (h_meas : ∀ (i : iota), Measurable (X i)) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma 1) (X i) 1) (hmean : ∀ i ∈ s, ∫ (omega : Omega), X i omega ∂mu = 0) (hr_half : 1 / 2 ≤ r) (hr_one : r ≤ 1) (hH : 0 < H) (hK : 0 < K) (hKH : K ≤ H) (hY_nonneg : 0 ≤ᵐ[mu] Y) (hZY : Z ≤ᵐ[mu] fun (omega : Omega) => Y omega ^ r) (hYsum : Y ≤ᵐ[mu] fun (omega : Omega) => H + K / ↑s.card * ∑ i ∈ s, X i omega) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma r⁻¹) (fun (omega : Omega) => Z omega - H ^ r) (momentBoostedLowPowerColorConst ↑(Finset.image color s).card * H ^ r / √↑s.card)

Concave-power endpoint with raw colored Bernstein input. This is the deterministic two-regime transport later instantiated with r = p / 2, the scale-two descendant mass Y, and the scale-p mass Z.