EmpiricalCovariance: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

The empirical second moment is an average of rank-one operators
A self outer product has operator norm equal to the squared vector norm
Empirical covariance is reduced to bounded symmetric centered summands
A unit-vector covariance has an exact centered operator second moment

Samplinglib mathematical lesson

The empirical second moment is an average of rank-one operators

AutoSamplingTheory.TechnicalLemmas.Probability.EmpiricalCovariance.empiricalSecondMoment · def · Teaching coverage

Read this first

Mathematical statement

For a finite sample x_i in a real inner-product space, the empirical second-moment operator is the inverse sample size times the sum of y ↦ ⟪x_i,y⟫x_i. The empty-sample convention is zero; concentration consumers use a nonempty index type.

\[\widehat\Sigma=|I|^{-1}\sum_{i\in I}x_i\otimes x_i\]

Lean statement · empiricalSecondMoment

Lean keeps the real inner-product space, finite sample index, and empty-sample inverse-cardinality convention explicit.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

def empiricalSecondMoment (sample : κ → E) : E →L[ℝ] E

Exact module and namespace context

Proof roadmap

1Turn each vector into a rank-one operator
The Mathlib rank-one operator sends y to the inner product with x_i multiplied by x_i.
2Average the finite family
Sum the continuous linear maps and scale by the inverse real cardinality.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space and I is a finite type.
The sample is an arbitrary function I→E.
No probability law, independence, centering, or boundedness is assumed by the definition.

Construction and meaning

1. Turn each vector into a rank-one operator

The Mathlib rank-one operator sends y to the inner product with x_i multiplied by x_i.

\[(x_i\otimes x_i)y=\langle x_i,y\rangle x_i\]

Corresponding Lean step

Use InnerProductSpace.rankOne ℝ (sample i) (sample i).

2. Average the finite family

Sum the continuous linear maps and scale by the inverse real cardinality.

\[\widehat\Sigma=|I|^{-1}\sum_i x_i\otimes x_i\]

Corresponding Lean step

Continuous linear maps carry finite sums and real scalar multiplication.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · empiricalSecondMoment

This is a transparent definition; no theorem or probabilistic premise is hidden in it.

Download module (.lean)

def empiricalSecondMoment (sample : κ → E) : E →L[ℝ] E :=
  (Fintype.card κ : ℝ)⁻¹ •
    ∑ i, InnerProductSpace.rankOne ℝ (sample i) (sample i)

Exact module and namespace context

Scope and omitted-condition boundaries

This definition is an empirical second moment. Calling it a covariance requires an appropriate centering convention, supplied separately by the consumer.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

InnerProductSpace.rankOne
Fintype.card

Mathematical sources

Tropp, An Introduction to Matrix Concentration Inequalities — Standard rank-one sample-covariance setup used before matrix concentration.
Samplinglib compiled definition — Exact finite-type normalization and operator representation.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

A self outer product has operator norm equal to the squared vector norm

AutoSamplingTheory.TechnicalLemmas.Probability.EmpiricalCovariance.norm_rankOne_self_eq_sq · theorem · Teaching coverage

Read this first

Mathematical statement

For every vector x in a real inner-product space, the continuous rank-one operator y ↦ ⟪x,y⟫x has operator norm exactly ‖x‖².

\[\|x\otimes x\|_{\mathrm{op}}=\|x\|^2\]

Lean statement · norm_rankOne_self_eq_sq

The equality is stated directly for Mathlib's continuous rank-one operator.

Download module (.lean)

theorem norm_rankOne_self_eq_sq (x : E) :
    ‖InnerProductSpace.rankOne ℝ x x‖ = ‖x‖ ^ 2

Exact module and namespace context

Proof roadmap

1Use the rank-one norm identity
Mathlib computes the norm of u⊗v as ‖u‖‖v‖.
2Rewrite the product as a square
The identical norm factors are exactly ‖x‖².

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
x is arbitrary; finite dimensionality and completeness are not assumed.

Mathematical proof

1. Use the rank-one norm identity

Mathlib computes the norm of u⊗v as ‖u‖‖v‖.

\[\|x\otimes x\|=\|x\|\,\|x\|\]

Corresponding Lean step

Simplify InnerProductSpace.rankOne with its norm theorem.

2. Rewrite the product as a square

The identical norm factors are exactly ‖x‖².

\[\|x\|\,\|x\|=\|x\|^2\]

Corresponding Lean step

simp [pow_two] closes the equality.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · norm_rankOne_self_eq_sq

The proof uses the library norm formula and the definition of a square.

Download module (.lean)

theorem norm_rankOne_self_eq_sq (x : E) :
    ‖InnerProductSpace.rankOne ℝ x x‖ = ‖x‖ ^ 2 := by
  simp [pow_two]

Exact module and namespace context

Scope and omitted-condition boundaries

This is deterministic Hilbert-space operator algebra; it contains no concentration claim.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

InnerProductSpace.rankOne
ContinuousLinearMap.norm_rankOne

Mathematical sources

Tropp, matrix concentration monograph — Rank-one covariance summands in the standard empirical-covariance application.
Samplinglib compiled norm leaf — Exact operator-norm equality.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

Empirical covariance is reduced to bounded symmetric centered summands

AutoSamplingTheory.TechnicalLemmas.Probability.EmpiricalCovariance.empiricalSecondMoment_preconcentration · theorem · Teaching coverage

Read this first

Mathematical statement

For a nonempty finite sample with ‖x_i‖≤B, a symmetric population operator Σ with ‖Σ‖≤B², and B≥0, the empirical error is the average of x_i⊗x_i−Σ; every summand is symmetric and has operator norm at most 2B².

\[\widehat\Sigma-\Sigma=|I|^{-1}\sum_i(x_i\otimes x_i-\Sigma),\qquad (x_i\otimes x_i-\Sigma)^*=x_i\otimes x_i-\Sigma,\qquad \|x_i\otimes x_i-\Sigma\|\le2B^2\]

Lean statement · empiricalSecondMoment_preconcentration

All boundedness, symmetry, nonemptiness, and normalization assumptions are explicit, and the conclusion is a three-part conjunction.

Download module (.lean)

theorem empiricalSecondMoment_preconcentration
    [Nonempty κ]
    (population : E →L[ℝ] E) (sample : κ → E) (B : ℝ)
    (hB : 0 ≤ B)
    (hpopulationSymmetric : LinearMap.IsSymmetric (population : E →ₗ[ℝ] E))
    (hpopulationNorm : ‖population‖ ≤ B ^ 2)
    (hsampleNorm : ∀ i, ‖sample i‖ ≤ B) :
    (empiricalSecondMoment sample - population =
      (Fintype.card κ : ℝ)⁻¹ •
        ∑ i, (InnerProductSpace.rankOne ℝ (sample i) (sample i) - population)) ∧
    (∀ i, LinearMap.IsSymmetric
      ((InnerProductSpace.rankOne ℝ (sample i) (sample i) - population : E →L[ℝ] E) :
        E →ₗ[ℝ] E)) ∧
    (∀ i,
      ‖InnerProductSpace.rankOne ℝ (sample i) (sample i) - population‖ ≤
        2 * B ^ 2)

Exact module and namespace context

Proof roadmap

1Expand the centered finite sum
Distribute the finite sum over subtraction. Nonemptiness makes the sample cardinality nonzero, so inverse scaling cancels the repeated population term.
2Preserve symmetry under centering
Each x_i⊗x_i is symmetric, and the difference of symmetric operators is symmetric.
3Bound each centered summand
The triangle inequality, the exact rank-one norm, ‖x_i‖≤B, and ‖Σ‖≤B² yield the standard 2B² bound.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space and I is a nonempty finite type.
B is nonnegative and every sample vector has norm at most B.
The supplied population continuous linear operator is symmetric and has norm at most B².
No independence, expectation, variance proxy, tail theorem, or dimension bound is assumed.

Mathematical proof

1. Expand the centered finite sum

Distribute the finite sum over subtraction. Nonemptiness makes the sample cardinality nonzero, so inverse scaling cancels the repeated population term.

\[|I|^{-1}\sum_i(A_i-\Sigma)=|I|^{-1}\sum_iA_i-\Sigma\]

Corresponding Lean step

Use Finset.sum_sub_distrib, Finset.sum_const, and inv_smul_smul₀.

2. Preserve symmetry under centering

Each x_i⊗x_i is symmetric, and the difference of symmetric operators is symmetric.

\[(x_i\otimes x_i-\Sigma)^*=x_i\otimes x_i-\Sigma\]

Corresponding Lean step

Combine isSymmetric_rankOne_self with LinearMap.IsSymmetric.sub.

3. Bound each centered summand

The triangle inequality, the exact rank-one norm, ‖x_i‖≤B, and ‖Σ‖≤B² yield the standard 2B² bound.

\[\|x_i\otimes x_i-\Sigma\|\le\|x_i\|^2+\|\Sigma\|\le2B^2\]

Corresponding Lean step

Use norm_sub_le, norm_rankOne_self_eq_sq, monotonicity of squaring on nonnegative reals, and ring normalization.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · empiricalSecondMoment_preconcentration

The proof performs the exact finite-sum cancellation, transports symmetry through subtraction, and combines the triangle inequality with the exact rank-one norm.

Download module (.lean)

theorem empiricalSecondMoment_preconcentration
    [Nonempty κ]
    (population : E →L[ℝ] E) (sample : κ → E) (B : ℝ)
    (hB : 0 ≤ B)
    (hpopulationSymmetric : LinearMap.IsSymmetric (population : E →ₗ[ℝ] E))
    (hpopulationNorm : ‖population‖ ≤ B ^ 2)
    (hsampleNorm : ∀ i, ‖sample i‖ ≤ B) :
    (empiricalSecondMoment sample - population =
      (Fintype.card κ : ℝ)⁻¹ •
        ∑ i, (InnerProductSpace.rankOne ℝ (sample i) (sample i) - population)) ∧
    (∀ i, LinearMap.IsSymmetric
      ((InnerProductSpace.rankOne ℝ (sample i) (sample i) - population : E →L[ℝ] E) :
        E →ₗ[ℝ] E)) ∧
    (∀ i,
      ‖InnerProductSpace.rankOne ℝ (sample i) (sample i) - population‖ ≤
        2 * B ^ 2) := by
  have hcard : (Fintype.card κ : ℝ) ≠ 0 := by
    exact_mod_cast Fintype.card_ne_zero
  constructor
  · rw [Finset.sum_sub_distrib]
    unfold empiricalSecondMoment
    rw [smul_sub]
    congr 1
    rw [Finset.sum_const, ← Nat.cast_smul_eq_nsmul ℝ]
    exact (inv_smul_smul₀ hcard population).symm
  constructor
  · intro i
    exact (InnerProductSpace.isSymmetric_rankOne_self (sample i)).sub
      hpopulationSymmetric
  · intro i
    have hsample_sq : ‖sample i‖ ^ 2 ≤ B ^ 2 :=
      (sq_le_sq₀ (norm_nonneg (sample i)) hB).2 (hsampleNorm i)
    calc
      ‖InnerProductSpace.rankOne ℝ (sample i) (sample i) - population‖
          ≤ ‖InnerProductSpace.rankOne ℝ (sample i) (sample i)‖ + ‖population‖ :=
        norm_sub_le _ _
      _ = ‖sample i‖ ^ 2 + ‖population‖ := by
        rw [norm_rankOne_self_eq_sq]
      _ ≤ B ^ 2 + B ^ 2 := add_le_add hsample_sq hpopulationNorm
      _ = 2 * B ^ 2 := by ring

Exact module and namespace context

Scope and omitted-condition boundaries

This theorem prepares a matrix-concentration input. It does not prove matrix Bernstein, choose a variance proxy, establish independence, or derive a probability tail or sample complexity.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Finset.sum_sub_distrib
InnerProductSpace.isSymmetric_rankOne_self
LinearMap.IsSymmetric.sub
norm_sub_le
inv_smul_smul₀

Mathematical sources

Tropp, An Introduction to Matrix Concentration Inequalities — Matrix Bernstein setup and empirical-covariance applications; the Lean theorem isolates the deterministic preprocessing obligations.
Samplinglib compiled preconcentration theorem — Exact decomposition, symmetry, and uniform summand norm bound.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

A unit-vector covariance has an exact centered operator second moment

AutoSamplingTheory.TechnicalLemmas.Probability.EmpiricalCovariance.unitRankOneCovariance_momentPackage · theorem · Teaching coverage

Read this first

Mathematical statement

Let X be a unit-vector-valued map such that X⊗X is Bochner integrable, and let C be the Bochner expectation of X⊗X. Then C is self-adjoint, ‖C‖≤1, E[(X⊗X-C)²]=C-C², and ‖C-C²‖≤2‖C‖.

\[C=\mathbb E[X\otimes X],\quad C^*=C,\quad \|C\|\le1,\quad \mathbb E[(X\otimes X-C)^2]=C-C^2,\quad \|C-C^2\|\le2\|C\|\]

Lean statement · unitRankOneCovariance_momentPackage

The conclusion is a four-part conjunction and all probability, integrability, unit-norm, and population-identification assumptions occur explicitly in the signature.

Download module (.lean)

theorem unitRankOneCovariance_momentPackage
    [CompleteSpace E]
    {Omega : Type*} [MeasurableSpace Omega]
    {mu : Measure Omega} [IsProbabilityMeasure mu]
    (sample : Omega → E) (population : E →L[ℝ] E)
    (hsampleUnit : ∀ omega, ‖sample omega‖ = 1)
    (hRankOneIntegrable :
      Integrable (fun omega =>
        InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) mu)
    (hPopulation :
      ∫ omega, InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu =
        population) :
    IsSelfAdjoint population ∧
      ‖population‖ ≤ 1 ∧
      (∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu =
        population - population ^ (2 : ℕ)) ∧
      ‖population - population ^ (2 : ℕ)‖ ≤ 2 * ‖population‖

Exact module and namespace context

Proof roadmap

1Integrate rank-one symmetry
Every self outer product is symmetric. Evaluation and the real inner product commute with the Bochner integral, so the expectation C is self-adjoint.
2Bound the population operator
The Bochner integral norm is at most the integral of the pointwise operator norm. Unit norm makes ‖X⊗X‖=1, and a probability measure gives total mass one.
3Expand the centered square
A unit-vector outer product is an idempotent projection. Expanding the noncommutative square and commuting left and right multiplication with integration turns both cross terms into C².
4Control the variance operator
Submultiplicativity gives ‖C²‖≤‖C‖². Since ‖C‖≤1, the triangle inequality yields ‖C-C²‖≤2‖C‖.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space and μ is a probability measure.
X has norm exactly one at every point; no almost-everywhere weakening is hidden.
The rank-one operator X⊗X is Bochner integrable and its integral is the supplied population operator C.
No independent sample family, dimension, matrix exponential, or concentration theorem is assumed.

Mathematical proof

1. Integrate rank-one symmetry

Every self outer product is symmetric. Evaluation and the real inner product commute with the Bochner integral, so the expectation C is self-adjoint.

\[(X\otimes X)^*=X\otimes X\Longrightarrow C^*=C\]

Corresponding Lean step

Use isSymmetric_rankOne_self, ContinuousLinearMap.integral_apply, integral_inner, and isSelfAdjoint_iff_isSymmetric.

2. Bound the population operator

The Bochner integral norm is at most the integral of the pointwise operator norm. Unit norm makes ‖X⊗X‖=1, and a probability measure gives total mass one.

\[\|C\|\le\mathbb E\|X\otimes X\|=1\]

Corresponding Lean step

Apply norm_integral_le_of_norm_le_const and norm_rankOne_self_eq_sq.

3. Expand the centered square

A unit-vector outer product is an idempotent projection. Expanding the noncommutative square and commuting left and right multiplication with integration turns both cross terms into C².

\[(X\otimes X-C)^2=X\otimes X-(X\otimes X)C-C(X\otimes X)+C^2\]

Corresponding Lean step

Use isStarProjection_rankOne_self, noncomm_ring, integral_sub/add, and ContinuousLinearMap.integral_comp_comm.

4. Control the variance operator

Submultiplicativity gives ‖C²‖≤‖C‖². Since ‖C‖≤1, the triangle inequality yields ‖C-C²‖≤2‖C‖.

\[\|C-C^2\|\le\|C\|+\|C\|^2\le2\|C\|\]

Corresponding Lean step

Use norm_sub_le, norm_pow_le', hNorm, and real arithmetic.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitRankOneCovariance_momentPackage

The proof integrates pointwise rank-one symmetry, applies the Bochner norm bound, expands the noncommutative centered square using rank-one idempotence, commutes multiplication through the integral, and finishes with the operator-norm triangle inequality.

Download module (.lean)

theorem unitRankOneCovariance_momentPackage
    [CompleteSpace E]
    {Omega : Type*} [MeasurableSpace Omega]
    {mu : Measure Omega} [IsProbabilityMeasure mu]
    (sample : Omega → E) (population : E →L[ℝ] E)
    (hsampleUnit : ∀ omega, ‖sample omega‖ = 1)
    (hRankOneIntegrable :
      Integrable (fun omega =>
        InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) mu)
    (hPopulation :
      ∫ omega, InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu =
        population) :
    IsSelfAdjoint population ∧
      ‖population‖ ≤ 1 ∧
      (∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu =
        population - population ^ (2 : ℕ)) ∧
      ‖population - population ^ (2 : ℕ)‖ ≤ 2 * ‖population‖ := by
  let A := E →L[ℝ] E
  have hSelfAdjoint : IsSelfAdjoint population := by
    rw [ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric]
    intro x y
    have hx : Integrable
        (fun omega =>
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) mu :=
      (ContinuousLinearMap.apply ℝ E x).integrable_comp hRankOneIntegrable
    have hy : Integrable
        (fun omega =>
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y) mu :=
      (ContinuousLinearMap.apply ℝ E y).integrable_comp hRankOneIntegrable
    rw [← hPopulation]
    calc
      inner ℝ ((∫ omega,
          InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) x) y =
          inner ℝ (∫ omega,
            (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x ∂mu) y := by
        rw [ContinuousLinearMap.integral_apply hRankOneIntegrable]
      _ = inner ℝ y (∫ omega,
            (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x ∂mu) :=
        real_inner_comm _ _
      _ = ∫ omega,
            inner ℝ y
              ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) ∂mu :=
        (integral_inner hx y).symm
      _ = ∫ omega,
            inner ℝ x
              ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y) ∂mu := by
        apply integral_congr_ae
        filter_upwards with omega
        calc
          inner ℝ y
              ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) =
              inner ℝ
                ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) y :=
            real_inner_comm _ _
          _ = inner ℝ x
                ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y) :=
            (InnerProductSpace.isSymmetric_rankOne_self
              (𝕜 := ℝ) (sample omega)) x y
      _ = inner ℝ x (∫ omega,
            (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y ∂mu) :=
        integral_inner hy x
      _ = inner ℝ x ((∫ omega,
          InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) y) := by
        rw [ContinuousLinearMap.integral_apply hRankOneIntegrable]
  have hNorm : ‖population‖ ≤ 1 := by
    rw [← hPopulation]
    calc
      ‖∫ omega,
          InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu‖ ≤
          1 * mu.real Set.univ := by
        apply norm_integral_le_of_norm_le_const
        filter_upwards with omega
        rw [norm_rankOne_self_eq_sq, hsampleUnit omega]
        norm_num
      _ = 1 := by simp
  have hright : Integrable
      (fun omega =>
        InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population) mu :=
    ((ContinuousLinearMap.mul ℝ A).flip population).integrable_comp
      hRankOneIntegrable
  have hleft : Integrable
      (fun omega =>
        population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) mu :=
    (ContinuousLinearMap.mul ℝ A population).integrable_comp
      hRankOneIntegrable
  have hconst : Integrable (fun _ : Omega => population ^ (2 : ℕ)) mu :=
    integrable_const _
  have hSecondMoment :
      ∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu =
        population - population ^ (2 : ℕ) := by
    calc
      (∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu) =
          ∫ omega,
            InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
              population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) +
              population ^ (2 : ℕ) ∂mu := by
        apply integral_congr_ae
        filter_upwards with omega
        have hp := rankOne_self_sq_of_norm_one (sample omega) (hsampleUnit omega)
        calc
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
              population) ^ (2 : ℕ) =
              (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) ^ (2 : ℕ) -
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) +
                population ^ (2 : ℕ) := by
            noncomm_ring
          _ = _ := by rw [hp]
      _ = (∫ omega,
            InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) -
            (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) -
            (∫ omega,
              population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) +
            (∫ _ : Omega, population ^ (2 : ℕ) ∂mu) := by
        have hthree :
            (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) =
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) -
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) -
              (∫ omega,
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) := by
          have houter := integral_sub (hRankOneIntegrable.sub hright) hleft
          have hinner := integral_sub hRankOneIntegrable hright
          calc
            (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                  population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) =
                (∫ omega,
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                    InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) -
                (∫ omega,
                  population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) := by
              simpa only [Pi.sub_apply] using houter
            _ = _ := by rw [hinner]
        have hadd := integral_add
          (hRankOneIntegrable.sub hright |>.sub hleft) hconst
        calc
          (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) +
                population ^ (2 : ℕ) ∂mu) =
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                  population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) +
              (∫ _ : Omega, population ^ (2 : ℕ) ∂mu) := by
            simpa only [Pi.add_apply, Pi.sub_apply] using hadd
          _ = _ := by rw [hthree]
      _ = population - population ^ (2 : ℕ) := by
        have hrightInt :
            (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) =
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) *
                population := by
          simpa [A, mul_apply_eq_comp] using
            ContinuousLinearMap.integral_comp_comm
              ((ContinuousLinearMap.mul ℝ A).flip population)
              hRankOneIntegrable
        have hleftInt :
            (∫ omega,
              population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) =
              population *
                (∫ omega,
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) := by
          simpa [A, mul_apply_eq_comp] using
            ContinuousLinearMap.integral_comp_comm
              (ContinuousLinearMap.mul ℝ A population) hRankOneIntegrable
        rw [hPopulation, hrightInt, hleftInt]
        simp [hPopulation]
        noncomm_ring
  have hVariance :
      ‖population - population ^ (2 : ℕ)‖ ≤ 2 * ‖population‖ := by
    calc
      ‖population - population ^ (2 : ℕ)‖ ≤
          ‖population‖ + ‖population ^ (2 : ℕ)‖ := norm_sub_le _ _
      _ ≤ ‖population‖ + ‖population‖ ^ (2 : ℕ) := by
        gcongr
        exact norm_pow_le' _ (by norm_num)
      _ ≤ 2 * ‖population‖ := by
        nlinarith [norm_nonneg population]
  exact ⟨hSelfAdjoint, hNorm, hSecondMoment, hVariance⟩

end EmpiricalCovariance
end Probability
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

This is the expectation-level moment calculation immediately before matrix Bernstein. It does not establish independence, an operator MGF bound, a trace inequality, a tail estimate, or sample complexity.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Probability.EmpiricalCovariance.norm_rankOne_self_eq_sq

Mathlib API called (external library)

InnerProductSpace.isStarProjection_rankOne_self
InnerProductSpace.isSymmetric_rankOne_self
ContinuousLinearMap.integral_apply
ContinuousLinearMap.integral_comp_comm
integral_inner
norm_integral_le_of_norm_le_const

Mathematical sources

Tropp, An Introduction to Matrix Concentration Inequalities — Self-adjoint matrix Bernstein setup and sample-covariance variance calculation.
Samplinglib compiled moment package — Self-adjointness, contraction, exact centered second moment, and variance-operator norm bound.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.