MomentBoostedColoring

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

Internal finite-color transport for the moment-boosted endpoint

This is the finite-range coloring step used by the large-cube route. Each color class is treated by the sharp independent-family endpoint, then a finite union transfers the one-sided tail to their sum. The resulting color factor is fixed once the spatial dimension and the coloring scale are fixed; it is deliberately left explicit here so that the stream application can absorb it into its single dimension-only constant.

No generic Gamma_sigma triangle inequality occurs in this module.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_finset_sum_momentBoosted_colored {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} {sigma : ℝ} (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)) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (X i) mu) (h_sq : ∀ i ∈ s, MeasureTheory.Integrable (fun (omega : Omega) => |X i omega| ^ 2) mu) (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hX : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigOWith mu (momentBoostedGammaSigma sigma) (X i) 1) (hmean : ∀ i ∈ s, ∫ (omega : Omega), X i omega ∂mu = 0) (hsecond : ∀ i ∈ s, ∫ (omega : Omega), |X i omega| ^ 2 ∂mu ≤ 1) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (fun (omega : Omega) => ∑ i ∈ s, X i omega) (16 * ↑(Finset.image color s).card * ↑(Finset.image color s).card ^ (1 / sigma) * √(momentBoostedIndependentVariance sigma) * √↑s.card)

A finite family split into independent color classes has the same sharp one-sided stretched-exponential endpoint, with an explicit finite-color factor. This is internal infrastructure; all locality and stationarity requirements are supplied later by the stream-specific application.