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.

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 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.