High-contrast homogenization: Provider.Quenched.UnitRangeConcentration

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

Concentration for sums from unit range of dependence

The concentration-for-sums condition, with the parameters supplied by unit range of dependence, asks that the normalized average of a family of centred observables bounded by one, each carried by its own standard aligned cube of a common scale, obey a weak-Orlicz tail at the exponent ν = d/2 with a gauge that depends on the dimension alone.

This file derives that condition from unit range of dependence. The sub-Gaussian moment bound of the colouring argument gives, through the Chernoff inequality applied to the sum and to its negative, a two-sided Gaussian tail with a dimensional prefactor two; the prefactor is absorbed into the dimensional threshold constant C_fr(d), leaving exactly the Gaussian concentration gauge Ψ_fr(t) = exp(c_fr(d) t²). The averaged form is the printed display: the average of N such observables is O_{Ψ_fr}(C_fr(d) N^{-1/2}), and N^{-1/2} = 3^{-ν(m-n)} for the family of scale-n cubes centred in □_m.

The two-sided Chernoff bound

theorem HCPolySupport.HighContrast.Quenched.measureReal_abs_sum_standardCell_ge_le {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 → ℤ)) {ε : ℝ} (hε : 0 ≤ ε) : P.real {a : CoeffSpace d | ε ≤ |∑ w ∈ Z, X w a|} ≤ 2 * Real.exp (-ε ^ 2 / (2 * ↑(3 ^ d * Z.card)))

The two-sided Gaussian tail of a sum of bounded centred local observables. Both constants depend on the dimension alone.

The prefactor is absorbed by the threshold constant

theorem HCPolySupport.HighContrast.Quenched.two_mul_exp_le_inv_frGauge (d : ℕ) {t : ℝ} (ht : 1 ≤ t) : 2 * Real.exp (-(frThreshold d ^ 2 * t ^ 2 * frGaugeConst d)) ≤ (frGauge d t)⁻¹

The dimensional threshold constant absorbs the two-sided union bound: at the enlarged threshold the doubled Gaussian tail is again a Gaussian tail at the dimensional constant c_fr(d).

The concentration-for-sums estimate

theorem HCPolySupport.HighContrast.Quenched.measureReal_abs_sum_standardCell_ge_le_frGauge {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 → ℤ)} (hZ : Z.Nonempty) {t : ℝ} (ht : 1 ≤ t) : P.real {a : CoeffSpace d | frThreshold d * t * √↑Z.card ≤ |∑ w ∈ Z, X w a|} ≤ (frGauge d t)⁻¹

Concentration for sums from unit range of dependence, on the sum. For a family of centred observables bounded by one, each measurable for the local sigma-field of its own standard aligned cube of a common nonnegative scale, the sum exceeds C_fr(d) t √N with probability at most Ψ_fr(t)⁻¹, for every t ≥ 1. Both dimensional numbers are fixed before any law datum.

theorem HCPolySupport.HighContrast.Quenched.measureReal_abs_average_standardCell_ge_le_frGauge {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 → ℤ)} (hZ : Z.Nonempty) {t : ℝ} (ht : 1 ≤ t) : P.real {a : CoeffSpace d | frThreshold d * t * (√↑Z.card)⁻¹ ≤ |(↑Z.card)⁻¹ * ∑ w ∈ Z, X w a|} ≤ (frGauge d t)⁻¹

Concentration for sums from unit range of dependence, printed form. The average of N centred observables bounded by one and local to their own standard aligned cubes exceeds C_fr(d) t N^{-1/2} with probability at most Ψ_fr(t)⁻¹. For the family of scale-n cubes centred in □_m the factor N^{-1/2} is 3^{-ν(m-n)} with ν = d/2.