Revision #2594 → #3200 · back to history
modifiedFrobenius inner product on complex matrices68ad2b6420ec
| Field | From #2594 | To #3200 |
|---|
| note | Mathlib has matrix-induced inner products and Matrix.trace, and EuclideanSpace gives a Frobenius-like form, but there is no dedicated `Matrix.frobeniusInner` decl. | `Matrix.toMatrixInnerProductSpace` (with `M = 1`) yields the Frobenius trace inner product, but Mathlib has no dedicated `Matrix.frobeniusInner` decl. |
modifiedPtolemy's inequality characterizes inner-product normscfb4a93d9dcc
| Field | From #2594 | To #3200 |
|---|
| mathlib.module | Mathlib.Geometry.Euclidean.Sphere.Ptolemy | Mathlib.Geometry.Euclidean.Inversion.Basic |
| note | Mathlib proves Ptolemy's inequality in Euclidean geometry but not the characterization that Ptolemy's inequality detects inner-product norms among general normed spaces. | Mathlib proves Ptolemy's inequality in Euclidean geometry (`Inversion.Basic`) but not the characterization that it detects inner-product norms among general normed spaces. |
modifiedPythagorean theorem for pairwise orthogonal vectorscda03e9ff86c
| Field | From #2594 | To #3200 |
|---|
| note | Mathlib's `OrthogonalFamily` / `Orthonormal.norm_sum_sq`-style lemmas extend Pythagoras to finite orthogonal sums. | Mathlib's `OrthogonalFamily.norm_sum` extends Pythagoras to finite orthogonal sums via `Subspace.lean`. |
modifiedSeparable inner product space has orthonormal basis017161e799ee
| Field | From #2594 | To #3200 |
|---|
| mathlib.decl | — | exists_hilbertBasis |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.InnerProductSpace.l2Space |
| note | Mathlib has `exists_orthonormalBasis` only in finite dimensions; no general existence theorem for separable Hilbert spaces is stated. | Mathlib's `exists_hilbertBasis` gives a Hilbert basis for any Hilbert space (assumes completeness); the general separable-but-not-necessarily-complete case is not stated. |
| status | not_formalized | partial |
modifiedComplete inner product space has orthonormal basis351e8a8d4817
| Field | From #2594 | To #3200 |
|---|
| mathlib.decl | exists_orthonormalBasis | exists_hilbertBasis |
| mathlib.match_kind | special_case | exact |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.PiL2 | Mathlib.Analysis.InnerProductSpace.l2Space |
| note | `exists_orthonormalBasis` covers the finite-dimensional case; the general Zorn-based existence of a `HilbertBasis` in any Hilbert space is not formalized. | `exists_hilbertBasis` proves any Hilbert space admits a `HilbertBasis` via Zorn. |
| status | partial | formalized |
addedGram–Schmidt processe21b7c0b0e10
addedOrthogonal projection onto a subspacec6552fcf908b
modifiedIsometry between inner product spaces8633365ab0d2
| Field | From #2594 | To #3200 |
|---|
| mathlib.module | Mathlib.Analysis.NormedSpace.LinearIsometry | Mathlib.Analysis.Normed.Operator.LinearIsometry |
modifiedIsometrical isomorphism / unitary operatore92914006f9d
| Field | From #2594 | To #3200 |
|---|
| mathlib.module | Mathlib.Analysis.NormedSpace.LinearIsometry | Mathlib.Analysis.Normed.Operator.LinearIsometry |