Diff — Hilbert space

Revision #1836 → #2349 · back to history

addedTriangle inequality for the inner-product norm6788dfa301c8

addedOrthonormal sequences converge weakly to zero91c190d70693

addedAdjoint is involutive (A** = A)4b4135a1de6a

modifiedSpectral theorem for unbounded self-adjoint operators (box)6c20e7031758

Field	From #1836	To #2349
note	The unbounded spectral theorem (resolution of identity for unbounded self-adjoint operators) is not in Mathlib.	The unbounded spectral theorem (resolution of identity for unbounded self-adjoint operators) is notin Mathlib.