Revision #3361 → #3908 · back to history
modifiedCauchy–Schwarz for positive functionals on C*-algebras2cc950602f3c
| Field | From #3361 | To #3908 |
|---|
| mathlib.decl | — | PositiveLinearMap.norm_map_star_mul_le |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal |
| note | 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. | `PositiveLinearMap.norm_map_star_mul_le` (aliased `cauchy_schwarz_star_mul`) is exactly the Cauchy–Schwarz inequality ‖f(x*·y)‖ ≤ √‖f(x*·x)‖·√‖f(y*·y)‖ for positive linear functionals on a non-unital star-ordered ℂ-algebra. |
| status | partial | formalized |
modifiedKadison–Schwarz inequality502cd9462937
| Field | From #3361 | To #3908 |
|---|
| note | No declaration for the Kadison–Schwarz inequality f(a)*f(a) ≤ f(a*a) for unital 2-positive maps was found in Mathlib (loogle "Kadison" returns zero hits). | No declaration for the Kadison–Schwarz inequality f(a)*f(a) ≤ f(a*a) for unital 2-positive maps was found in Mathlib (grep for "Kadison" returns zero hits). |
modifiedCallebaut's inequality4b7d3756281a
| Field | From #3361 | To #3908 |
|---|
| note | No declaration for Callebaut's inequality was found in Mathlib (loogle "Callebaut" returns zero hits). | No declaration for Callebaut's inequality was found in Mathlib (grep for "Callebaut" returns zero hits). |
modifiedHilbert space012452962cd3
| Field | From #3361 | To #3908 |
|---|
| note | A Hilbert space is an inner product space that is a `CompleteSpace`; Mathlib expresses this via the `[InnerProductSpace 𝕜 E] [CompleteSpace E]` combination rather than a dedicated `HilbertSpace` typeclass (module corrected via decl_exists). | A Hilbert space is an inner product space that is a `CompleteSpace`; Mathlib expresses this via the `[InnerProductSpace 𝕜 E] [CompleteSpace E]` combination rather than a dedicated `HilbertSpace` typeclass. |
modifiedSquare-integrable complex-valued functions (L²)a709094f3332
| Field | From #3361 | To #3908 |
|---|
| note | `MeasureTheory.Lp E 2 μ` (also `MeasureTheory.L2`) is the space of (equivalence classes of) square-integrable functions, given an inner product space instance in Mathlib.MeasureTheory.Function.L2Space (module corrected via decl_exists). | `MeasureTheory.Lp E 2 μ` (also `MeasureTheory.L2`) is the space of (equivalence classes of) square-integrable functions, given an inner product space instance in Mathlib.MeasureTheory.Function.L2Space. |
addedComplex conjugation6cdfd2f154ce
addedGNS construction / positive functional inner product7a9d6949f9f7