Revision #2854 → #3361 · back to history
modifiedCauchy–Schwarz for positive functionals on C*-algebras2cc950602f3c
| Field | From #2854 | To #3361 |
|---|
| mathlib.decl | PositiveLinearMap.preGNSpreInnerProdSpace | — |
| mathlib.match_kind | invocation | — |
| mathlib.module | Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal | — |
| note | The GNS construction defines the pre-inner product ⟪a,b⟫ = f(a*·b) from a positive functional, so Cauchy–Schwarz follows by invoking `inner_mul_inner_self_le`, but no standalone named theorem states it. | No standalone named theorem for the C*-algebra positive-functional Cauchy–Schwarz was located; the GNS construction (Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal) builds the pre-inner product ⟪a,b⟫ = f(a*·b), from which the inequality follows by `inner_mul_inner_self_le`, but no direct decl states it. |
| provenance | ai | ai-moderated |
modifiedDot product on Rⁿfe2969439e9a
| Field | From #2854 | To #3361 |
|---|
| note | The standard inner product on Rⁿ is the dot product ∑ xᵢyᵢ, realized in Mathlib via `EuclideanSpace` whose inner product equals the (conjugated) dot product (module corrected from EuclideanDist to PiL2 per decl_exists). | The standard inner product on Rⁿ is the dot product ∑ xᵢyᵢ, realized in Mathlib via `EuclideanSpace` whose inner product equals the (conjugated) dot product. |
modifiedPositive linear functionaldc1b3a404dee
| Field | From #2854 | To #3361 |
|---|
| note | `PositiveLinearMap` is Mathlib's typeclass for positive (order-preserving) linear maps; corrected from the non-existent `CStarAlgebra.IsPositive` verified via decl_exists. | `PositiveLinearMap` is Mathlib's typeclass for positive (order-preserving) linear maps, which generalizes positive linear functionals into codomain ℝ. |
modifiedC*-algebra0970bcdb64cb
| Field | From #2854 | To #3361 |
|---|
| note | `CStarAlgebra` is the typeclass for a Banach *-algebra satisfying the C* identity ‖a*·a‖ = ‖a‖², providing the setting for the operator-algebra Cauchy–Schwarz generalizations (module corrected from Basic to Classes per decl_exists). | `CStarAlgebra` is the typeclass for a Banach *-algebra satisfying the C* identity ‖a*·a‖ = ‖a‖², the setting for the operator-algebra Cauchy–Schwarz generalizations. |
addedHilbert space012452962cd3
addedSquare-integrable complex-valued functions (L²)a709094f3332
addedCauchy–Schwarz proof via the orthogonal projection517155b0ee95