High-contrast homogenization: Provider.Quenched.UnitRangeSubgaussianSums

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Sub-Gaussian sums of bounded local observables under unit range

Unit range of dependence makes a family of observables carried by pairwise ℓ^∞-separated regions jointly independent. Bounded centred random variables have sub-Gaussian moment-generating functions by Hoeffding's lemma, and the moment-generating function of a sum of independent sub-Gaussian variables is the product of theirs, so a sum over a separated family is sub-Gaussian with parameter the number of its members.

The family the concentration-for-sums condition is stated for is not separated: neighbouring standard aligned cubes touch. It becomes separated after a triadic colouring, and the moment-generating function of the whole sum is bounded by the product of the colour-class ones without any independence between the colours. The Cauchy–Schwarz inequality turns the resulting sum of square roots into the dimensional parameter 3^d N for a family of N cubes.

Every constant produced here is a power of three in the dimension: nothing in this file sees a law, a reference block, a source scale or an exponent.

Two facts about sub-Gaussian moment-generating functions

theorem HCPolySupport.HighContrast.Quenched.hasSubgaussianMGF_mono {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c c' : NNReal} (h : ProbabilityTheory.HasSubgaussianMGF X c μ) (hc : c ≤ c') : ProbabilityTheory.HasSubgaussianMGF X c' μ

The sub-Gaussian parameter may be enlarged.

theorem HCPolySupport.HighContrast.Quenched.hasSubgaussianMGF_finset_sum {Ω : Type u_1} {κ : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Y : κ → Ω → ℝ} {n : κ → NNReal} (T : Finset κ) (h : ∀ c ∈ T, ProbabilityTheory.HasSubgaussianMGF (Y c) (n c) μ) : ProbabilityTheory.HasSubgaussianMGF (fun (a : Ω) => ∑ c ∈ T, Y c a) ((∑ c ∈ T, NNReal.sqrt (n c)) ^ 2) μ

A finite sum of sub-Gaussian variables, with no independence assumed, is sub-Gaussian with the square of the sum of the square roots of the parameters.

Bounded centred observables

theorem HCPolySupport.HighContrast.Quenched.hasSubgaussianMGF_of_abs_le_one {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {X : CoeffSpace d → ℝ} (hm : AEMeasurable X P) (hbd : ∀ᵐ (a : CoeffSpace d) ∂P, |X a| ≤ 1) (hmean : ∫ (a : CoeffSpace d), X a ∂P = 0) : ProbabilityTheory.HasSubgaussianMGF X 1 P

Hoeffding's lemma on the coefficient space: a centred observable bounded by one has a sub-Gaussian moment-generating function with parameter one.

Sums over a separated family

theorem HCPolySupport.HighContrast.Quenched.hasSubgaussianMGF_sum_of_pairwise_unitSeparated {d : ℕ} {ι : Type u_1} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {U : ι → Set (Vec d)} (hU : ∀ (i : ι), MeasurableSet (U i)) (hsep : Pairwise fun (i j : ι) => UnitSeparated (U i) (U j)) {X : ι → CoeffSpace d → ℝ} (hXloc : ∀ (i : ι), Measurable (X i)) (hXbd : ∀ (i : ι), ∀ᵐ (a : CoeffSpace d) ∂P, |X i a| ≤ 1) (hXmean : ∀ (i : ι), ∫ (a : CoeffSpace d), X i a ∂P = 0) (s : Finset ι) : ProbabilityTheory.HasSubgaussianMGF (fun (a : CoeffSpace d) => ∑ i ∈ s, X i a) (↑s.card) P

A sum of centred observables bounded by one, each measurable for the local sigma-field of its own region, over a pairwise unit-separated family of regions, is sub-Gaussian with parameter the number of summands.

Sums over one colour class of standard aligned cubes

theorem HCPolySupport.HighContrast.Quenched.hasSubgaussianMGF_sum_standardCell_colour {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {k : ℤ} (hk : 0 ≤ k) {X : (Fin d → ℤ) → CoeffSpace d → ℝ} (hXloc : ∀ (w : Fin d → ℤ), Measurable (X w)) (hXbd : ∀ (w : Fin d → ℤ), ∀ᵐ (a : CoeffSpace d) ∂P, |X w a| ≤ 1) (hXmean : ∀ (w : Fin d → ℤ), ∫ (a : CoeffSpace d), X w a ∂P = 0) (c : Fin d → ZMod 3) (Zc : Finset (Fin d → ℤ)) (hZc : ∀ w ∈ Zc, (fun (i : Fin d) => ↑(w i)) = c) : ProbabilityTheory.HasSubgaussianMGF (fun (a : CoeffSpace d) => ∑ w ∈ Zc, X w a) (↑Zc.card) P

A sum of centred observables bounded by one, each local to its own standard aligned cube, over a family of cubes of one colour, is sub-Gaussian with parameter the number of cubes.

Sums over the whole family

theorem HCPolySupport.HighContrast.Quenched.hasSubgaussianMGF_sum_standardCell {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsUnitRangeLaw P) {k : ℤ} (hk : 0 ≤ k) {X : (Fin d → ℤ) → CoeffSpace d → ℝ} (hXloc : ∀ (w : Fin d → ℤ), Measurable (X w)) (hXbd : ∀ (w : Fin d → ℤ), ∀ᵐ (a : CoeffSpace d) ∂P, |X w a| ≤ 1) (hXmean : ∀ (w : Fin d → ℤ), ∫ (a : CoeffSpace d), X w a ∂P = 0) (Z : Finset (Fin d → ℤ)) : ProbabilityTheory.HasSubgaussianMGF (fun (a : CoeffSpace d) => ∑ w ∈ Z, X w a) (↑(3 ^ d * Z.card)) P

The concentration-for-sums moment bound. A sum of centred observables bounded by one, each local to its own standard aligned cube of a common nonnegative scale, is sub-Gaussian with the dimensional parameter 3^d N, where N is the number of cubes. The colour classes carry independence; the sum over the at most 3^d colours costs the Cauchy–Schwarz factor.