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.

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)

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.