Commit 2026-01-06 18:26 a6375940

View on Github →

feat(Analysis/InnerProductSpace): define rank-one operators (#33439) We define rank-one operators on Hilbert spaces (also known as outer product of two vectors). We follow the bra-ket notation way, where rankOne 𝕜 x y a = |x⟩⟨y|_𝕜 a = ⟪y, a⟫_𝕜 • x.

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/End.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added theorem InnerProductSpace.adjoint_rankOne

added theorem InnerProductSpace.isStarProjection_rankOne_self

added theorem InnerProductSpace.rankOne_comp

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

added theorem InnerProductSpace.rank_rankOne

Modified Mathlib/Analysis/InnerProductSpace/LinearMap.lean

added theorem ContinuousLinearMap.toLinearMap_innerSL_apply

added theorem InnerProductSpace.comp_rankOne

added theorem InnerProductSpace.enorm_rankOne

added theorem InnerProductSpace.inner_left_rankOne_apply

added theorem InnerProductSpace.inner_right_rankOne_apply

added theorem InnerProductSpace.isIdempotentElem_rankOne_self

added theorem InnerProductSpace.isIdempotentElem_rankOne_self_iff

added theorem InnerProductSpace.nnnorm_rankOne

added theorem InnerProductSpace.norm_rankOne

added theorem InnerProductSpace.rankOne_apply

added theorem InnerProductSpace.rankOne_comp_rankOne

added theorem InnerProductSpace.rankOne_def'

added theorem InnerProductSpace.rankOne_def

added theorem InnerProductSpace.rankOne_eq_zero

added theorem InnerProductSpace.rankOne_ne_zero

added theorem InnerProductSpace.rankOne_one_left_eq_innerSL

added theorem InnerProductSpace.rankOne_one_right_eq_toSpanSingleton

added theorem InnerProductSpace.toLinearMap_rankOne

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

added theorem InnerProductSpace.symm_toEuclideanLin_rankOne

added theorem InnerProductSpace.toMatrix_rankOne

added theorem LinearMap.toMatrix_innerₛₗ_apply

added theorem OrthonormalBasis.sum_rankOne_eq_id

deleted theorem toMatrix_innerSL_apply

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

added theorem InnerProductSpace.isPositive_rankOne_self

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

added theorem InnerProductSpace.isSymmetricProjection_rankOne_self

added theorem InnerProductSpace.isSymmetric_rankOne_self

Modified Mathlib/Analysis/InnerProductSpace/Trace.lean

added theorem InnerProductSpace.trace_rankOne

Modified Mathlib/Analysis/Normed/Operator/Bilinear.lean