2.2. Gaussian companions and rotation🔗

Theorem2.2.1

uses 0

Used by 5

Reverse dependency previews

Preview

Lemma 2.2.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkusgaussian-replacementprobability-transportsource-bentkus-2004fidelity-canonical-product-realization

Gaussian companions and canonical probability-space transport. Let X_i:\Omega\to\mathbb R^d be a finite measurable family on a probability space (\Omega,\mu), put \nu_i=\mathcal L_\mu(X_i), and let \Sigma_i be the matrix of the covariance bilinear form of \nu_i. Then \Sigma_i is positive semidefinite, and the canonical Gaussian product \Gamma=\bigotimes_i N(0,\Sigma_i) has independent coordinate variables Y_i that are centered, belong to L^3, and satisfy \operatorname{Cov}(Y_i)[u,v] =\operatorname{Cov}_{\nu_i}[u,v]\qquad(u,v\in\mathbb R^d). The marginal-law product \nu=\bigotimes_i\nu_i is a probability measure whose coordinate variables \widetilde X_i are independent. If the original X_i are independent, then \mathcal L_\mu((X_i)_i)=\nu,\qquad \mathcal L_\mu\!\left(\sum_iX_i\right) =\mathcal L_\nu\!\left(\sum_i\widetilde X_i\right). Finally, the product \nu\otimes\Gamma carries the two coordinate families (\widetilde X_i)_i and (Y_i)_i on one probability space. Each family is mutually independent, the two coordinate blocks are independent, and hence every \widetilde X_i is independent of every Y_j. On this product space the original coordinate retains law \nu_i, the Gaussian coordinate retains law N(0,\Sigma_i), and their covariance bilinear forms agree.

Lean code for Theorem2.2.1●32 declarations

defdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

def ProbabilityTheory.covarianceMatrix {d : ℕ}
  (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))) :
  Matrix (Fin d) (Fin d) ℝ

def ProbabilityTheory.covarianceMatrix {d : ℕ}
  (ν :
    MeasureTheory.Measure
      (EuclideanSpace ℝ (Fin d))) :
  Matrix (Fin d) (Fin d) ℝ

The covariance matrix of a probability law on Euclidean space, written in the canonical
orthonormal basis.  This definition remains meaningful without moment hypotheses because
`covarianceBilin` is defined to be zero when the second moment is infinite.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

theorem ProbabilityTheory.covarianceMatrix_posSemidef {d : ℕ}
  (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))) :
  (ProbabilityTheory.covarianceMatrix ν).PosSemidef

theorem ProbabilityTheory.covarianceMatrix_posSemidef
  {d : ℕ}
  (ν :
    MeasureTheory.Measure
      (EuclideanSpace ℝ (Fin d))) :
  (ProbabilityTheory.covarianceMatrix
      ν).PosSemidef

Every covariance matrix is positive semidefinite, including in the singular case.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

theorem ProbabilityTheory.dotProduct_covarianceMatrix_mulVec {d : ℕ}
  (ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d)))
  (x y : EuclideanSpace ℝ (Fin d)) :
  x.ofLp ⬝ᵥ (ProbabilityTheory.covarianceMatrix ν).mulVec y.ofLp =
    ((ProbabilityTheory.covarianceBilin ν) x) y

theorem ProbabilityTheory.dotProduct_covarianceMatrix_mulVec
  {d : ℕ}
  (ν :
    MeasureTheory.Measure
      (EuclideanSpace ℝ (Fin d)))
  (x y : EuclideanSpace ℝ (Fin d)) :
  x.ofLp ⬝ᵥ
      (ProbabilityTheory.covarianceMatrix
            ν).mulVec
        y.ofLp =
    ((ProbabilityTheory.covarianceBilin ν)
        x)
      y

The matrix form of `covarianceMatrix` recovers the covariance bilinear form.

defdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

def ProbabilityTheory.gaussianCompanion {n d : ℕ} (i : Fin n) :
  (Fin n → EuclideanSpace ℝ (Fin d)) → EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.gaussianCompanion
  {n d : ℕ} (i : Fin n) :
  (Fin n → EuclideanSpace ℝ (Fin d)) →
    EuclideanSpace ℝ (Fin d)

The `i`th coordinate on the canonical Gaussian-companion product space.

defdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

def ProbabilityTheory.summandCovarianceMatrix.{u_1} {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (i : Fin n) :
  Matrix (Fin d) (Fin d) ℝ

def ProbabilityTheory.summandCovarianceMatrix.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (i : Fin n) : Matrix (Fin d) (Fin d) ℝ

The covariance matrix of the `i`th summand law.

defdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

def ProbabilityTheory.gaussianCompanionMeasureOf.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Measure (Fin n → EuclideanSpace ℝ (Fin d))

def ProbabilityTheory.gaussianCompanionMeasureOf.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n →
      Ω → EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Measure
    (Fin n → EuclideanSpace ℝ (Fin d))

The canonical product law for the Gaussian companions of a given summand family.  This is the
probability-space realization of the family `Y₁, …, Yₙ` introduced in Bentkus (2004), (3.2).

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

theorem ProbabilityTheory.iIndepFun_gaussianCompanion_of.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) :
  ProbabilityTheory.iIndepFun
    (fun i => ProbabilityTheory.gaussianCompanion i)
    (ProbabilityTheory.gaussianCompanionMeasureOf μ X)

theorem ProbabilityTheory.iIndepFun_gaussianCompanion_of.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n →
      Ω → EuclideanSpace ℝ (Fin d)) :
  ProbabilityTheory.iIndepFun
    (fun i =>
      ProbabilityTheory.gaussianCompanion
        i)
    (ProbabilityTheory.gaussianCompanionMeasureOf
      μ X)

The companion coordinates associated with a summand family are mutually independent.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

theorem ProbabilityTheory.integral_gaussianCompanion_of_eq_zero.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (i : Fin n) :
  ∫ (ω : Fin n → EuclideanSpace ℝ (Fin d)),
      ProbabilityTheory.gaussianCompanion i
        ω ∂ProbabilityTheory.gaussianCompanionMeasureOf μ X =
    0

theorem ProbabilityTheory.integral_gaussianCompanion_of_eq_zero.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (i : Fin n) :
  ∫ (ω :
      Fin n → EuclideanSpace ℝ (Fin d)),
      ProbabilityTheory.gaussianCompanion
        i
        ω ∂ProbabilityTheory.gaussianCompanionMeasureOf
        μ X =
    0

Every companion associated with a summand family is centered.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

theorem ProbabilityTheory.memLp_three_gaussianCompanion_of.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (i : Fin n) :
  MeasureTheory.MemLp (ProbabilityTheory.gaussianCompanion i) 3
    (ProbabilityTheory.gaussianCompanionMeasureOf μ X)

theorem ProbabilityTheory.memLp_three_gaussianCompanion_of.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (i : Fin n) :
  MeasureTheory.MemLp
    (ProbabilityTheory.gaussianCompanion
      i)
    3
    (ProbabilityTheory.gaussianCompanionMeasureOf
      μ X)

Every companion associated with a summand family has a finite third moment.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanions.lean

complete

theorem ProbabilityTheory.covarianceBilin_map_gaussianCompanion_of.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (i : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.gaussianCompanion i)
            (ProbabilityTheory.gaussianCompanionMeasureOf μ X)))
        x)
      y =
    ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map (X i) μ))
        x)
      y

theorem ProbabilityTheory.covarianceBilin_map_gaussianCompanion_of.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (i : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.gaussianCompanion
              i)
            (ProbabilityTheory.gaussianCompanionMeasureOf
              μ X)))
        x)
      y =
    ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map (X i)
            μ))
        x)
      y

Each canonical Gaussian companion has exactly the covariance bilinear form of the
corresponding summand law, including when that covariance is singular.

defdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

def ProbabilityTheory.independentLawProduct.{u_1, u_2} {n : ℕ}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [MeasurableSpace E]
  (μ : MeasureTheory.Measure Ω) (X : Fin n → Ω → E) :
  MeasureTheory.Measure (Fin n → E)

def ProbabilityTheory.independentLawProduct.{u_1,
    u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace E]
  (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → E) :
  MeasureTheory.Measure (Fin n → E)

Product of the marginal laws of a finite family.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.isProbabilityMeasure_independentLawProduct.{u_1, u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [MeasurableSpace E] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  MeasureTheory.IsProbabilityMeasure
    (ProbabilityTheory.independentLawProduct μ X)

theorem ProbabilityTheory.isProbabilityMeasure_independentLawProduct.{u_1,
    u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace E]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  MeasureTheory.IsProbabilityMeasure
    (ProbabilityTheory.independentLawProduct
      μ X)

The product of marginal laws is a probability measure when the original family is
measurable.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.iIndepFun_independentLawProduct.{u_1, u_2} {n : ℕ}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [MeasurableSpace E]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E} (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.iIndepFun (fun i x => x i)
    (ProbabilityTheory.independentLawProduct μ X)

theorem ProbabilityTheory.iIndepFun_independentLawProduct.{u_1,
    u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace E]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.iIndepFun
    (fun i x => x i)
    (ProbabilityTheory.independentLawProduct
      μ X)

The coordinate family on the product of marginal laws is independent.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.map_coordinate_independentLawProduct.{u_1, u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [MeasurableSpace E] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  MeasureTheory.Measure.map (fun x => x i)
      (ProbabilityTheory.independentLawProduct μ X) =
    MeasureTheory.Measure.map (X i) μ

theorem ProbabilityTheory.map_coordinate_independentLawProduct.{u_1,
    u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace E]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  MeasureTheory.Measure.map (fun x => x i)
      (ProbabilityTheory.independentLawProduct
        μ X) =
    MeasureTheory.Measure.map (X i) μ

Each coordinate of the marginal-law product has the corresponding original marginal law.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.map_family_eq_independentLawProduct.{u_1, u_2} {n : ℕ}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [MeasurableSpace E]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E} (hX : ∀ (i : Fin n), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ) :
  MeasureTheory.Measure.map (fun ω i => X i ω) μ =
    ProbabilityTheory.independentLawProduct μ X

theorem ProbabilityTheory.map_family_eq_independentLawProduct.{u_1,
    u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace E]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ) :
  MeasureTheory.Measure.map
      (fun ω i => X i ω) μ =
    ProbabilityTheory.independentLawProduct
      μ X

The joint law of an independent family is the product of its marginal laws.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.map_sum_eq_map_sum_independentLawProduct.{u_1, u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [MeasurableSpace E] [NormedAddCommGroup E] [MeasurableAdd₂ E]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E} (hX : ∀ (i : Fin n), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ) :
  MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ =
    MeasureTheory.Measure.map (fun x => ∑ i, x i)
      (ProbabilityTheory.independentLawProduct μ X)

theorem ProbabilityTheory.map_sum_eq_map_sum_independentLawProduct.{u_1,
    u_2}
  {n : ℕ} {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace E]
  [NormedAddCommGroup E]
  [MeasurableAdd₂ E]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → E}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ) :
  MeasureTheory.Measure.map
      (fun ω => ∑ i, X i ω) μ =
    MeasureTheory.Measure.map
      (fun x => ∑ i, x i)
      (ProbabilityTheory.independentLawProduct
        μ X)

Transport of the finite sum from the user's probability space to the canonical product of
marginal laws.

defdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

def ProbabilityTheory.bentkusReplacementMeasure.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Measure
    ((Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d)))

def ProbabilityTheory.bentkusReplacementMeasure.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n →
      Ω → EuclideanSpace ℝ (Fin d)) :
  MeasureTheory.Measure
    ((Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d)))

Product probability space carrying both the canonical original summands and their Gaussian
companions.

defdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

def ProbabilityTheory.replacementOriginal {n d : ℕ} (i : Fin n) :
  (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d)) →
    EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.replacementOriginal
  {n d : ℕ} (i : Fin n) :
  (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d)) →
    EuclideanSpace ℝ (Fin d)

The original-coordinate family on the replacement space.

defdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

def ProbabilityTheory.replacementGaussian {n d : ℕ} (i : Fin n) :
  (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d)) →
    EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.replacementGaussian
  {n d : ℕ} (i : Fin n) :
  (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d)) →
    EuclideanSpace ℝ (Fin d)

The Gaussian-coordinate family on the replacement space.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.indepFun_replacement_blocks.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.IndepFun Prod.fst Prod.snd
    (ProbabilityTheory.bentkusReplacementMeasure μ X)

theorem ProbabilityTheory.indepFun_replacement_blocks.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.IndepFun Prod.fst
    Prod.snd
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)

The two coordinate blocks of the replacement space are independent.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.indepFun_replacementOriginal_replacementGaussian.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i j : Fin n) :
  ProbabilityTheory.IndepFun (ProbabilityTheory.replacementOriginal i)
    (ProbabilityTheory.replacementGaussian j)
    (ProbabilityTheory.bentkusReplacementMeasure μ X)

theorem ProbabilityTheory.indepFun_replacementOriginal_replacementGaussian.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i j : Fin n) :
  ProbabilityTheory.IndepFun
    (ProbabilityTheory.replacementOriginal
      i)
    (ProbabilityTheory.replacementGaussian
      j)
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)

Every original coordinate is independent of every Gaussian coordinate on the replacement
space.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.map_replacementOriginal.{u_1} {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  MeasureTheory.Measure.map (ProbabilityTheory.replacementOriginal i)
      (ProbabilityTheory.bentkusReplacementMeasure μ X) =
    MeasureTheory.Measure.map (X i) μ

theorem ProbabilityTheory.map_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  MeasureTheory.Measure.map
      (ProbabilityTheory.replacementOriginal
        i)
      (ProbabilityTheory.bentkusReplacementMeasure
        μ X) =
    MeasureTheory.Measure.map (X i) μ

The original coordinate on the enlarged space has its original marginal law.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.map_replacementGaussian.{u_1} {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  MeasureTheory.Measure.map (ProbabilityTheory.replacementGaussian i)
      (ProbabilityTheory.bentkusReplacementMeasure μ X) =
    ProbabilityTheory.multivariateGaussian 0
      (ProbabilityTheory.summandCovarianceMatrix μ X i)

theorem ProbabilityTheory.map_replacementGaussian.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  MeasureTheory.Measure.map
      (ProbabilityTheory.replacementGaussian
        i)
      (ProbabilityTheory.bentkusReplacementMeasure
        μ X) =
    ProbabilityTheory.multivariateGaussian
      0
      (ProbabilityTheory.summandCovarianceMatrix
        μ X i)

The Gaussian coordinate on the enlarged space has the prescribed companion law.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.measurePreserving_replacementOriginal.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  MeasureTheory.MeasurePreserving
    (ProbabilityTheory.replacementOriginal i)
    (ProbabilityTheory.bentkusReplacementMeasure μ X)
    (MeasureTheory.Measure.map (X i) μ)

theorem ProbabilityTheory.measurePreserving_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  MeasureTheory.MeasurePreserving
    (ProbabilityTheory.replacementOriginal
      i)
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)
    (MeasureTheory.Measure.map (X i) μ)

The original replacement coordinate is measure-preserving onto its original marginal law.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.measurePreserving_replacementGaussian.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  MeasureTheory.MeasurePreserving
    (ProbabilityTheory.replacementGaussian i)
    (ProbabilityTheory.bentkusReplacementMeasure μ X)
    (ProbabilityTheory.multivariateGaussian 0
      (ProbabilityTheory.summandCovarianceMatrix μ X i))

theorem ProbabilityTheory.measurePreserving_replacementGaussian.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  MeasureTheory.MeasurePreserving
    (ProbabilityTheory.replacementGaussian
      i)
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)
    (ProbabilityTheory.multivariateGaussian
      0
      (ProbabilityTheory.summandCovarianceMatrix
        μ X i))

The Gaussian replacement coordinate is measure-preserving onto its prescribed Gaussian law.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.memLp_replacementOriginal.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) {p : ENNReal}
  (hp : ∀ (i : Fin n), MeasureTheory.MemLp (X i) p μ) (i : Fin n) :
  MeasureTheory.MemLp (ProbabilityTheory.replacementOriginal i) p
    (ProbabilityTheory.bentkusReplacementMeasure μ X)

theorem ProbabilityTheory.memLp_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  {p : ENNReal}
  (hp :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) p μ)
  (i : Fin n) :
  MeasureTheory.MemLp
    (ProbabilityTheory.replacementOriginal
      i)
    p
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)

Moments of each original summand are preserved on the canonical replacement space.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.memLp_three_replacementGaussian.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  MeasureTheory.MemLp (ProbabilityTheory.replacementGaussian i) 3
    (ProbabilityTheory.bentkusReplacementMeasure μ X)

theorem ProbabilityTheory.memLp_three_replacementGaussian.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  MeasureTheory.MemLp
    (ProbabilityTheory.replacementGaussian
      i)
    3
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)

Gaussian replacement coordinates have finite third moments.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.integral_replacementOriginal_eq.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ProbabilityTheory.replacementOriginal i
        ω ∂ProbabilityTheory.bentkusReplacementMeasure μ X =
    ∫ (ω : Ω), X i ω ∂μ

theorem ProbabilityTheory.integral_replacementOriginal_eq.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ProbabilityTheory.replacementOriginal
        i
        ω ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X =
    ∫ (ω : Ω), X i ω ∂μ

The enlarged original coordinate has the same Bochner mean as the original summand.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.integral_replacementGaussian_eq_zero.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ProbabilityTheory.replacementGaussian i
        ω ∂ProbabilityTheory.bentkusReplacementMeasure μ X =
    0

theorem ProbabilityTheory.integral_replacementGaussian_eq_zero.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ProbabilityTheory.replacementGaussian
        i
        ω ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X =
    0

Every Gaussian coordinate remains centered on the enlarged replacement space.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.covarianceBilin_replacementGaussian_eq_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) (i : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.replacementGaussian i)
            (ProbabilityTheory.bentkusReplacementMeasure μ X)))
        x)
      y =
    ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.replacementOriginal i)
            (ProbabilityTheory.bentkusReplacementMeasure μ X)))
        x)
      y

theorem ProbabilityTheory.covarianceBilin_replacementGaussian_eq_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i))
  (i : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.replacementGaussian
              i)
            (ProbabilityTheory.bentkusReplacementMeasure
              μ X)))
        x)
      y =
    ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.replacementOriginal
              i)
            (ProbabilityTheory.bentkusReplacementMeasure
              μ X)))
        x)
      y

Original and Gaussian replacement coordinates have identical covariance bilinear forms.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.iIndepFun_replacementOriginal.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.iIndepFun
    (fun i => ProbabilityTheory.replacementOriginal i)
    (ProbabilityTheory.bentkusReplacementMeasure μ X)

theorem ProbabilityTheory.iIndepFun_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.iIndepFun
    (fun i =>
      ProbabilityTheory.replacementOriginal
        i)
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)

The canonical original coordinates remain mutually independent on the enlarged replacement
space.

theoremdefined in ProbabilityApproximation/Bentkus/ProbabilitySpaceTransport.lean

complete

theorem ProbabilityTheory.iIndepFun_replacementGaussian.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.iIndepFun
    (fun i => ProbabilityTheory.replacementGaussian i)
    (ProbabilityTheory.bentkusReplacementMeasure μ X)

theorem ProbabilityTheory.iIndepFun_replacementGaussian.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), Measurable (X i)) :
  ProbabilityTheory.iIndepFun
    (fun i =>
      ProbabilityTheory.replacementGaussian
        i)
    (ProbabilityTheory.bentkusReplacementMeasure
      μ X)

The Gaussian coordinates remain mutually independent on the enlarged replacement space.

This is the canonical-space realization of the Gaussian companions Y_i, the leave-one-out variables in equation (3.2), and the joint enlargement implicit in the telescoping/rotation setup (3.2)--(3.5) of Bentkus (2004), printed pp. 403--404. The source simply assumes all variables exist independently in the aggregate; the formal statement constructs the required marginal and Gaussian product spaces and allows singular individual covariance matrices. It deliberately stops before the rotation identity (3.4), which is recorded in the rotation nodes below.

Lemma2.2.2

uses 0used by 1✓L∃∀N

Tagsbentkusgaussian-replacementmomentssource-bentkus-2004fidelity-explicit-sufficient-bound

Dimension-free fourth-moment control for a Gaussian vector. Let S be a positive semidefinite d\times d real matrix and let Y\sim N(0,S). Then \mathbb E\|Y\|^4\le 3\bigl(\mathbb E\|Y\|^2\bigr)^2. No nonsingularity assumption is imposed on S.

Lean code for Lemma2.2.2●1 theorem

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanionMoments.lean

complete

theorem ProbabilityTheory.integral_norm_pow_four_multivariateGaussian_le {d : ℕ}
  {S : Matrix (Fin d) (Fin d) ℝ} (hS : S.PosSemidef) :
  ∫ (x : EuclideanSpace ℝ (Fin d)),
      ‖x‖ ^ 4 ∂ProbabilityTheory.multivariateGaussian 0 S ≤
    3 *
      (∫ (x : EuclideanSpace ℝ (Fin d)),
          ‖x‖ ^ 2 ∂ProbabilityTheory.multivariateGaussian 0 S) ^
        2

theorem ProbabilityTheory.integral_norm_pow_four_multivariateGaussian_le
  {d : ℕ} {S : Matrix (Fin d) (Fin d) ℝ}
  (hS : S.PosSemidef) :
  ∫ (x : EuclideanSpace ℝ (Fin d)),
      ‖x‖ ^
        4 ∂ProbabilityTheory.multivariateGaussian
        0 S ≤
    3 *
      (∫ (x : EuclideanSpace ℝ (Fin d)),
          ‖x‖ ^
            2 ∂ProbabilityTheory.multivariateGaussian
            0 S) ^
        2

The Gaussian fourth norm moment is at most three times the square of its second moment.

This is an explicit sufficient estimate for the dimension-free Gaussian moment comparison used by Bentkus (2004), in the discussion following equation (3.35), printed p. 408. Bentkus records the resulting third-moment comparison with an implicit absolute constant; the displayed fourth-moment bound is the formal route used to make that constant explicit.

Lemma2.2.3

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.2.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkusgaussian-replacementmomentssource-bentkus-2004fidelity-exact

Exact second-moment matching on the replacement space. Let X_i be measurable, centered, square-integrable random vectors in \mathbb R^d. On the canonical replacement space, let \widetilde X_i have the law of X_i and let Y_i\sim N(0,\operatorname{Cov}(X_i)) be its independent Gaussian companion. Then \mathbb E\|Y_i\|^2=\mathbb E\|\widetilde X_i\|^2. The covariance, and hence the Gaussian law, may be singular.

Lean code for Lemma2.2.3●1 theorem

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanionMoments.lean

complete

theorem ProbabilityTheory.integral_norm_sq_replacementGaussian_eq_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX2 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 2 μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementGaussian i ω‖ ^
        2 ∂ProbabilityTheory.bentkusReplacementMeasure μ X =
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementOriginal i ω‖ ^
        2 ∂ProbabilityTheory.bentkusReplacementMeasure μ X

theorem ProbabilityTheory.integral_norm_sq_replacementGaussian_eq_replacementOriginal.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX2 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 2 μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementGaussian
            i ω‖ ^
        2 ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X =
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementOriginal
            i ω‖ ^
        2 ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X

Exact second-norm-moment matching for one original coordinate and its Gaussian companion on
the canonical replacement space.

This is the norm-moment consequence of the covariance matching used by Bentkus (2004), immediately after equation (3.35), printed p. 408, where the equality \mathbb E\lvert Y\rvert^2= \mathbb E\lvert X\rvert^2 is invoked explicitly.

Theorem2.2.4

Statement uses 2

Statement dependency previews

Preview

Lemma 2.2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkusgaussian-replacementmomentssource-bentkus-2004fidelity-explicit-absolute-constant

Third-moment comparison for a covariance-matched Gaussian. Let X be a centered L^3 random vector in \mathbb R^d, and let Y\sim N(0,\operatorname{Cov}(X)). With the absolute constant C_G=27, one has \mathbb E\|Y\|^3\le C_G\,\mathbb E\|X\|^3. Equivalently, for each coordinate pair (\widetilde X_i,Y_i) on the canonical replacement space, \mathbb E\|Y_i\|^3\le 27\,\mathbb E\|\widetilde X_i\|^3.

Lean code for Theorem2.2.4●3 declarations

defdefined in ProbabilityApproximation/Bentkus/GaussianCompanionMoments.lean

complete

def ProbabilityTheory.gaussianCompanionThirdMomentConstant : ℝ

def ProbabilityTheory.gaussianCompanionThirdMomentConstant :
  ℝ

The explicit absolute constant used for the Gaussian-companion third-moment comparison.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanionMoments.lean

complete

theorem ProbabilityTheory.integral_norm_pow_three_multivariateGaussian_covarianceMatrix_le.{u_1}
  {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → EuclideanSpace ℝ (Fin d)} (hX3 : MeasureTheory.MemLp X 3 μ)
  (hX0 : ∫ (ω : Ω), X ω ∂μ = 0) :
  ∫ (y : EuclideanSpace ℝ (Fin d)),
      ‖y‖ ^
        3 ∂ProbabilityTheory.multivariateGaussian 0
        (ProbabilityTheory.covarianceMatrix
          (MeasureTheory.Measure.map X μ)) ≤
    ProbabilityTheory.gaussianCompanionThirdMomentConstant *
      ∫ (ω : Ω), ‖X ω‖ ^ 3 ∂μ

theorem ProbabilityTheory.integral_norm_pow_three_multivariateGaussian_covarianceMatrix_le.{u_1}
  {d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : MeasureTheory.MemLp X 3 μ)
  (hX0 : ∫ (ω : Ω), X ω ∂μ = 0) :
  ∫ (y : EuclideanSpace ℝ (Fin d)),
      ‖y‖ ^
        3 ∂ProbabilityTheory.multivariateGaussian
        0
        (ProbabilityTheory.covarianceMatrix
          (MeasureTheory.Measure.map X
            μ)) ≤
    ProbabilityTheory.gaussianCompanionThirdMomentConstant *
      ∫ (ω : Ω), ‖X ω‖ ^ 3 ∂μ

A centered Gaussian with the covariance of `X` has a dimension-free third norm moment bounded
by an absolute multiple of the third norm moment of `X`.  The covariance may be singular.

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanionMoments.lean

complete

theorem ProbabilityTheory.integral_norm_pow_three_replacementGaussian_le.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementGaussian i ω‖ ^
        3 ∂ProbabilityTheory.bentkusReplacementMeasure μ X ≤
    ProbabilityTheory.gaussianCompanionThirdMomentConstant *
      ∫ (ω :
        (Fin n → EuclideanSpace ℝ (Fin d)) ×
          (Fin n → EuclideanSpace ℝ (Fin d))),
        ‖ProbabilityTheory.replacementOriginal i ω‖ ^
          3 ∂ProbabilityTheory.bentkusReplacementMeasure μ X

theorem ProbabilityTheory.integral_norm_pow_three_replacementGaussian_le.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementGaussian
            i ω‖ ^
        3 ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X ≤
    ProbabilityTheory.gaussianCompanionThirdMomentConstant *
      ∫ (ω :
        (Fin n →
            EuclideanSpace ℝ (Fin d)) ×
          (Fin n →
            EuclideanSpace ℝ (Fin d))),
        ‖ProbabilityTheory.replacementOriginal
              i ω‖ ^
          3 ∂ProbabilityTheory.bentkusReplacementMeasure
          μ X

Bentkus's dimension-free Gaussian-companion comparison, realized on the canonical replacement
space.  This is the explicit-constant form of the `E ‖Y‖³ ≪ E ‖X‖³` estimate used on p. 408
after equation (3.35).

Bentkus (2004), uses \mathbb E\lvert Y\rvert^3\ll\mathbb E\lvert X\rvert^3 after equation (3.35), printed p. 408, and reuses the same absolute-moment control in equations (3.39)--(3.40), printed p. 409. The formal statement replaces the source's implicit constant by the conservative explicit value 27.

Lemma2.2.5

Statement uses 2

Statement dependency previews

Preview

Theorem 2.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkusgaussian-replacementmomentssource-bentkus-2004fidelity-explicit-holder-bound

Mixed original--Gaussian moment bound. Under the preceding centered L^3 hypotheses, the independent canonical pair (\widetilde X_i,Y_i) satisfies \mathbb E\bigl[\|\widetilde X_i\|^2\|Y_i\|\bigr] \le \mathbb E\|\widetilde X_i\|^3.

Lean code for Lemma2.2.5●1 theorem

theoremdefined in ProbabilityApproximation/Bentkus/GaussianCompanionMoments.lean

complete

theorem ProbabilityTheory.integral_norm_sq_replacementOriginal_mul_norm_replacementGaussian_le.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementOriginal i ω‖ ^ 2 *
        ‖ProbabilityTheory.replacementGaussian i
            ω‖ ∂ProbabilityTheory.bentkusReplacementMeasure μ X ≤
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementOriginal i ω‖ ^
        3 ∂ProbabilityTheory.bentkusReplacementMeasure μ X

theorem ProbabilityTheory.integral_norm_sq_replacementOriginal_mul_norm_replacementGaussian_le.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (i : Fin n) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementOriginal
              i ω‖ ^
          2 *
        ‖ProbabilityTheory.replacementGaussian
            i
            ω‖ ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X ≤
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ‖ProbabilityTheory.replacementOriginal
            i ω‖ ^
        3 ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X

The mixed Hölder estimate used immediately before Bentkus (3.30), on the canonical
replacement space: `E (‖X‖² ‖Y‖) ≤ E ‖X‖³`.

This is the Hölder estimate used immediately before equation (3.30) in Vidmantas Bentkus (2004), printed p. 407. The source writes the estimate with X and its covariance-matched Gaussian Y; the formal statement records it on the canonical independent replacement space.

Theorem2.2.6

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.2.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkusgaussian-replacementrotationsource-bentkus-2004fidelity-low-order-cancellation

Rotation and low-order moment cancellation. Let X,Y be independent random vectors in a real Banach space E, assume that they are integrable and centered, and let B:E\times E\to\mathbb R be a continuous bilinear form for which B(X,X) and B(Y,Y) are integrable. If \mathbb E B(X,X)=\mathbb E B(Y,Y), then, for every \alpha\in\mathbb R, the rotation and its angular derivative X_\alpha=\cos\alpha\,X+\sin\alpha\,Y,\qquad X'_\alpha=-\sin\alpha\,X+\cos\alpha\,Y are centered and satisfy the quadratic cancellation \mathbb E B(X_\alpha,X'_\alpha)=0. Pointwise, the bilinear term expands as B(X_\alpha,X'_\alpha) =-\cos\alpha\sin\alpha\,B(X,X) +\cos^2\alpha\,B(X,Y) -\sin^2\alpha\,B(Y,X) +\sin\alpha\cos\alpha\,B(Y,Y). In particular, for every centered measurable L^3 summand X_i, the canonical pair consisting of its marginal-law coordinate and its covariance-matched Gaussian companion satisfies this cancellation for every continuous bilinear B.

Lean code for Theorem2.2.6●7 declarations

defdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

def ProbabilityTheory.bentkusRotated.{u_1, u_2} {Ω : Type u_1}
  {E : Type u_2} [AddCommMonoid E] [Module ℝ E] (α : ℝ) (X Y : Ω → E) :
  Ω → E

def ProbabilityTheory.bentkusRotated.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [AddCommMonoid E] [Module ℝ E] (α : ℝ)
  (X Y : Ω → E) : Ω → E

Rotation from a summand toward its matched Gaussian companion.

defdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

def ProbabilityTheory.bentkusRotatedDeriv.{u_1, u_2} {Ω : Type u_1}
  {E : Type u_2} [AddCommGroup E] [Module ℝ E] (α : ℝ) (X Y : Ω → E) :
  Ω → E

def ProbabilityTheory.bentkusRotatedDeriv.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [AddCommGroup E] [Module ℝ E] (α : ℝ)
  (X Y : Ω → E) : Ω → E

Angular derivative of `bentkusRotated`.

theoremdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

theorem ProbabilityTheory.integral_bentkusRotated_eq_zero.{u_1, u_2}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure Ω}
  {X Y : Ω → E} (hX : MeasureTheory.Integrable X μ)
  (hY : MeasureTheory.Integrable Y μ) (hX0 : ∫ (ω : Ω), X ω ∂μ = 0)
  (hY0 : ∫ (ω : Ω), Y ω ∂μ = 0) (α : ℝ) :
  ∫ (ω : Ω), ProbabilityTheory.bentkusRotated α X Y ω ∂μ = 0

theorem ProbabilityTheory.integral_bentkusRotated_eq_zero.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  {μ : MeasureTheory.Measure Ω}
  {X Y : Ω → E}
  (hX : MeasureTheory.Integrable X μ)
  (hY : MeasureTheory.Integrable Y μ)
  (hX0 : ∫ (ω : Ω), X ω ∂μ = 0)
  (hY0 : ∫ (ω : Ω), Y ω ∂μ = 0) (α : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.bentkusRotated α X
        Y ω ∂μ =
    0

The rotation of two centered integrable vectors is centered.

theoremdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

theorem ProbabilityTheory.integral_bentkusRotatedDeriv_eq_zero.{u_1, u_2}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure Ω}
  {X Y : Ω → E} (hX : MeasureTheory.Integrable X μ)
  (hY : MeasureTheory.Integrable Y μ) (hX0 : ∫ (ω : Ω), X ω ∂μ = 0)
  (hY0 : ∫ (ω : Ω), Y ω ∂μ = 0) (α : ℝ) :
  ∫ (ω : Ω), ProbabilityTheory.bentkusRotatedDeriv α X Y ω ∂μ = 0

theorem ProbabilityTheory.integral_bentkusRotatedDeriv_eq_zero.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  {μ : MeasureTheory.Measure Ω}
  {X Y : Ω → E}
  (hX : MeasureTheory.Integrable X μ)
  (hY : MeasureTheory.Integrable Y μ)
  (hX0 : ∫ (ω : Ω), X ω ∂μ = 0)
  (hY0 : ∫ (ω : Ω), Y ω ∂μ = 0) (α : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.bentkusRotatedDeriv
        α X Y ω ∂μ =
    0

The angular derivative of the rotation of two centered integrable vectors is centered.

theoremdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

theorem ProbabilityTheory.bentkusRotated_bilin_bentkusRotatedDeriv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (B : E →L[ℝ] E →L[ℝ] ℝ) (α : ℝ) (x y : E) :
  (B (Real.cos α • x + Real.sin α • y))
      (-Real.sin α • x + Real.cos α • y) =
    -(Real.cos α * Real.sin α) * (B x) x + Real.cos α ^ 2 * (B x) y -
        Real.sin α ^ 2 * (B y) x +
      Real.sin α * Real.cos α * (B y) y

theorem ProbabilityTheory.bentkusRotated_bilin_bentkusRotatedDeriv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  (B : E →L[ℝ] E →L[ℝ] ℝ) (α : ℝ)
  (x y : E) :
  (B (Real.cos α • x + Real.sin α • y))
      (-Real.sin α • x + Real.cos α • y) =
    -(Real.cos α * Real.sin α) * (B x) x +
          Real.cos α ^ 2 * (B x) y -
        Real.sin α ^ 2 * (B y) x +
      Real.sin α * Real.cos α * (B y) y

Pointwise bilinear expansion underlying the quadratic cancellation in Bentkus (3.5).

theoremdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

theorem ProbabilityTheory.integral_bilin_bentkusRotated_bentkusRotatedDeriv_eq_zero.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure Ω}
  {X Y : Ω → E} (hXY : ProbabilityTheory.IndepFun X Y μ)
  (hX : MeasureTheory.Integrable X μ)
  (hY : MeasureTheory.Integrable Y μ) (hX0 : ∫ (ω : Ω), X ω ∂μ = 0)
  (hY0 : ∫ (ω : Ω), Y ω ∂μ = 0) (B : E →L[ℝ] E →L[ℝ] ℝ)
  (hXX : MeasureTheory.Integrable (fun ω => (B (X ω)) (X ω)) μ)
  (hYY : MeasureTheory.Integrable (fun ω => (B (Y ω)) (Y ω)) μ)
  (hmatch :
    ∫ (ω : Ω), (B (X ω)) (X ω) ∂μ = ∫ (ω : Ω), (B (Y ω)) (Y ω) ∂μ)
  (α : ℝ) :
  ∫ (ω : Ω),
      (B (ProbabilityTheory.bentkusRotated α X Y ω))
        (ProbabilityTheory.bentkusRotatedDeriv α X Y ω) ∂μ =
    0

theorem ProbabilityTheory.integral_bilin_bentkusRotated_bentkusRotatedDeriv_eq_zero.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSpace E]
  [BorelSpace E]
  {μ : MeasureTheory.Measure Ω}
  {X Y : Ω → E}
  (hXY : ProbabilityTheory.IndepFun X Y μ)
  (hX : MeasureTheory.Integrable X μ)
  (hY : MeasureTheory.Integrable Y μ)
  (hX0 : ∫ (ω : Ω), X ω ∂μ = 0)
  (hY0 : ∫ (ω : Ω), Y ω ∂μ = 0)
  (B : E →L[ℝ] E →L[ℝ] ℝ)
  (hXX :
    MeasureTheory.Integrable
      (fun ω => (B (X ω)) (X ω)) μ)
  (hYY :
    MeasureTheory.Integrable
      (fun ω => (B (Y ω)) (Y ω)) μ)
  (hmatch :
    ∫ (ω : Ω), (B (X ω)) (X ω) ∂μ =
      ∫ (ω : Ω), (B (Y ω)) (Y ω) ∂μ)
  (α : ℝ) :
  ∫ (ω : Ω),
      (B
          (ProbabilityTheory.bentkusRotated
            α X Y ω))
        (ProbabilityTheory.bentkusRotatedDeriv
          α X Y ω) ∂μ =
    0

Bentkus (2004), equation (3.5), in its expected-bilinear form.  Independence kills the two
cross terms, while equality of the two self moments kills the remaining pair.

theoremdefined in ProbabilityApproximation/Bentkus/Rotation.lean

complete

theorem ProbabilityTheory.integral_bilin_replacementRotated_replacementRotatedDeriv_eq_zero.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (i : Fin n)
  (B : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)
  (α : ℝ) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      (B
          (ProbabilityTheory.bentkusRotated α
            (ProbabilityTheory.replacementOriginal i)
            (ProbabilityTheory.replacementGaussian i) ω))
        (ProbabilityTheory.bentkusRotatedDeriv α
          (ProbabilityTheory.replacementOriginal i)
          (ProbabilityTheory.replacementGaussian i)
          ω) ∂ProbabilityTheory.bentkusReplacementMeasure μ X =
    0

theorem ProbabilityTheory.integral_bilin_replacementRotated_replacementRotatedDeriv_eq_zero.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (i : Fin n)
  (B :
    EuclideanSpace ℝ (Fin d) →L[ℝ]
      EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)
  (α : ℝ) :
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      (B
          (ProbabilityTheory.bentkusRotated
            α
            (ProbabilityTheory.replacementOriginal
              i)
            (ProbabilityTheory.replacementGaussian
              i)
            ω))
        (ProbabilityTheory.bentkusRotatedDeriv
          α
          (ProbabilityTheory.replacementOriginal
            i)
          (ProbabilityTheory.replacementGaussian
            i)
          ω) ∂ProbabilityTheory.bentkusReplacementMeasure
        μ X =
    0

Bentkus (2004), equation (3.5), realized on the canonical replacement space for one original
summand and its covariance-matched Gaussian companion.  The hypotheses use measurable
representatives; the final setwise theorem transports arbitrary `MemLp` representatives to this
canonical form.

This is the low-order rotation layer introduced immediately before equation (3.4) in Bentkus (2004), and the linear/bilinear cancellation asserted in equation (3.5), printed p. 404. Independence kills the two mixed expectations and the matched second moment kills the remaining pair. The full telescoping identity (3.4) and its third-order remainder estimates are assembled in the rotation and standardized-induction nodes below.

Theorem2.2.7

Statement uses 4

Statement dependency previews

Preview

Theorem 2.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkusgaussian-replacementrotationfubinisource-bentkus-2004fidelity-explicit-integrability

Coordinate rotation integrands and justified exchange of expectations. On the canonical replacement space (\widetilde X_i,Y_i)_{i\in I}, put Z_\alpha=\sum_i(\cos\alpha\,\widetilde X_i+\sin\alpha\,Y_i), \qquad Z'_{k,\alpha}=-\sin\alpha\,\widetilde X_k+\cos\alpha\,Y_k, and let V_k=\sum_{i\ne k}Y_i. For a convex set A\subseteq\mathbb R^d, \varepsilon>0, and the Bentkus cutoff \varphi=\varphi_{\varepsilon,A}, define T_k(\alpha)=D\varphi(Z_\alpha)[Z'_{k,\alpha}], \qquad R_k(\alpha)=D\varphi\!\left(V_k+\cos\alpha\,\widetilde X_k+ \sin\alpha\,Y_k\right)[Z'_{k,\alpha}]. The rotated sum splits pointwise into its leave-one-out base and exposed coordinate: Z_\alpha= \cos\alpha\sum_{i\ne k}\widetilde X_i+ \sin\alpha\sum_{i\ne k}Y_i+ \cos\alpha\,\widetilde X_k+ \sin\alpha\,Y_k. If the original coordinates are measurable and belong to L^3, then on every bounded angle interval both coordinate integrands are jointly integrable with respect to angle and the replacement law. Consequently, \int_a^b\mathbb E T_k(\alpha)\,d\alpha =\mathbb E\int_a^bT_k(\alpha)\,d\alpha, \qquad \int_a^b\mathbb E R_k(\alpha)\,d\alpha =\mathbb E\int_a^bR_k(\alpha)\,d\alpha. If a\le b, finite summation may also be interchanged: \mathbb E\left[\sum_k\int_a^bT_k(\alpha)\,d\alpha\right] =\sum_k\int_a^b\mathbb E T_k(\alpha)\,d\alpha.

Lean code for Theorem2.2.7●10 declarations

defdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

def ProbabilityTheory.bentkusRotationCoordinateIntegrand {n d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ) (k : Fin n) (α : ℝ)
  (ω :
    (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d))) :
  ℝ

def ProbabilityTheory.bentkusRotationCoordinateIntegrand
  {n d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) (k : Fin n) (α : ℝ)
  (ω :
    (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n →
        EuclideanSpace ℝ (Fin d))) :
  ℝ

The coordinate contribution of the actual replacement rotation.

defdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

def ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand {n d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d))) (ε : ℝ) (k : Fin n) (α : ℝ)
  (ω :
    (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n → EuclideanSpace ℝ (Fin d))) :
  ℝ

def ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
  {n d : ℕ}
  (s : Set (EuclideanSpace ℝ (Fin d)))
  (ε : ℝ) (k : Fin n) (α : ℝ)
  (ω :
    (Fin n → EuclideanSpace ℝ (Fin d)) ×
      (Fin n →
        EuclideanSpace ℝ (Fin d))) :
  ℝ

The coordinate contribution with a fully Gaussian leave-one-out base.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.bentkusRotatedSum_eq_leaveOneOut_add.{u_1} {n d : ℕ}
  {Ω : Type u_1} (α : ℝ) (X Y : Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (k : Fin n) (ω : Ω) :
  ProbabilityTheory.bentkusRotatedSum α X Y ω =
    Real.cos α • ProbabilityTheory.bentkusLeaveOneOut X k ω +
        Real.sin α • ProbabilityTheory.bentkusLeaveOneOut Y k ω +
      ProbabilityTheory.bentkusRotated α (X k) (Y k) ω

theorem ProbabilityTheory.bentkusRotatedSum_eq_leaveOneOut_add.{u_1}
  {n d : ℕ} {Ω : Type u_1} (α : ℝ)
  (X Y :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (k : Fin n) (ω : Ω) :
  ProbabilityTheory.bentkusRotatedSum α X
      Y ω =
    Real.cos α •
          ProbabilityTheory.bentkusLeaveOneOut
            X k ω +
        Real.sin α •
          ProbabilityTheory.bentkusLeaveOneOut
            Y k ω +
      ProbabilityTheory.bentkusRotated α
        (X k) (Y k) ω

Splitting the rotated full sum at one coordinate gives the rotated leave-one-out base plus
the exposed coordinate.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.integrable_bentkusCoordinateIntegrands.{u} {n d : ℕ}
  {Ω : Type u} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (a b : ℝ) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  MeasureTheory.Integrable
      (Function.uncurry
        (ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k))
      ((MeasureTheory.volume.restrict (Set.uIoc a b)).prod ρ) ∧
    MeasureTheory.Integrable
      (Function.uncurry
        (ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand s
          ε k))
      ((MeasureTheory.volume.restrict (Set.uIoc a b)).prod ρ)

theorem ProbabilityTheory.integrable_bentkusCoordinateIntegrands.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) (a b : ℝ) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  MeasureTheory.Integrable
      (Function.uncurry
        (ProbabilityTheory.bentkusRotationCoordinateIntegrand
          s ε k))
      ((MeasureTheory.volume.restrict
            (Set.uIoc a b)).prod
        ρ) ∧
    MeasureTheory.Integrable
      (Function.uncurry
        (ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
          s ε k))
      ((MeasureTheory.volume.restrict
            (Set.uIoc a b)).prod
        ρ)

Both coordinate integrands are integrable over a bounded angle interval times the canonical
replacement probability space.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.intervalIntegrable_integral_bentkusCoordinateIntegrands.{u}
  {n d : ℕ} {Ω : Type u} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (a b : ℝ) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  IntervalIntegrable
      (fun α =>
        ∫ (ω :
          (Fin n → EuclideanSpace ℝ (Fin d)) ×
            (Fin n → EuclideanSpace ℝ (Fin d))),
          ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k α
            ω ∂ρ)
      MeasureTheory.volume a b ∧
    IntervalIntegrable
      (fun α =>
        ∫ (ω :
          (Fin n → EuclideanSpace ℝ (Fin d)) ×
            (Fin n → EuclideanSpace ℝ (Fin d))),
          ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
            s ε k α ω ∂ρ)
      MeasureTheory.volume a b

theorem ProbabilityTheory.intervalIntegrable_integral_bentkusCoordinateIntegrands.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) (a b : ℝ) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  IntervalIntegrable
      (fun α =>
        ∫ (ω :
          (Fin n →
              EuclideanSpace ℝ (Fin d)) ×
            (Fin n →
              EuclideanSpace ℝ (Fin d))),
          ProbabilityTheory.bentkusRotationCoordinateIntegrand
            s ε k α ω ∂ρ)
      MeasureTheory.volume a b ∧
    IntervalIntegrable
      (fun α =>
        ∫ (ω :
          (Fin n →
              EuclideanSpace ℝ (Fin d)) ×
            (Fin n →
              EuclideanSpace ℝ (Fin d))),
          ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
            s ε k α ω ∂ρ)
      MeasureTheory.volume a b

The expected actual and Gaussian-reference coordinate contributions are interval integrable
as functions of the rotation angle.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.integrable_intervalIntegral_bentkusRotationCoordinate.{u}
  {n d : ℕ} {Ω : Type u} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) {a b : ℝ} (hab : a ≤ b) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  MeasureTheory.Integrable
    (fun ω =>
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k α ω)
    ρ

theorem ProbabilityTheory.integrable_intervalIntegral_bentkusRotationCoordinate.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) {a b : ℝ} (hab : a ≤ b) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  MeasureTheory.Integrable
    (fun ω =>
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusRotationCoordinateIntegrand
          s ε k α ω)
    ρ

The interval-integrated actual coordinate is integrable on the replacement space.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.integrable_intervalIntegral_bentkusGaussianReferenceCoordinate.{u}
  {n d : ℕ} {Ω : Type u} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) {a b : ℝ} (hab : a ≤ b) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  MeasureTheory.Integrable
    (fun ω =>
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand s
          ε k α ω)
    ρ

theorem ProbabilityTheory.integrable_intervalIntegral_bentkusGaussianReferenceCoordinate.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) {a b : ℝ} (hab : a ≤ b) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  MeasureTheory.Integrable
    (fun ω =>
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
          s ε k α ω)
    ρ

The interval-integrated Gaussian-reference coordinate is integrable on the replacement
space.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.intervalIntegral_integral_bentkusRotationCoordinate_swap.{u}
  {n d : ℕ} {Ω : Type u} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (a b : ℝ) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  ∫ (α : ℝ) in a..b,
      ∫ (ω :
        (Fin n → EuclideanSpace ℝ (Fin d)) ×
          (Fin n → EuclideanSpace ℝ (Fin d))),
        ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k α
          ω ∂ρ =
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k α
          ω ∂ρ

theorem ProbabilityTheory.intervalIntegral_integral_bentkusRotationCoordinate_swap.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) (a b : ℝ) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  ∫ (α : ℝ) in a..b,
      ∫ (ω :
        (Fin n →
            EuclideanSpace ℝ (Fin d)) ×
          (Fin n →
            EuclideanSpace ℝ (Fin d))),
        ProbabilityTheory.bentkusRotationCoordinateIntegrand
          s ε k α ω ∂ρ =
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusRotationCoordinateIntegrand
          s ε k α ω ∂ρ

Fubini interchange for the actual coordinate contribution.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.intervalIntegral_integral_bentkusGaussianReferenceCoordinate_swap.{u}
  {n d : ℕ} {Ω : Type u} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) (a b : ℝ) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  ∫ (α : ℝ) in a..b,
      ∫ (ω :
        (Fin n → EuclideanSpace ℝ (Fin d)) ×
          (Fin n → EuclideanSpace ℝ (Fin d))),
        ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand s
          ε k α ω ∂ρ =
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand s
          ε k α ω ∂ρ

theorem ProbabilityTheory.intervalIntegral_integral_bentkusGaussianReferenceCoordinate_swap.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (k : Fin n)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) (a b : ℝ) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  ∫ (α : ℝ) in a..b,
      ∫ (ω :
        (Fin n →
            EuclideanSpace ℝ (Fin d)) ×
          (Fin n →
            EuclideanSpace ℝ (Fin d))),
        ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
          s ε k α ω ∂ρ =
    ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ∫ (α : ℝ) in a..b,
        ProbabilityTheory.bentkusGaussianReferenceCoordinateIntegrand
          s ε k α ω ∂ρ

Fubini interchange for the Gaussian-reference coordinate contribution.

theoremdefined in ProbabilityApproximation/Bentkus/RotationIntegration.lean

complete

theorem ProbabilityTheory.integral_sum_intervalIntegral_bentkusRotationCoordinate_eq.{u}
  {n d : ℕ} {Ω : Type u} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  {s : Set (EuclideanSpace ℝ (Fin d))} (hs : Convexity.IsConvexSet ℝ s)
  {ε : ℝ} (hε : 0 < ε) {a b : ℝ} (hab : a ≤ b) :
  have ρ := ProbabilityTheory.bentkusReplacementMeasure μ X;
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n → EuclideanSpace ℝ (Fin d))),
      ∑ k,
        ∫ (α : ℝ) in a..b,
          ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k α
            ω ∂ρ =
    ∑ k,
      ∫ (α : ℝ) in a..b,
        ∫ (ω :
          (Fin n → EuclideanSpace ℝ (Fin d)) ×
            (Fin n → EuclideanSpace ℝ (Fin d))),
          ProbabilityTheory.bentkusRotationCoordinateIntegrand s ε k α
            ω ∂ρ

theorem ProbabilityTheory.integral_sum_intervalIntegral_bentkusRotationCoordinate_eq.{u}
  {n d : ℕ} {Ω : Type u}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hXm : ∀ (i : Fin n), Measurable (X i))
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  {s : Set (EuclideanSpace ℝ (Fin d))}
  (hs : Convexity.IsConvexSet ℝ s) {ε : ℝ}
  (hε : 0 < ε) {a b : ℝ} (hab : a ≤ b) :
  have ρ :=
    ProbabilityTheory.bentkusReplacementMeasure
      μ X;
  ∫ (ω :
      (Fin n → EuclideanSpace ℝ (Fin d)) ×
        (Fin n →
          EuclideanSpace ℝ (Fin d))),
      ∑ k,
        ∫ (α : ℝ) in a..b,
          ProbabilityTheory.bentkusRotationCoordinateIntegrand
            s ε k α ω ∂ρ =
    ∑ k,
      ∫ (α : ℝ) in a..b,
        ∫ (ω :
          (Fin n →
              EuclideanSpace ℝ (Fin d)) ×
            (Fin n →
              EuclideanSpace ℝ (Fin d))),
          ProbabilityTheory.bentkusRotationCoordinateIntegrand
            s ε k α ω ∂ρ

The expected integral of the finite coordinate sum equals the sum of the expected
coordinate integrals, with the angle integral moved outside.

Bentkus (2004), introduces the uniform rotation and leave-one-out sums immediately before equation (3.4), printed pp. 403--404; equations (3.4)--(3.5), printed p. 404, give the coordinate representation and low-order cancellations. The actual and fully Gaussian reference contributions are the terms split in equations (3.11)--(3.12), also printed p. 404. The paper writes the angle expectations compactly; the formal statement makes their joint integrability and every Fubini interchange explicit.

Theorem2.2.8

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 2.2.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkuscovarianceleave-one-outsource-bentkus-2004fidelity-exact

Covariance additivity and the leave-one-out identity. Let X_1,\ldots,X_n be independent square-integrable random vectors in \mathbb R^d. For every set of indices J and every u,v\in\mathbb R^d, one has \operatorname{Cov}\!\left(\sum_{i\in J}X_i\right)[u,v] =\sum_{i\in J}\operatorname{Cov}(X_i)[u,v]. Writing W=\sum_iX_i,\qquad U_k=\sum_{i\ne k}X_i, it follows that \operatorname{Cov}(W) =\operatorname{Cov}(U_k)+\operatorname{Cov}(X_k). Consequently, if \operatorname{Cov}(W)=I_d, and if P_k^2 denotes the covariance matrix of U_k while \Sigma_k denotes that of X_k, then P_k^2=I_d-\Sigma_k. No individual covariance matrix is required to be nonsingular.

Lean code for Theorem2.2.8●7 declarations

theoremdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

theorem ProbabilityTheory.covarianceBilin_map_finsetSum_eq_sum.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {n d : ℕ}
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ) (s : Finset (Fin n))
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map (fun ω => ∑ i ∈ s, X i ω) μ))
        x)
      y =
    ∑ i ∈ s,
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map (X i) μ))
          x)
        y

theorem ProbabilityTheory.covarianceBilin_map_finsetSum_eq_sum.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {n d : ℕ}
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (s : Finset (Fin n))
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (fun ω => ∑ i ∈ s, X i ω) μ))
        x)
      y =
    ∑ i ∈ s,
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map
              (X i) μ))
          x)
        y

Covariance bilinear form of a subsum of an independent finite family.

theoremdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

theorem ProbabilityTheory.covarianceBilin_map_sum_eq_sum.{u_1} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {n d : ℕ}
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
        x)
      y =
    ∑ i,
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map (X i) μ))
          x)
        y

theorem ProbabilityTheory.covarianceBilin_map_sum_eq_sum.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {n d : ℕ}
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (fun ω => ∑ i, X i ω) μ))
        x)
      y =
    ∑ i,
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map
              (X i) μ))
          x)
        y

Covariance bilinear form of the full independent sum.

defdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

def ProbabilityTheory.bentkusLeaveOneOut.{u_1} {n d : ℕ} {Ω : Type u_1}
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (k : Fin n) :
  Ω → EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.bentkusLeaveOneOut.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (k : Fin n) :
  Ω → EuclideanSpace ℝ (Fin d)

Sum of all summands except the `k`th.  This is `Uₖ = S - Xₖ` in Bentkus (2004), (3.2).

theoremdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

theorem ProbabilityTheory.covarianceBilin_map_sum_eq_leaveOneOut_add.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {n d : ℕ}
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ) (k : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
        x)
      y =
    ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map
              (ProbabilityTheory.bentkusLeaveOneOut X k) μ))
          x)
        y +
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map (X k) μ))
          x)
        y

theorem ProbabilityTheory.covarianceBilin_map_sum_eq_leaveOneOut_add.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {n d : ℕ}
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (k : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (fun ω => ∑ i, X i ω) μ))
        x)
      y =
    ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map
              (ProbabilityTheory.bentkusLeaveOneOut
                X k)
              μ))
          x)
        y +
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map
              (X k) μ))
          x)
        y

Covariance of the full sum decomposes into leave-one-out covariance plus the omitted
summand's covariance.

defdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

def ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (k : Fin n) :
  Matrix (Fin d) (Fin d) ℝ

def ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (k : Fin n) : Matrix (Fin d) (Fin d) ℝ

Covariance matrix of the leave-one-out sum.

theoremdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

theorem ProbabilityTheory.covarianceBilin_leaveOneOut_eq_inner_sub.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {n d : ℕ}
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.bentkusLeaveOneOut X k) μ))
        x)
      y =
    inner ℝ x y -
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map (X k) μ))
          x)
        y

theorem ProbabilityTheory.covarianceBilin_leaveOneOut_eq_inner_sub.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {n d : ℕ}
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (ProbabilityTheory.bentkusLeaveOneOut
              X k)
            μ))
        x)
      y =
    inner ℝ x y -
      ((ProbabilityTheory.covarianceBilin
            (MeasureTheory.Measure.map
              (X k) μ))
          x)
        y

Under identity total covariance, leave-one-out covariance is identity covariance minus the
omitted summand covariance.  This is the matrix `Pₖ² = I - cov Xₖ` used after (3.2).

theoremdefined in ProbabilityApproximation/Bentkus/CovarianceAlgebra.lean

complete

theorem ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix_eq_one_sub.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {n d : ℕ}
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) :
  ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix μ X k =
    1 - ProbabilityTheory.summandCovarianceMatrix μ X k

theorem ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix_eq_one_sub.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {n d : ℕ}
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) :
  ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix
      μ X k =
    1 -
      ProbabilityTheory.summandCovarianceMatrix
        μ X k

Matrix form of `Pₖ² = I - cov Xₖ` from Bentkus (2004), page 403.

This is the covariance algebra in equation (3.2) and the paragraph immediately following it in Bentkus (2004), printed p. 403. The formal subsum identity is stated at the level of covariance bilinear forms; the last display is its coordinate-matrix form and is exactly the paper's P_k^2=I-\operatorname{cov}X_k notation.