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.