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
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‖².
Lean statement · norm_rankOne_self_eq_sq
The equality is stated directly for Mathlib's continuous rank-one operator.
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.
theorem norm_rankOne_self_eq_sq (x : E) :
‖InnerProductSpace.rankOne ℝ x x‖ = ‖x‖ ^ 2Proof 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‖.
Corresponding Lean step
Simplify InnerProductSpace.rankOne with its norm theorem.
2. Rewrite the product as a square
The identical norm factors are exactly ‖x‖².
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.
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.
theorem norm_rankOne_self_eq_sq (x : E) :
‖InnerProductSpace.rankOne ℝ x x‖ = ‖x‖ ^ 2 := by
simp [pow_two]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.