WeightedSubgaussian

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

Weighted sub-Gaussian concentration from weak Gamma-two tails

Internal probability infrastructure for the corrected off-diagonal part of ABK26's Section 3.1 L2 estimate. It proves the classical tail-to-MGF bridge and the weighted independent-family estimate needed after finer-shell coloring. These ordinary reusable probability lemmas make no source-node status claim.

Pointwise real inequality exp u ≤ u + exp (u²).

Square-exponential moment via the layer-cake formula.

theorem Algsuperdiff.Section3.Provider.Orlicz.integral_exp_smul_le_of_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {W : Ω → ℝ} (hW_meas : AEMeasurable W μ) (hW_nn : 0 ≤ᵐ[μ] W) (hW_tail : ∀ (s : ℝ), 0 < s → μ.real {ω : Ω | s < W ω} ≤ 2 * Real.exp (-s)) {l : ℝ} (hl0 : 0 ≤ l) (hl1 : l < 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * W ω)) μ ∧ ∫ (ω : Ω), Real.exp (l * W ω) ∂μ ≤ 1 + 2 * l / (1 - l)

Square-exponential moment bound. For a nonnegative W with the clean exponential tail P[W > s] ≤ 2 exp(−s) and 0 ≤ l < 1, the variable exp (l·W) is integrable with ∫ exp (l·W) ≤ 1 + 2l/(1−l). Proved by the weighted layer-cake formula: E[exp l W] = 1 + ∫₀^∞ P[W>s]·l e^{ls} ds, and the tail bounds the density integral by ∫₀^∞ 2 l e^{(l−1)s} ds = 2l/(1−l).

The tail → MGF converter.

theorem Algsuperdiff.Section3.Provider.Orlicz.hasSubgaussianMGF_of_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : AEMeasurable X μ) {c : NNReal} (hc : 0 < c) (hcenter : ∫ (ω : Ω), X ω ∂μ = 0) (htail : ∀ (t : ℝ), 0 < t → μ.real {ω : Ω | t < |X ω|} ≤ 2 * Real.exp (-t ^ 2 / ↑c)) : ProbabilityTheory.HasSubgaussianMGF X (8 * c) μ

A centered real random variable X (∫ X = 0) with the two-sided sub-Gaussian tail P[|X| > t] ≤ 2 exp(−t²/c) (c > 0) has a sub-Gaussian moment generating function with the universal parameter 8·c: HasSubgaussianMG (8·c) μ.

Centering and measurability are honest hypotheses (mean-zero comes from the spine downstream).

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.weightedSubgaussianConst : ℝ

weightedSubgaussianConst ^ 2 / 2 = 1 + log 2, which lets the union-bound factor 2 be absorbed into the t ≥ 1 decay: 2 · exp(−(1+log 2) t²) ≤ exp(−t²).

Equations

• Algsuperdiff.Section3.Provider.Orlicz.weightedSubgaussianConst = √(2 * (1 + Real.log 2))

theorem Algsuperdiff.Section3.Provider.Orlicz.weightedSubgaussianConst_pos : 0 < weightedSubgaussianConst

theorem Algsuperdiff.Section3.Provider.Orlicz.weightedSubgaussianConst_sq : weightedSubgaussianConst ^ 2 = 2 * (1 + Real.log 2)

theorem Algsuperdiff.Section3.Provider.Orlicz.two_mul_exp_neg_log_two_le (t : ℝ) (ht : 1 ≤ t) : 2 * Real.exp (-((1 + Real.log 2) * t ^ 2)) ≤ Real.exp (-t ^ 2)

Pure-real absorption of the union-bound factor 2: for t ≥ 1, 2 · exp(−((1 + log 2) t²)) ≤ exp(−(t ^ (2:ℝ))). Extracted so no numeric tactic ever enters a Real.rpow/Real.exp term.

theorem Algsuperdiff.Section3.Provider.Orlicz.measureReal_abs_weightedSum_gt_le {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {c : ι → NNReal} {s : Finset ι} (a : ι → ℝ) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_subG : ∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω : Ω | ε < |∑ i ∈ s, a i * X i ω|} ≤ 2 * Real.exp (-ε ^ 2 / (2 * ∑ i ∈ s, a i ^ 2 * ↑(c i)))

Weighted sub-Gaussian tail (raw two-sided form). For whole-family independent X with per-term sub-Gaussian MGF HasSubgaussianMGF (X i) (c i), real weights a, and any ε ≥ 0, μ.real {ω | ε < |Σ_{i∈s} a i X i ω|} ≤ 2 exp(−ε²/(2 Σ_{i∈s} (a i)² c i)). The weighted sum is sub-Gaussian by const_mul (scaling by a i multiplies the parameter by (a i)²), iIndepFun.comp (the scaled family stays independent) and sum_of_iIndepFun; the union of the two Chernoff tails carries the 2.

theorem Algsuperdiff.Section3.Provider.Orlicz.weightedSum_ae_zero_of_variance_zero {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {c : ι → NNReal} {s : Finset ι} (a : ι → ℝ) (h_subG : ∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) (hV0 : ∑ i ∈ s, a i ^ 2 * ↑(c i) = 0) : (fun (ω : Ω) => ∑ i ∈ s, a i * X i ω) =ᵐ[μ] 0

If the weighted variance Σ_{i∈s} (a i)² c i vanishes then the weighted sum is a.e. zero: each term is either 0 (weight) or a.e. 0 (a HasSubgaussianMGF · 0 variable).

theorem Algsuperdiff.Section3.Provider.Orlicz.weightedSum_subgaussian_tail {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {c : ι → NNReal} {s : Finset ι} (a : ι → ℝ) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_subG : ∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) ⦃t : ℝ⦄ : 1 ≤ t → μ.real {ω : Ω | weightedSubgaussianConst * √(∑ i ∈ s, a i ^ 2 * ↑(c i)) * t < |∑ i ∈ s, a i * X i ω|} ≤ Real.exp (-t ^ 2)

Weighted sub-Gaussian concentration (normalized gammaSigma 2 form). For whole-family independent X with per-term sub-Gaussian MGF, real weights a, and every t ≥ 1, μ.real {ω | C · (Σ a² c)^{1/2} · t < |Σ a X ω|} ≤ exp(−(t ^ 2)), where C = weightedSubgaussianConst. This is definitionally IsBigO μ (gammaSigma 2) (Σ a X) (C (Σ a² c)^{1/2}).

theorem Algsuperdiff.Section3.Provider.Orlicz.weightedSum_isBigO_gammaSigma_two {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {c : ι → NNReal} {s : Finset ι} (a : ι → ℝ) (h_indep : ProbabilityTheory.iIndepFun X μ) (h_subG : ∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Ω) => ∑ i ∈ s, a i * X i omega) (weightedSubgaussianConst * √(∑ i ∈ s, a i ^ 2 * ↑(c i)))

The weighted sub-Gaussian tail in CoarseGraining's Gamma_2 rendering.

theorem Algsuperdiff.Section3.Provider.Orlicz.hasSubgaussianMGF_of_isBigO_gammaSigma_two {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : AEMeasurable X μ) {A : ℝ} (hA : 0 < A) (hcenter : ∫ (ω : Ω), X ω ∂μ = 0) (hbd : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) X A) : ProbabilityTheory.HasSubgaussianMGF X (8 * (2 * A ^ 2).toNNReal) μ

The two-sided tail P[|X| > u] ≤ 2 exp(−u²/(2A²)) (all u > 0) is fed to hasSubgaussianMGF_of_tail with c = 2A², κ = 8.

theorem Algsuperdiff.Section3.Provider.Orlicz.weightedSum_of_gammaSigma_tails_nonneg {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} {A : ι → ℝ} {s : Finset ι} (a : ι → ℝ) (h_indep : ProbabilityTheory.iIndepFun X μ) (hX : ∀ i ∈ s, AEMeasurable (X i) μ) (hA : ∀ i ∈ s, 0 ≤ A i) (hzero : ∀ i ∈ s, A i = 0 → X i =ᵐ[μ] 0) (hcenter : ∀ i ∈ s, ∫ (ω : Ω), X i ω ∂μ = 0) (htail : ∀ i ∈ s, HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (X i) (A i)) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (ω : Ω) => ∑ i ∈ s, a i * X i ω) (weightedSubgaussianConst * √(∑ i ∈ s, a i ^ 2 * (16 * A i ^ 2)))

The weighted tail-to-MGF estimate with possibly vanishing scales. A zero-scale summand must be almost surely zero; positive-scale summands use the tail-to-MGF converter above. This is the form needed when deterministic local energies supply the scales and some cells can carry no energy.