Analysis of Boolean Functions in Lean

5.2. Majority, and the Central Limit Theorem🔗

Definition5.2.1
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 6
Reverse dependency previews
Preview
Theorem 5.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2fidelity-direct-mathlib

Notation 5.14. We write Z\sim N(0,1) when Z is a standard Gaussian random variable. Its probability density function, cumulative distribution function, and complementary cumulative distribution function are denoted by \phi(z)=\frac1{\sqrt{2\pi}}e^{-z^2/2}, \qquad \Phi(t)=\int_{-\infty}^{t}\phi(z)\,dz, \qquad \overline\Phi(t)=\Phi(-t)=\int_t^\infty\phi(z)\,dz. More generally, if \mu\in\mathbb R^d and \Sigma\in\mathbb R^{d\times d} is positive semidefinite, then Z\sim N(\mu,\Sigma) means that Z is a d-dimensional Gaussian random vector with mean \mu and covariance matrix \Sigma.

Lean code for Definition5.2.1●5 definitions
  • defdefined in Mathlib/Probability/Distributions/Gaussian/Real.lean
    complete
    def ProbabilityTheory.gaussianPDFReal (μ : ℝ) (v : NNReal) (x : ℝ) : ℝ
    def ProbabilityTheory.gaussianPDFReal (μ : ℝ)
  (v : NNReal) (x : ℝ) : ℝ
    Probability density function of the Gaussian distribution with mean `μ` and variance `v`.
  • defdefined in Mathlib/Probability/Distributions/Gaussian/Real.lean
    complete
    def ProbabilityTheory.gaussianReal (μ : ℝ) (v : NNReal) :
  MeasureTheory.Measure ℝ
    def ProbabilityTheory.gaussianReal (μ : ℝ)
  (v : NNReal) : MeasureTheory.Measure ℝ
    A Gaussian distribution on `ℝ` with mean `μ` and variance `v`.
  • defdefined in Mathlib/Probability/CDF.lean
    complete
    def ProbabilityTheory.cdf (μ : MeasureTheory.Measure ℝ) :
  StieltjesFunction ℝ
    def ProbabilityTheory.cdf
  (μ : MeasureTheory.Measure ℝ) :
  StieltjesFunction ℝ
    Cumulative distribution function of a real measure. The definition currently makes sense only
for probability measures. In that case, it satisfies `cdf μ x = μ.real (Iic x)` (see
`ProbabilityTheory.cdf_eq_real`).
  • defdefined in Mathlib/Probability/Distributions/Gaussian/Multivariate.lean
    complete
    def ProbabilityTheory.stdGaussian.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] : MeasureTheory.Measure E
    def ProbabilityTheory.stdGaussian.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] :
  MeasureTheory.Measure E
    Standard Gaussian distribution on a finite-dimensional real inner product space `E`.
This is the random vector whose coordinates in an orthonormal basis are independent standard
Gaussian.

The definition uses `stdOrthonormalBasis ℝ E` but does not actually depend on the
basis, see `stdGaussian_eq_map_pi_orthonormalBasis`.
  • defdefined in Mathlib/Probability/Distributions/Gaussian/Multivariate.lean
    complete
    def ProbabilityTheory.multivariateGaussian.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (μ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) :
  MeasureTheory.Measure (EuclideanSpace ℝ ι)
    def ProbabilityTheory.multivariateGaussian.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (μ : EuclideanSpace ℝ ι)
  (S : Matrix ι ι ℝ) :
  MeasureTheory.Measure
    (EuclideanSpace ℝ ι)
    Multivariate Gaussian measure on `EuclideanSpace ℝ ι` with mean `μ` and covariance
matrix `S`. This only makes sense when `S` is positive semidefinite,
as then `CFC.sqrt S * CFC.sqrt S = S`. Otherwise `CFC.sqrt S = 0`, and
`multivariateGaussian μ S = Measure.dirac μ` (see `multivariateGaussian_of_not_posSemidef`).
Theorem5.2.2
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 6
Reverse dependency previews
Preview
Lemma 5.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2external-probability-dependencyfidelity-explicit-universal-constant

Berry--Esseen (Central Limit) Theorem. Let X_1,\ldots,X_n be independent real-valued random variables satisfying \mathbb E[X_i]=0, \qquad \operatorname{Var}[X_i]=\sigma_i^2, \qquad \sum_{i=1}^n\sigma_i^2=1. Set S=\sum_{i=1}^nX_i, let Z\sim N(0,1), and define \gamma=\sum_{i=1}^n\lVert X_i\rVert_3^3 =\sum_{i=1}^n\mathbb E[|X_i|^3]. Then for every u\in\mathbb R, \bigl|\Pr[S\le u]-\Pr[Z\le u]\bigr|\le c\gamma, where c is a universal constant. For definiteness, the book permits c=.56.

Lean code for Theorem5.2.2●1 theorem
  • theoremdefined in ProbabilityApproximation/ChenShao/UniformBerryEsseen.lean
    complete
    theorem ProbabilityTheory.uniformBerryEsseen_thirdMoment.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX : ∀ (k : ι), MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar : ∑ k, ProbabilityTheory.variance (X k) μ = 1)
  (h3 : ∀ (k : ι), MeasureTheory.Integrable (fun ω => |X k ω| ^ 3) μ)
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
          x -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          x| ≤
    ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.uniformBerryEsseen_thirdMoment.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX :
    ∀ (k : ι),
      MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar :
    ∑ k,
        ProbabilityTheory.variance (X k)
          μ =
      1)
  (h3 :
    ∀ (k : ι),
      MeasureTheory.Integrable
        (fun ω => |X k ω| ^ 3) μ)
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
          x -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          x| ≤
    ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ
    Pure linear third-moment Berry-Esseen: `|F-Phi| ≤ 30 γ` for all `γ`.
Lemma5.2.3
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2

Remark 5.15. In the setting of the Berry--Esseen Theorem, suppose in addition that |X_i|\le\epsilon with probability 1 for every i. Then \begin{aligned} \gamma &=\sum_{i=1}^n\mathbb E[|X_i|^3]\\ &\le\epsilon\sum_{i=1}^n\mathbb E[|X_i|^2] =\epsilon\sum_{i=1}^n\sigma_i^2 =\epsilon. \end{aligned}

Lean code for Lemma5.2.3●1 theorem
  • theoremdefined in FABL/Chapter05/BerryEsseenConsequences.lean
    complete
    theorem FABL.sum_integral_abs_cube_le_of_ae_abs_le.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ]
  (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (hmean : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvariance : ∑ i, ProbabilityTheory.variance (X i) μ = 1) {ε : ℝ}
  (hbound : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ ε) :
  ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ ≤ ε
    theorem FABL.sum_integral_abs_cube_le_of_ae_abs_le.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hX :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (hmean :
    ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvariance :
    ∑ i,
        ProbabilityTheory.variance (X i)
          μ =
      1)
  {ε : ℝ}
  (hbound :
    ∀ (i : ι),
      ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ ε) :
  ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ ≤ ε
    O'Donnell, Remark 5.15: uniformly bounded centered summands whose total variance is one
have total third absolute moment at most the uniform bound.
Lemma5.2.4
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2supportexternal-probability-dependencyfidelity-exact

Exercise 5.16 (strict inequalities and intervals). Under the assumptions and notation of the Berry--Esseen Theorem:

(a) For every u\in\mathbb R, \bigl|\Pr[S<u]-\Pr[Z<u]\bigr|\le c\gamma. The passage from non-strict to strict inequalities uses \lim_{\delta\to0^+}\Pr[Z\le u-\delta]=\Pr[Z\le u].

(b) Consequently, for every interval I\subseteq\mathbb R, with arbitrary choices of open or closed endpoints and allowing unbounded intervals, \bigl|\Pr[S\in I]-\Pr[Z\in I]\bigr|\le2c\gamma.

Lean code for Lemma5.2.4●4 declarations
  • inductive(4 constructors)defined in FABL/Chapter05/BerryEsseenIntervals.lean
    complete
    inductive FABL.RealInterval : Type
    inductive FABL.RealInterval : Type
    A single classification of bounded and unbounded real intervals, with endpoint inclusion
recorded by the Boolean flags.

    Constructors

    FABL.RealInterval.univ : FABL.RealInterval
    FABL.RealInterval.below (closed : Bool) (upper : ℝ) :
  FABL.RealInterval
    FABL.RealInterval.above (closed : Bool) (lower : ℝ) :
  FABL.RealInterval
    FABL.RealInterval.bounded (leftClosed rightClosed : Bool)
  (lower upper : ℝ) : FABL.RealInterval
  • defdefined in FABL/Chapter05/BerryEsseenIntervals.lean
    complete
    def FABL.RealInterval.toSet : FABL.RealInterval → Set ℝ
    def FABL.RealInterval.toSet :
  FABL.RealInterval → Set ℝ
    The subset of `ℝ` represented by a `RealInterval`.
  • theoremdefined in FABL/Chapter05/BerryEsseenIntervals.lean
    complete
    theorem FABL.exercise5_16_strict.{u_1, u_2} {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ}
  (hX : ∀ (k : ι), MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar : ∑ k, ProbabilityTheory.variance (X k) μ = 1)
  (h3 : ∀ (k : ι), MeasureTheory.Integrable (fun ω => |X k ω| ^ 3) μ)
  (x : ℝ) :
  |(MeasureTheory.Measure.map (ProbabilityTheory.sumX X) μ).real
          (Set.Iio x) -
        (ProbabilityTheory.gaussianReal 0 1).real (Set.Iio x)| ≤
    ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ
    theorem FABL.exercise5_16_strict.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ}
  (hX :
    ∀ (k : ι),
      MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar :
    ∑ k,
        ProbabilityTheory.variance (X k)
          μ =
      1)
  (h3 :
    ∀ (k : ι),
      MeasureTheory.Integrable
        (fun ω => |X k ω| ^ 3) μ)
  (x : ℝ) :
  |(MeasureTheory.Measure.map
              (ProbabilityTheory.sumX X)
              μ).real
          (Set.Iio x) -
        (ProbabilityTheory.gaussianReal 0
              1).real
          (Set.Iio x)| ≤
    ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ
    O'Donnell, Exercise 5.16(a): the uniform third-moment Berry--Esseen estimate also holds
for strict lower half-lines.
  • theoremdefined in FABL/Chapter05/BerryEsseenIntervals.lean
    complete
    theorem FABL.exercise5_16_interval.{u_1, u_2} {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ}
  (hX : ∀ (k : ι), MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar : ∑ k, ProbabilityTheory.variance (X k) μ = 1)
  (h3 : ∀ (k : ι), MeasureTheory.Integrable (fun ω => |X k ω| ^ 3) μ)
  (I : FABL.RealInterval) :
  |(MeasureTheory.Measure.map (ProbabilityTheory.sumX X) μ).real
          I.toSet -
        (ProbabilityTheory.gaussianReal 0 1).real I.toSet| ≤
    2 * ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ
    theorem FABL.exercise5_16_interval.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ}
  (hX :
    ∀ (k : ι),
      MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar :
    ∑ k,
        ProbabilityTheory.variance (X k)
          μ =
      1)
  (h3 :
    ∀ (k : ι),
      MeasureTheory.Integrable
        (fun ω => |X k ω| ^ 3) μ)
  (I : FABL.RealInterval) :
  |(MeasureTheory.Measure.map
              (ProbabilityTheory.sumX X)
              μ).real
          I.toSet -
        (ProbabilityTheory.gaussianReal 0
              1).real
          I.toSet| ≤
    2 *
        ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ
    O'Donnell, Exercise 5.16(b): on every bounded or unbounded real interval, with either
choice of endpoint inclusion, the Berry--Esseen error is at most twice the half-line error.
Lemma5.2.5
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
Tagssection-5-2supportexternal-probability-dependencyfidelity-exact

Exercise 5.17 (centering and rescaling Berry--Esseen). Let X_1,\ldots,X_n be independent real-valued random variables with finite means and variances. Write S=\sum_{i=1}^nX_i, \qquad \mu=\sum_{i=1}^n\mathbb E[X_i], \qquad \sigma^2=\sum_{i=1}^n\operatorname{Var}[X_i], and assume \sigma^2>0. If Z\sim N(\mu,\sigma^2) and \epsilon =\sum_{i=1}^n\lVert X_i-\mathbb E[X_i]\rVert_3^3, then for every u\in\mathbb R, \bigl|\Pr[S\le u]-\Pr[Z\le u]\bigr| \le\frac{c\epsilon}{\sigma^3}, where c is the same universal constant as in the Berry--Esseen Theorem.

Lean code for Lemma5.2.5●1 theorem
  • theoremdefined in FABL/Chapter05/BerryEsseenRescaling.lean
    complete
    theorem FABL.exercise5_17.{u_1, u_2} {ι : Type u_1} {Ω : Type u_2} [Fintype ι]
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] (X : ι → Ω → ℝ)
  (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h3 :
    ∀ (i : ι),
      MeasureTheory.Integrable
        (fun ω => |X i ω - ∫ (ω : Ω), X i ω ∂μ| ^ 3) μ)
  (hvariance : 0 < ∑ i, ProbabilityTheory.variance (X i) μ) (x : ℝ) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map (ProbabilityTheory.sumX X) μ))
          x -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal (∑ i, ∫ (ω : Ω), X i ω ∂μ)
                ⟨∑ i, ProbabilityTheory.variance (X i) μ, ⋯⟩))
          x| ≤
    (ProbabilityTheory.thirdMomentBerryEsseenConstant *
        ∑ i, ∫ (ω : Ω), |X i ω - ∫ (ω : Ω), X i ω ∂μ| ^ 3 ∂μ) /
      √(∑ i, ProbabilityTheory.variance (X i) μ) ^ 3
    theorem FABL.exercise5_17.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  (X : ι → Ω → ℝ)
  (hX :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h3 :
    ∀ (i : ι),
      MeasureTheory.Integrable
        (fun ω =>
          |X i ω - ∫ (ω : Ω), X i ω ∂μ| ^
            3)
        μ)
  (hvariance :
    0 <
      ∑ i,
        ProbabilityTheory.variance (X i)
          μ)
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map
                (ProbabilityTheory.sumX X)
                μ))
          x -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                (∑ i, ∫ (ω : Ω), X i ω ∂μ)
                ⟨∑ i,
                    ProbabilityTheory.variance
                      (X i) μ,
                  ⋯⟩))
          x| ≤
    (ProbabilityTheory.thirdMomentBerryEsseenConstant *
        ∑ i,
          ∫ (ω : Ω),
            |X i ω -
                  ∫ (ω : Ω), X i ω ∂μ| ^
              3 ∂μ) /
      √(∑ i,
            ProbabilityTheory.variance
              (X i) μ) ^
        3
    O'Donnell, Exercise 5.17: the uniform third-moment Berry--Esseen estimate for
independent summands with arbitrary finite means and positive total variance.
Lemma5.2.6
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 5.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 5.2.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2supportexternal-probability-dependencyfidelity-explicit-small-parameter-range

Exercise 5.31 (absolute first moments). Let a_1,\ldots,a_n\in\mathbb R satisfy \sum_{i=1}^na_i^2=1 and |a_i|\le\epsilon for every i. For uniformly random x\in\{-1,1\}^n, set S=\sum_{i=1}^na_ix_i, and let Z\sim N(0,1).

(a) For every t\ge0, \Pr[|S|\ge t]\le2e^{-t^2/2}, \qquad \Pr[|Z|\ge t]\le2e^{-t^2/2}.

(b) Using \mathbb E[|Y|]=\int_0^\infty\Pr[|Y|\ge t]\,dt, the Berry--Esseen Theorem, Remark 5.15, and Exercise 5.16, show that for every T\ge1, \bigl|\mathbb E[|S|]-\mathbb E[|Z|]\bigr| \le O\bigl(\epsilon T+e^{-T^2/2}\bigr), with a universal implied constant.

(c) For 0<\epsilon<1, deduce \left|\mathbb E[|S|]-\sqrt{\frac2\pi}\right| \le O\left(\epsilon\sqrt{\log(1/\epsilon)}\right).

(d) Improve this to the universal bound \left|\mathbb E[|S|]-\sqrt{\frac2\pi}\right|\le O(\epsilon) by using the nonuniform Berry--Esseen estimate \bigl|\Pr[S\le u]-\Pr[Z\le u]\bigr| \le\frac{C\gamma}{1+|u|^3} for a universal constant C.

The estimate in part (c) holds with an explicit universal constant on the standard neighbourhood 0<\epsilon\le e^{-1} of zero. This is the literal small-parameter content of the book's estimate; reading the displayed O(\epsilon\sqrt{\log(1/\epsilon)}) as a uniform bound all the way to \epsilon=1 would be false.

Lean code for Lemma5.2.6●4 theorems
  • theoremdefined in FABL/Chapter05/RademacherFirstMoment.lean
    complete
    theorem FABL.exercise5_31a {n : ℕ} (a : Fin n → ℝ) {ε t : ℝ}
  (hnormalized : ∑ i, a i ^ 2 = 1) (_hbound : ∀ (i : Fin n), |a i| ≤ ε)
  (ht : 0 ≤ t) :
  (FABL.rademacherMeasure✝ n).real {x | t ≤ |FABL.linearForm a x|} ≤
      2 * Real.exp (-t ^ 2 / 2) ∧
    (ProbabilityTheory.gaussianReal 0 1).real {z | t ≤ |z|} ≤
      2 * Real.exp (-t ^ 2 / 2)
    theorem FABL.exercise5_31a {n : ℕ} (a : Fin n → ℝ)
  {ε t : ℝ}
  (hnormalized : ∑ i, a i ^ 2 = 1)
  (_hbound : ∀ (i : Fin n), |a i| ≤ ε)
  (ht : 0 ≤ t) :
  (FABL.rademacherMeasure✝ n).real
        {x | t ≤ |FABL.linearForm a x|} ≤
      2 * Real.exp (-t ^ 2 / 2) ∧
    (ProbabilityTheory.gaussianReal 0
            1).real
        {z | t ≤ |z|} ≤
      2 * Real.exp (-t ^ 2 / 2)
    O'Donnell, Exercise 5.31(a): normalized Rademacher sums and a standard Gaussian
have the same two-sided subgaussian tail bound.
  • theoremdefined in FABL/Chapter05/RademacherFirstMoment.lean
    complete
    theorem FABL.exercise5_31b {n : ℕ} (a : Fin n → ℝ) {ε T : ℝ}
  (hnormalized : ∑ i, a i ^ 2 = 1) (hbound : ∀ (i : Fin n), |a i| ≤ ε)
  (hT : 1 ≤ T) :
  |(Finset.univ.expect fun x => |FABL.linearForm a x|) -
        √(2 / Real.pi)| ≤
    2 * ProbabilityTheory.thirdMomentBerryEsseenConstant * ε * T +
      4 * Real.exp (-T ^ 2 / 2)
    theorem FABL.exercise5_31b {n : ℕ} (a : Fin n → ℝ)
  {ε T : ℝ}
  (hnormalized : ∑ i, a i ^ 2 = 1)
  (hbound : ∀ (i : Fin n), |a i| ≤ ε)
  (hT : 1 ≤ T) :
  |(Finset.univ.expect fun x =>
          |FABL.linearForm a x|) -
        √(2 / Real.pi)| ≤
    2 *
            ProbabilityTheory.thirdMomentBerryEsseenConstant *
          ε *
        T +
      4 * Real.exp (-T ^ 2 / 2)
    O'Donnell, Exercise 5.31(b): splitting the layer-cake integral at `T ≥ 1`
combines the uniform Berry--Esseen estimate below `T` with the subgaussian
tails above `T`.
  • theoremdefined in FABL/Chapter05/RademacherFirstMoment.lean
    complete
    theorem FABL.exercise5_31c {n : ℕ} (a : Fin n → ℝ) {ε : ℝ}
  (hnormalized : ∑ i, a i ^ 2 = 1) (hbound : ∀ (i : Fin n), |a i| ≤ ε)
  (hεpos : 0 < ε) (hεsmall : ε ≤ Real.exp (-1)) :
  |(Finset.univ.expect fun x => |FABL.linearForm a x|) -
        √(2 / Real.pi)| ≤
    4 * (ProbabilityTheory.thirdMomentBerryEsseenConstant + 1) * ε *
      √(Real.log (1 / ε))
    theorem FABL.exercise5_31c {n : ℕ} (a : Fin n → ℝ)
  {ε : ℝ} (hnormalized : ∑ i, a i ^ 2 = 1)
  (hbound : ∀ (i : Fin n), |a i| ≤ ε)
  (hεpos : 0 < ε)
  (hεsmall : ε ≤ Real.exp (-1)) :
  |(Finset.univ.expect fun x =>
          |FABL.linearForm a x|) -
        √(2 / Real.pi)| ≤
    4 *
          (ProbabilityTheory.thirdMomentBerryEsseenConstant +
            1) *
        ε *
      √(Real.log (1 / ε))
    O'Donnell, Exercise 5.31(c): choosing
`T = sqrt (2 * log (1 / ε))` in part (b) gives the asserted
`O(ε sqrt (log (1 / ε)))` estimate. The bound is stated on the standard
small-`ε` range `ε ≤ exp (-1)`, which is the formal meaning of the
asymptotic `O` in the exercise.
  • theoremdefined in FABL/Chapter05/RademacherFirstMoment.lean
    complete
    theorem FABL.exercise5_31d :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (a : Fin n → ℝ) {ε : ℝ},
        ∑ i, a i ^ 2 = 1 →
          (∀ (i : Fin n), |a i| ≤ ε) →
            |(Finset.univ.expect fun x => |FABL.linearForm a x|) -
                  √(2 / Real.pi)| ≤
              C * ε
    theorem FABL.exercise5_31d :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (a : Fin n → ℝ) {ε : ℝ},
        ∑ i, a i ^ 2 = 1 →
          (∀ (i : Fin n), |a i| ≤ ε) →
            |(Finset.univ.expect fun x =>
                    |FABL.linearForm a
                        x|) -
                  √(2 / Real.pi)| ≤
              C * ε
    O'Donnell, Exercise 5.31(d): the nonuniform Berry--Esseen theorem gives a
dimension-free linear bound for the absolute first moment of a regular
Rademacher sum.
Theorem5.2.7
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagssection-5-2fidelity-exact

Theorem 5.16. There is a universal constant C such that the following holds. If a_1,\ldots,a_n\in\mathbb R satisfy \sum_{i=1}^na_i^2=1, \qquad |a_i|\le\epsilon\quad\text{for every }i, then \left| \mathbb E_{x\sim\{-1,1\}^n} \left[\left|\sum_{i=1}^na_ix_i\right|\right] -\sqrt{\frac2\pi} \right| \le C\epsilon.

Lean code for Theorem5.2.7●1 theorem
  • theoremdefined in FABL/Chapter05/RademacherFirstMoment.lean
    complete
    theorem FABL.exists_expect_abs_linearForm_sub_sqrt_two_div_pi_le_of_regular :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (a : Fin n → ℝ) {ε : ℝ},
        ∑ i, a i ^ 2 = 1 →
          (∀ (i : Fin n), |a i| ≤ ε) →
            |(Finset.univ.expect fun x => |FABL.linearForm a x|) -
                  √(2 / Real.pi)| ≤
              C * ε
    theorem FABL.exists_expect_abs_linearForm_sub_sqrt_two_div_pi_le_of_regular :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (a : Fin n → ℝ) {ε : ℝ},
        ∑ i, a i ^ 2 = 1 →
          (∀ (i : Fin n), |a i| ≤ ε) →
            |(Finset.univ.expect fun x =>
                    |FABL.linearForm a
                        x|) -
                  √(2 / Real.pi)| ≤
              C * ε
    O'Donnell, Theorem 5.16: the absolute first moment of a normalized regular
Rademacher sum is universally within `O(ε)` of its Gaussian limit.
Lemma5.2.8
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagssection-5-2supportfidelity-exact

Exercise 5.19 (covariance of the correlated sum). Let \rho\in[-1,1], let (x,y) be a \rho-correlated pair of uniformly random strings in \{-1,1\}^n, and define the random vector \widetilde S =\sum_{i=1}^n \begin{pmatrix}x_i/\sqrt n\\y_i/\sqrt n\end{pmatrix} \in\mathbb R^2. \tag{5.7} Then \mathbb E[\widetilde S_1] =\mathbb E[\widetilde S_2]=0, \qquad \mathbb E[\widetilde S_1^2] =\mathbb E[\widetilde S_2^2]=1, \qquad \mathbb E[\widetilde S_1\widetilde S_2]=\rho. Equivalently, \mathbb E[\widetilde S] =\begin{pmatrix}0\\0\end{pmatrix}, \qquad \operatorname{Cov}[\widetilde S] =\begin{pmatrix}1&\rho\\\rho&1\end{pmatrix}.

Lean code for Lemma5.2.8●3 theorems
  • theoremdefined in FABL/Chapter05/CorrelatedMajority.lean
    complete
    theorem FABL.exercise5_19 (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) {n : ℕ}
  (hn : 0 < n) :
  (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
        FABL.correlationFirstCoordinate
          (FABL.normalizedCorrelatedPairSum n xy)) =
      0 ∧
    (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
          FABL.correlationSecondCoordinate
            (FABL.normalizedCorrelatedPairSum n xy)) =
        0 ∧
      (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
            FABL.correlationFirstCoordinate
                (FABL.normalizedCorrelatedPairSum n xy) ^
              2) =
          1 ∧
        (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
              FABL.correlationSecondCoordinate
                  (FABL.normalizedCorrelatedPairSum n xy) ^
                2) =
            1 ∧
          (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
              FABL.correlationFirstCoordinate
                  (FABL.normalizedCorrelatedPairSum n xy) *
                FABL.correlationSecondCoordinate
                  (FABL.normalizedCorrelatedPairSum n xy)) =
            ρ
    theorem FABL.exercise5_19 (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) {n : ℕ}
  (hn : 0 < n) :
  (FABL.pmfExpectation
        (FABL.correlatedPairPMF ρ hρ)
        fun xy =>
        FABL.correlationFirstCoordinate
          (FABL.normalizedCorrelatedPairSum
            n xy)) =
      0 ∧
    (FABL.pmfExpectation
          (FABL.correlatedPairPMF ρ hρ)
          fun xy =>
          FABL.correlationSecondCoordinate
            (FABL.normalizedCorrelatedPairSum
              n xy)) =
        0 ∧
      (FABL.pmfExpectation
            (FABL.correlatedPairPMF ρ hρ)
            fun xy =>
            FABL.correlationFirstCoordinate
                (FABL.normalizedCorrelatedPairSum
                  n xy) ^
              2) =
          1 ∧
        (FABL.pmfExpectation
              (FABL.correlatedPairPMF ρ
                hρ)
              fun xy =>
              FABL.correlationSecondCoordinate
                  (FABL.normalizedCorrelatedPairSum
                    n xy) ^
                2) =
            1 ∧
          (FABL.pmfExpectation
              (FABL.correlatedPairPMF ρ
                hρ)
              fun xy =>
              FABL.correlationFirstCoordinate
                  (FABL.normalizedCorrelatedPairSum
                    n xy) *
                FABL.correlationSecondCoordinate
                  (FABL.normalizedCorrelatedPairSum
                    n xy)) =
            ρ
    Exercise 5.19: the two normalized correlated vote margins are centered, have unit second
moments, and have cross moment `ρ`.
  • theoremdefined in FABL/Chapter05/CorrelatedMajority.lean
    complete
    theorem FABL.normalizedCorrelatedPairSum_projection_mean (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) {n : ℕ} (t : FABL.CorrelationPlane) :
  (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
      inner ℝ (FABL.normalizedCorrelatedPairSum n xy) t) =
    0
    theorem FABL.normalizedCorrelatedPairSum_projection_mean
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1)
  {n : ℕ} (t : FABL.CorrelationPlane) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy =>
      inner ℝ
        (FABL.normalizedCorrelatedPairSum
          n xy)
        t) =
    0
    The mean vector in Exercise 5.19 is zero, expressed by testing every linear functional.
  • theoremdefined in FABL/Chapter05/CorrelatedMajority.lean
    complete
    theorem FABL.normalizedCorrelatedPairSum_projection_secondMoment (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) {n : ℕ} (hn : 0 < n)
  (t : FABL.CorrelationPlane) :
  (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
      inner ℝ (FABL.normalizedCorrelatedPairSum n xy) t ^ 2) =
    FABL.correlationQuadraticForm ρ t
    theorem FABL.normalizedCorrelatedPairSum_projection_secondMoment
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1)
  {n : ℕ} (hn : 0 < n)
  (t : FABL.CorrelationPlane) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy =>
      inner ℝ
          (FABL.normalizedCorrelatedPairSum
            n xy)
          t ^
        2) =
    FABL.correlationQuadraticForm ρ t
    The covariance matrix in Exercise 5.19 is `[[1, ρ], [ρ, 1]]`, expressed by its quadratic
form on every direction.
Theorem5.2.9
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.2.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2fidelity-exact-canonical-law

Sheppard's Formula. Let z_1,z_2 be standard Gaussian random variables with correlation \mathbb E[z_1z_2]=\rho\in[-1,1]. Then \Pr[z_1\le0,\ z_2\le0] =\frac12-\frac12\frac{\arccos\rho}{\pi}. The book defers its rotational-symmetry proof to Example 11.19. Alternatively, the formula follows directly from the Gaussian-disagreement identity in Theorem 2.45.

Lean code for Theorem5.2.9●1 theorem
  • theoremdefined in FABL/Chapter05/GaussianThresholds.lean
    complete
    theorem FABL.sheppardsFormula (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  (↑(FABL.correlatedGaussianMeasure ρ)).real
      {z |
        FABL.correlationFirstCoordinate z ≤ 0 ∧
          FABL.correlationSecondCoordinate z ≤ 0} =
    1 / 2 - 1 / 2 * (Real.arccos ρ / Real.pi)
    theorem FABL.sheppardsFormula (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) :
  (↑(FABL.correlatedGaussianMeasure
            ρ)).real
      {z |
        FABL.correlationFirstCoordinate
              z ≤
            0 ∧
          FABL.correlationSecondCoordinate
              z ≤
            0} =
    1 / 2 -
      1 / 2 * (Real.arccos ρ / Real.pi)
    O'Donnell, Sheppard's Formula: the canonical correlated Gaussian law represents the
book's pair of standard Gaussian random variables with correlation `ρ`; its lower-left quadrant
has the stated probability.
Theorem5.2.10
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.2.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-2external-probability-dependencyfidelity-positive-definite-specialization

Theorem 5.38 (multidimensional Berry--Esseen). There is a universal constant C with the following property. Let X_1,\ldots,X_n be independent \mathbb R^d-valued random vectors, each having mean zero. Set S=\sum_{i=1}^nX_i, \qquad \Sigma=\operatorname{Cov}[S], and assume that \Sigma is invertible. Let Z\sim N(0,\Sigma). Then for every convex set U\subseteq\mathbb R^d, \bigl|\Pr[S\in U]-\Pr[Z\in U]\bigr| \le C d^{1/4}\gamma, \qquad \gamma =\sum_{i=1}^n \mathbb E\!\left[ \left\lVert\Sigma^{-1/2}X_i\right\rVert_2^3 \right]. Here \lVert\cdot\rVert_2 is the Euclidean norm on \mathbb R^d.

For a covariance matrix, invertibility is equivalent to positive definiteness, so the hypothesis may equivalently be written \Sigma\succ0.

Lean code for Theorem5.2.10●1 theorem
  • theoremdefined in ProbabilityApproximation/Bentkus/Induction.lean
    complete
    theorem ProbabilityTheory.exists_bentkus_convex_set_constant.{u} :
  ∃ C,
    0 < C ∧
      ∀ {d n : ℕ},
        0 < d →
          ∀ {Ω : Type u} [inst : MeasurableSpace Ω]
            (μ : MeasureTheory.Measure Ω)
            [MeasureTheory.IsProbabilityMeasure μ]
            (X : Fin n → Ω → EuclideanSpace ℝ (Fin d))
            (S : Matrix (Fin d) (Fin d) ℝ),
            (∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) →
              ProbabilityTheory.iIndepFun X μ →
                (∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) →
                  S.PosDef →
                    (∀ (x y : EuclideanSpace ℝ (Fin d)),
                        ((ProbabilityTheory.covarianceBilin
                                (MeasureTheory.Measure.map
                                  (fun ω => ∑ i, X i ω) μ))
                              x)
                            y =
                          x.ofLp ⬝ᵥ S.mulVec y.ofLp) →
                      ∀ (A : Set (EuclideanSpace ℝ (Fin d))),
                        MeasurableSet A →
                          Convexity.IsConvexSet ℝ A →
                            |((MeasureTheory.Measure.map
                                        (fun ω => ∑ i, X i ω) μ)
                                      A).toReal -
                                  ((ProbabilityTheory.multivariateGaussian
                                        0 S)
                                      A).toReal| ≤
                              C * ↑d ^ (1 / 4) *
                                ∑ i,
                                  ∫ (ω : Ω),
                                    ‖(Matrix.toEuclideanCLM
                                            (CFC.sqrt S)⁻¹)
                                          (X i ω)‖ ^
                                      3 ∂μ
    theorem ProbabilityTheory.exists_bentkus_convex_set_constant.{u} :
  ∃ C,
    0 < C ∧
      ∀ {d n : ℕ},
        0 < d →
          ∀ {Ω : Type u}
            [inst : MeasurableSpace Ω]
            (μ : MeasureTheory.Measure Ω)
            [MeasureTheory.IsProbabilityMeasure
                μ]
            (X :
              Fin n →
                Ω →
                  EuclideanSpace ℝ
                    (Fin d))
            (S :
              Matrix (Fin d) (Fin d) ℝ),
            (∀ (i : Fin n),
                MeasureTheory.MemLp (X i)
                  3 μ) →
              ProbabilityTheory.iIndepFun
                  X μ →
                (∀ (i : Fin n),
                    ∫ (ω : Ω), X i ω ∂μ =
                      0) →
                  S.PosDef →
                    (∀
                        (x y :
                          EuclideanSpace ℝ
                            (Fin d)),
                        ((ProbabilityTheory.covarianceBilin
                                (MeasureTheory.Measure.map
                                  (fun
                                      ω =>
                                    ∑ i,
                                      X i
                                        ω)
                                  μ))
                              x)
                            y =
                          x.ofLp ⬝ᵥ
                            S.mulVec
                              y.ofLp) →
                      ∀
                        (A :
                          Set
                            (EuclideanSpace
                              ℝ (Fin d))),
                        MeasurableSet A →
                          Convexity.IsConvexSet
                              ℝ A →
                            |((MeasureTheory.Measure.map
                                        (fun
                                            ω =>
                                          ∑
                                            i,
                                            X
                                              i
                                              ω)
                                        μ)
                                      A).toReal -
                                  ((ProbabilityTheory.multivariateGaussian
                                        0
                                        S)
                                      A).toReal| ≤
                              C *
                                  ↑d ^
                                    (1 /
                                      4) *
                                ∑ i,
                                  ∫ (ω :
                                    Ω),
                                    ‖(Matrix.toEuclideanCLM
                                            (CFC.sqrt
                                                S)⁻¹)
                                          (X
                                            i
                                            ω)‖ ^
                                      3 ∂μ
    Bentkus's multivariate Berry--Esseen theorem for measurable convex sets.
Lemma5.2.11
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 2.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-2supportexternal-probability-dependencyfidelity-exact

Exercise 5.33 (the two-dimensional CLT calculation). Use Theorem 5.38 to complete the proof of Theorem 5.17.

(a) For \Sigma=\begin{pmatrix}1&\rho\\\rho&1\end{pmatrix}, \qquad -1<\rho<1, show that \Sigma^{-1} = \begin{pmatrix}1&-\rho\\0&1\end{pmatrix} \begin{pmatrix}1&0\\0&(1-\rho^2)^{-1}\end{pmatrix} \begin{pmatrix}1&0\\-\rho&1\end{pmatrix}.

(b) If y=(\pm a,\pm a)^{\mathsf T}\in\mathbb R^2, compute y^{\mathsf T}\Sigma^{-1}y. It equals \frac{2a^2}{1+\rho} \quad\text{when the two signs agree}, \qquad \frac{2a^2}{1-\rho} \quad\text{when the two signs disagree}.

(c) Apply the multidimensional Berry--Esseen estimate to the four quadrants, use Sheppard's Formula, and complete the proof of Theorem 5.17.

Lean code for Lemma5.2.11●12 declarations
  • defdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    def FABL.correlationMatrix (ρ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ
    def FABL.correlationMatrix (ρ : ℝ) :
  Matrix (Fin 2) (Fin 2) ℝ
    The covariance matrix of two standard random variables with correlation `ρ`.
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.exercise5_33a {ρ : ℝ} (hρ : ρ ∈ Set.Ioo (-1) 1) :
  (FABL.correlationMatrix ρ)⁻¹ =
    !![1, -ρ; 0, 1] * !![1, 0; 0, (1 - ρ ^ 2)⁻¹] * !![1, 0; -ρ, 1]
    theorem FABL.exercise5_33a {ρ : ℝ}
  (hρ : ρ ∈ Set.Ioo (-1) 1) :
  (FABL.correlationMatrix ρ)⁻¹ =
    !![1, -ρ; 0, 1] *
        !![1, 0; 0, (1 - ρ ^ 2)⁻¹] *
      !![1, 0; -ρ, 1]
    O'Donnell, Exercise 5.33(a): the inverse of the bivariate correlation matrix in the
factorization used to evaluate its quadratic form.
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.exercise5_33b_sameSigns {ρ a : ℝ} (hρ : ρ ∈ Set.Ioo (-1) 1)
  (s : FABL.Sign) :
  have y := ![FABL.signValue s * a, FABL.signValue s * a];
  y ⬝ᵥ (FABL.correlationMatrix ρ)⁻¹.mulVec y = 2 * a ^ 2 / (1 + ρ)
    theorem FABL.exercise5_33b_sameSigns {ρ a : ℝ}
  (hρ : ρ ∈ Set.Ioo (-1) 1)
  (s : FABL.Sign) :
  have y :=
    ![FABL.signValue s * a,
      FABL.signValue s * a];
  y ⬝ᵥ
      (FABL.correlationMatrix ρ)⁻¹.mulVec
        y =
    2 * a ^ 2 / (1 + ρ)
    O'Donnell, Exercise 5.33(b), equal-sign case: the inverse-covariance quadratic form of
`(±a, ±a)` is `2a² / (1 + ρ)`.
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.exercise5_33b_oppositeSigns {ρ a : ℝ} (hρ : ρ ∈ Set.Ioo (-1) 1)
  (s : FABL.Sign) :
  have y := ![FABL.signValue s * a, -(FABL.signValue s * a)];
  y ⬝ᵥ (FABL.correlationMatrix ρ)⁻¹.mulVec y = 2 * a ^ 2 / (1 - ρ)
    theorem FABL.exercise5_33b_oppositeSigns {ρ a : ℝ}
  (hρ : ρ ∈ Set.Ioo (-1) 1)
  (s : FABL.Sign) :
  have y :=
    ![FABL.signValue s * a,
      -(FABL.signValue s * a)];
  y ⬝ᵥ
      (FABL.correlationMatrix ρ)⁻¹.mulVec
        y =
    2 * a ^ 2 / (1 - ρ)
    O'Donnell, Exercise 5.33(b), opposite-sign case: the inverse-covariance quadratic form
of `(±a, ∓a)` is `2a² / (1 - ρ)`.
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.correlationMatrix_posDef {ρ : ℝ} (hρ : ρ ∈ Set.Ioo (-1) 1) :
  (FABL.correlationMatrix ρ).PosDef
    theorem FABL.correlationMatrix_posDef {ρ : ℝ}
  (hρ : ρ ∈ Set.Ioo (-1) 1) :
  (FABL.correlationMatrix ρ).PosDef
    The bivariate correlation matrix is positive definite away from the degenerate
correlations `±1`.
  • defdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    def FABL.regularCorrelatedSignSummand (c : ℝ) (z : FABL.Sign × FABL.Sign) :
  EuclideanSpace ℝ (Fin 2)
    def FABL.regularCorrelatedSignSummand (c : ℝ)
  (z : FABL.Sign × FABL.Sign) :
  EuclideanSpace ℝ (Fin 2)
    A single correlated sign pair scaled by one threshold coefficient.
  • defdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    def FABL.regularThresholdPairSummand {n : ℕ} (a : Fin n → ℝ) (i : Fin n)
  (xy : FABL.SignCube n × FABL.SignCube n) : EuclideanSpace ℝ (Fin 2)
    def FABL.regularThresholdPairSummand {n : ℕ}
  (a : Fin n → ℝ) (i : Fin n)
  (xy :
    FABL.SignCube n × FABL.SignCube n) :
  EuclideanSpace ℝ (Fin 2)
    The `i`th planar summand attached to a correlated pair and a coefficient vector.
  • defdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    def FABL.regularThresholdPairSum {n : ℕ} (a : Fin n → ℝ)
  (xy : FABL.SignCube n × FABL.SignCube n) : EuclideanSpace ℝ (Fin 2)
    def FABL.regularThresholdPairSum {n : ℕ}
  (a : Fin n → ℝ)
  (xy :
    FABL.SignCube n × FABL.SignCube n) :
  EuclideanSpace ℝ (Fin 2)
    The planar pair of homogeneous linear forms is the sum of its coordinate summands.
  • defdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    def FABL.signQuadrant (s t : FABL.Sign) : Set (EuclideanSpace ℝ (Fin 2))
    def FABL.signQuadrant (s t : FABL.Sign) :
  Set (EuclideanSpace ℝ (Fin 2))
    A closed quadrant indexed by the desired signs of its two coordinates.
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.measurableSet_signQuadrant (s t : FABL.Sign) :
  MeasurableSet (FABL.signQuadrant s t)
    theorem FABL.measurableSet_signQuadrant
  (s t : FABL.Sign) :
  MeasurableSet (FABL.signQuadrant s t)
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.isConvexSet_signQuadrant (s t : FABL.Sign) :
  Convexity.IsConvexSet ℝ (FABL.signQuadrant s t)
    theorem FABL.isConvexSet_signQuadrant
  (s t : FABL.Sign) :
  Convexity.IsConvexSet ℝ
    (FABL.signQuadrant s t)
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.exists_exercise5_33c_constant :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} {ρ ε : ℝ} (hρ : ρ ∈ Set.Ioo (-1) 1) (a : Fin n → ℝ),
        ∑ i, a i ^ 2 = 1 →
          (∀ (i : Fin n), |a i| ≤ ε) →
            ∀ (s t : FABL.Sign),
              |((MeasureTheory.Measure.map
                          (FABL.regularThresholdPairSum a)
                          (FABL.correlatedPairPMF ρ ⋯).toMeasure)
                        (FABL.signQuadrant s t)).toReal -
                    ((ProbabilityTheory.multivariateGaussian 0
                          (FABL.correlationMatrix ρ))
                        (FABL.signQuadrant s t)).toReal| ≤
                C * ε / √(1 - ρ ^ 2)
    theorem FABL.exists_exercise5_33c_constant :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} {ρ ε : ℝ}
        (hρ : ρ ∈ Set.Ioo (-1) 1)
        (a : Fin n → ℝ),
        ∑ i, a i ^ 2 = 1 →
          (∀ (i : Fin n), |a i| ≤ ε) →
            ∀ (s t : FABL.Sign),
              |((MeasureTheory.Measure.map
                          (FABL.regularThresholdPairSum
                            a)
                          (FABL.correlatedPairPMF
                              ρ
                              ⋯).toMeasure)
                        (FABL.signQuadrant
                          s t)).toReal -
                    ((ProbabilityTheory.multivariateGaussian
                          0
                          (FABL.correlationMatrix
                            ρ))
                        (FABL.signQuadrant
                          s t)).toReal| ≤
                C * ε / √(1 - ρ ^ 2)
    O'Donnell, Exercise 5.33(c): Bentkus's theorem controls each of the four
quadrants for the pair of regular homogeneous linear forms.
Theorem5.2.12
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-2fidelity-exact

Theorem 5.17. There is a universal constant C such that the following holds. Let f:\{-1,1\}^n\to\{-1,1\} be an unbiased homogeneous linear threshold function, f(x)=\operatorname{sgn}\left(\sum_{i=1}^na_ix_i\right), \qquad \mathbb E[f]=0, whose coefficients satisfy \sum_{i=1}^na_i^2=1, \qquad |a_i|\le\epsilon\quad\text{for every }i. Then for every \rho\in(-1,1), \left| \operatorname{Stab}_\rho[f]-\frac2\pi\arcsin\rho \right| \le \frac{C\epsilon}{\sqrt{1-\rho^2}}.

Lean code for Theorem5.2.12●1 theorem
  • theoremdefined in FABL/Chapter05/RegularThresholdNoiseStability.lean
    complete
    theorem FABL.exists_noiseStability_sub_arcsine_le_of_regular_homogeneous_threshold :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (f : FABL.BooleanFunction n) (a : Fin n → ℝ) {ε ρ : ℝ},
        FABL.IsBalanced f.toReal →
          (∀ (x : FABL.SignCube n),
              f x = FABL.thresholdSign (FABL.linearForm a x)) →
            ∑ i, a i ^ 2 = 1 →
              (∀ (i : Fin n), |a i| ≤ ε) →
                ∀ (hρ : ρ ∈ Set.Ioo (-1) 1),
                  |FABL.noiseStability ρ ⋯ f.toReal -
                        2 / Real.pi * Real.arcsin ρ| ≤
                    C * ε / √(1 - ρ ^ 2)
    theorem FABL.exists_noiseStability_sub_arcsine_le_of_regular_homogeneous_threshold :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ}
        (f : FABL.BooleanFunction n)
        (a : Fin n → ℝ) {ε ρ : ℝ},
        FABL.IsBalanced f.toReal →
          (∀ (x : FABL.SignCube n),
              f x =
                FABL.thresholdSign
                  (FABL.linearForm a x)) →
            ∑ i, a i ^ 2 = 1 →
              (∀ (i : Fin n), |a i| ≤ ε) →
                ∀
                  (hρ :
                    ρ ∈ Set.Ioo (-1) 1),
                  |FABL.noiseStability ρ ⋯
                          f.toReal -
                        2 / Real.pi *
                          Real.arcsin ρ| ≤
                    C * ε / √(1 - ρ ^ 2)
    O'Donnell, Theorem 5.17: the noise stability of an unbiased regular
homogeneous linear threshold function is within the Berry--Esseen error of the
Gaussian arcsine law.
Theorem5.2.13
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-5-2fidelity-exact

Theorem 5.18. There is a universal constant C such that for every \rho\in[0,1), the sequence \operatorname{Stab}_\rho[\operatorname{Maj}_n] is decreasing as n ranges through the positive odd integers, and for every such n, \frac2\pi\arcsin\rho \le \operatorname{Stab}_\rho[\operatorname{Maj}_n] \le \frac2\pi\arcsin\rho + \frac{C}{\sqrt{1-\rho^2}\sqrt n}.

Lean code for Theorem5.2.13●1 theorem
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.exists_majorityNoiseStability_constant :
  ∃ C,
    0 < C ∧
      ∀ (ρ : ℝ) (hρ : ρ ∈ Set.Ico 0 1),
        (Antitone fun m =>
            FABL.noiseStability ρ ⋯
              (FABL.majority (2 * m + 1)).toReal) ∧
          ∀ (m : ℕ),
            2 / Real.pi * Real.arcsin ρ ≤
                FABL.noiseStability ρ ⋯
                  (FABL.majority (2 * m + 1)).toReal ∧
              FABL.noiseStability ρ ⋯
                  (FABL.majority (2 * m + 1)).toReal ≤
                2 / Real.pi * Real.arcsin ρ +
                  C / (√(1 - ρ ^ 2) * √↑(2 * m + 1))
    theorem FABL.exists_majorityNoiseStability_constant :
  ∃ C,
    0 < C ∧
      ∀ (ρ : ℝ) (hρ : ρ ∈ Set.Ico 0 1),
        (Antitone fun m =>
            FABL.noiseStability ρ ⋯
              (FABL.majority
                  (2 * m + 1)).toReal) ∧
          ∀ (m : ℕ),
            2 / Real.pi * Real.arcsin ρ ≤
                FABL.noiseStability ρ ⋯
                  (FABL.majority
                      (2 * m +
                        1)).toReal ∧
              FABL.noiseStability ρ ⋯
                  (FABL.majority
                      (2 * m +
                        1)).toReal ≤
                2 / Real.pi *
                    Real.arcsin ρ +
                  C /
                    (√(1 - ρ ^ 2) *
                      √↑(2 * m + 1))
    O'Donnell, Theorem 5.18 and Exercise 5.23. The endpoint `ρ = 0`
is non-strict: all odd-majority stabilities there equal zero.
Theorem5.2.14
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 2.2.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagssection-5-2deferredlater-chapter-dependency

Majority Is Stablest Theorem. Fix \rho\in(0,1). If f:\{-1,1\}^n\to[-1,1] satisfies \mathbb E[f]=0, \qquad \operatorname{MaxInf}[f]\le\tau, then \operatorname{Stab}_\rho[f] \le\frac2\pi\arcsin\rho+o_\tau(1) =1-\frac2\pi\arccos\rho+o_\tau(1). Precisely, for every \eta>0 there is a \tau_0>0, depending only on \rho and \eta, such that whenever 0\le\tau\le\tau_0 the first upper bound holds with \eta in place of o_\tau(1).

Section 5.4 proves only the sufficiently-small-\rho case. The full theorem is deferred to Chapter 11.