Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.UnitRangeGaussianGauge

High-contrast homogenization: Provider.Quenched.UnitRangeGaussianGauge #

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

The finite-range Gaussian gauge #

A unit-range law satisfies the concentration-for-sums condition with the dimensional parameters supplied by unit range of dependence: the exponents β = 0 and ν = d/2, the Gaussian concentration gauge Ψ_fr(t) = exp(c_fr(d) t²), and a dimensional growth witness K_fr(d) ∈ [3, ∞).

This file fixes those numbers and proves the two structural properties a gauge must have before the weak-Orlicz calculus can use it: admissibility, that is monotonicity on [0, ∞) together with the lower bound one, and the growth inequality t Ψ(t) ≤ Ψ(K t) for t ≥ 1.

The value of c_fr(d) recorded here is the one the colouring argument produces. A triadic colouring of the aligned cells uses 3^d colours, each colour class is independent under unit range, and the resulting sub-Gaussian parameter of a sum of N bounded local observables is 3^d N; the exponent constant is the reciprocal (2 · 3^d)⁻¹ that the Chernoff bound then supplies. Every number here depends on the dimension alone; none of them sees a law, a reference block, a source scale or an exponent.

The dimensional numbers #

source
noncomputable def HCPolySupport.HighContrast.Quenched.frGaugeConst (d : ℕ) :
ℝ

The dimensional constant c_fr(d) of the finite-range Gaussian gauge.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Quenched.frGauge (d : ℕ) :
    ℝ → ℝ

    The finite-range Gaussian gauge Ψ_fr(t) = exp(c_fr(d) t²).

    Equations
    Instances For
      source
      def HCPolySupport.HighContrast.Quenched.frThreshold (d : ℕ) :
      ℝ

      The dimensional threshold constant of the finite-range concentration estimate: the factor by which the natural fluctuation scale is enlarged so that the two-sided union bound is absorbed into the gauge itself.

      Equations
      Instances For

        Elementary positivity #

        source
        theorem HCPolySupport.HighContrast.Quenched.one_le_three_pow (d : ℕ) :
        1 ≤ 3 ^ d
        source
        theorem HCPolySupport.HighContrast.Quenched.three_pow_pos (d : ℕ) :
        0 < 3 ^ d
        source
        theorem HCPolySupport.HighContrast.Quenched.two_mul_three_pow_pos (d : ℕ) :
        0 < 2 * 3 ^ d
        source
        theorem HCPolySupport.HighContrast.Quenched.frGaugeConst_pos (d : ℕ) :
        0 < frGaugeConst d
        source
        theorem HCPolySupport.HighContrast.Quenched.three_le_frThreshold (d : ℕ) :
        3 ≤ frThreshold d
        source
        theorem HCPolySupport.HighContrast.Quenched.frThreshold_pos (d : ℕ) :
        0 < frThreshold d
        source
        theorem HCPolySupport.HighContrast.Quenched.frGauge_pos (d : ℕ) (t : ℝ) :
        0 < frGauge d t
        source
        theorem HCPolySupport.HighContrast.Quenched.inv_frGauge (d : ℕ) (t : ℝ) :
        (frGauge d t)⁻¹ = Real.exp (-(frGaugeConst d * t ^ 2))

        The reciprocal of the finite-range gauge is the Gaussian tail.

        The gauge is admissible #

        source
        theorem HCPolySupport.HighContrast.Quenched.admissiblePsi_frGauge (d : ℕ) :
        IndependentSums.AdmissiblePsi (frGauge d)

        The finite-range gauge is admissible: it is monotone on [0, ∞) and at least one there.

        The growth witness #

        source
        theorem HCPolySupport.HighContrast.Quenched.log_two_le_frGaugeConst_mul_threshold (d : ℕ) :
        Real.log 2 ≤ frGaugeConst d * (frThreshold d ^ 2 - 1)

        The defining arithmetic of the threshold constant: the two-sided union bound of the Chernoff estimate is absorbed by the enlarged threshold.