Revision #1290 → #1836 · back to history
modifiedReal inner product842b0017b897
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"An operation on pairs of vectors that, like the dot product, satisfies these three properties is known as a"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {x} \\cdot \\mathbf {y} =\\left\\|\\mathbf {x} \\right\\|\\left\\|\\mathbf {y} \\right\\|\\,\\cos \\theta \\,.}"}] | — |
modifiedReal inner product space4e6cde1fa208
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"A vector space equipped with such an inner product is known as a"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {x} \\cdot \\mathbf {y} =\\left\\|\\mathbf {x} \\right\\|\\left\\|\\mathbf {y} \\right\\|\\,\\cos \\theta \\,.}"}] | — |
modifiedFinite-dimensional inner product spaces are Hilbert0eab229de5dd
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"Every finite-dimensional inner product space is also a Hilbert space"},{"type":"math_alttext","value":"{\\displaystyle \\mathbf {x} \\cdot \\mathbf {y} =\\left\\|\\mathbf {x} \\right\\|\\left\\|\\mathbf {y} \\right\\|\\,\\cos \\theta \\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.Normed.Module.FiniteDimension | Mathlib.Topology.Algebra.Module.FiniteDimension |
modifiedAbsolutely convergent series of vectorse117cf558004
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"is absolutely convergent provided that the sum of the lengths converges as an ordinary series of real numbers"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n=0}^{\\infty }\\mathbf {x} _{n}}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }\\|\\mathbf {x} _{k}\\|<\\infty \\,.}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{N\\to \\infty }\\left\\|\\mathbf {L} -\\sum _{k=0}^{N}\\mathbf {x} _{k}\\right\\|=0.}"}] | — |
modifiedCompleteness of Euclidean space6bb0f3a6edd5
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"This property expresses the completeness of Euclidean space"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n=0}^{\\infty }\\mathbf {x} _{n}}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }\\|\\mathbf {x} _{k}\\|<\\infty \\,.}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{N\\to \\infty }\\left\\|\\mathbf {L} -\\sum _{k=0}^{N}\\mathbf {x} _{k}\\right\\|=0.}"}] | — |
modifiedComplex modulus6198a0fdc74b
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"the complex modulus | z | , which is defined as the square root of the product of z with its complex conjugate"},{"type":"math_alttext","value":"{\\displaystyle |z|^{2}=z{\\overline {z}}\\,.}"}] | — |
| mathlib.decl | Complex.abs | Complex.normSq |
| mathlib.match_kind | exact | generalization |
| note | The complex modulus is `Complex.abs`. | `Complex.normSq z = z * conj z` is the square of the modulus; the modulus itself is `‖z‖` via `Complex.instNorm`. |
modifiedInner product on complex numbers2859b2a6fc6a
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"The inner product of a pair of complex numbers z and w is the product of z with the complex conjugate of w"},{"type":"math_alttext","value":"{\\displaystyle \\langle z,w\\rangle =z{\\overline {w}}\\,.}"}] | — |
| mathlib.decl | Complex.innerProductSpace | RCLike.innerProductSpace |
| mathlib.match_kind | exact | generalization |
| note | The standard `InnerProductSpace ℂ ℂ` instance gives `⟪z,w⟫ = conj w * z`. | `RCLike.innerProductSpace` gives `InnerProductSpace ℂ ℂ` with `⟪z,w⟫ = conj w * z`. |
modifiedInner product on C²3624708592f9
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"A second example is the space"},{"type":"math_alttext","value":"{\\displaystyle \\langle z,w\\rangle =z_{1}{\\overline {w}}_{1}+z_{2}{\\overline {w}}_{2}\\,.}"}] | — |
modifiedHermitian symmetry of the C² inner product7e7c7fb92ab4
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Motivation","snippet":"This inner product is Hermitian symmetric"},{"type":"math_alttext","value":"{\\displaystyle \\langle w,z\\rangle ={\\overline {\\langle z,w\\rangle }}\\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Defs | Mathlib.Analysis.InnerProductSpace.Basic |
modifiedConjugate symmetry of inner product9c7d1a0fd6a9
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"The inner product is conjugate symmetric"},{"type":"math_alttext","value":"{\\displaystyle \\langle y,x\\rangle ={\\overline {\\langle x,y\\rangle }}\\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Defs | Mathlib.Analysis.InnerProductSpace.Basic |
| note | `inner_conj_symm : ⟪y,x⟫ = conj ⟪x,y⟫` is in `InnerProductSpace.Defs`. | `inner_conj_symm : ⟪y,x⟫ = conj ⟪x,y⟫` holds in any `InnerProductSpace`. |
modifiedLinearity in first argument6537313f43a7
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"The inner product is linear in its first argument"},{"type":"math_alttext","value":"{\\displaystyle \\langle ax_{1}+bx_{2},y\\rangle =a\\langle x_{1},y\\rangle +b\\langle x_{2},y\\rangle \\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Defs | Mathlib.Analysis.InnerProductSpace.Basic |
modifiedPositive definiteness of inner productdfa8d71bb93b
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"The inner product of an element with itself is positive definite"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{alignedat}{4}\\langle x,x\\rangle >0&\\quad {\\text{ if }}x\\neq 0,\\\\\\langle x,x\\rangle =0&\\quad {\\text{ if }}x=0\\,.\\end{alignedat}}}"}] | — |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Defs | Mathlib.Analysis.InnerProductSpace.Basic |
modifiedAntilinearity in second argument61d70aa191c0
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"It follows from properties 1 and 2 that a complex inner product is antilinear"},{"type":"math_alttext","value":"{\\displaystyle \\langle x,ay_{1}+by_{2}\\rangle ={\\bar {a}}\\langle x,y_{1}\\rangle +{\\bar {b}}\\langle x,y_{2}\\rangle \\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Defs | Mathlib.Analysis.InnerProductSpace.Basic |
modifiedNorm and distance from inner product41ba29ea7504
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"The norm is the real-valued function"},{"type":"math_alttext","value":"{\\displaystyle \\|x\\|={\\sqrt {\\langle x,x\\rangle }}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle d(x,y)=\\|x-y\\|={\\sqrt {\\langle x-y,x-y\\rangle }}\\,.}"},{"type":"math_alttext","value":"{\\displaystyle d(x,z)\\leq d(x,y)+d(y,z)\\,.}"}] | — |
modifiedCauchy–Schwarz inequality860d60ade728
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"This last property is ultimately a consequence of the more fundamental Cauchy–Schwarz inequality"},{"type":"math_alttext","value":"{\\displaystyle \\left|\\langle x,y\\rangle \\right|\\leq \\|x\\|\\|y\\|}"}] | — |
| mathlib.decl | inner_mul_le_norm_mul_norm | norm_inner_le_norm |
| note | Cauchy–Schwarz is `inner_mul_le_norm_mul_norm` (with several equivalent forms). | Cauchy–Schwarz is `norm_inner_le_norm : ‖⟪x,y⟫‖ ≤ ‖x‖ * ‖y‖`. |
modifiedCompleteness via Cauchy criterion / absolute convergence2fa84cfd2022
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Formal definition","snippet":"The completeness of H is expressed using a form of the Cauchy criterion for sequences in H"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }u_{k}}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }\\|u_{k}\\|<\\infty \\,,}"}] | — |
| mathlib.decl | summable_of_summable_norm | Summable.of_norm |
| note | In any complete normed group, absolute convergence implies convergence. | In any complete normed group, absolute convergence implies convergence via `Summable.of_norm`. |
modifiedClosed linear subspace is a Hilbert space6ac602c480a5
| Field | From #1290 | To #1836 |
|---|
| mathlib.decl | Submodule.instInnerProductSpace | Submodule.innerProductSpace |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Basic | Mathlib.Analysis.InnerProductSpace.Subspace |
| note | A submodule inherits an `InnerProductSpace` instance; closed submodules of complete spaces are complete. | A submodule inherits an `InnerProductSpace` instance via `Submodule.innerProductSpace`; closed submodules of complete spaces are complete. |
modifiedSequence space ℓ²7e3cff42149e
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sequence spaces","snippet":"consists of all infinite sequences"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n=1}^{\\infty }|z_{n}|^{2}}"}] | — |
modifiedInner product on ℓ²be89102f359b
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sequence spaces","snippet":"The inner product on l 2 is defined by"},{"type":"math_alttext","value":"{\\displaystyle \\langle \\mathbf {z} ,\\mathbf {w} \\rangle =\\sum _{n=1}^{\\infty }z_{n}{\\overline {w}}_{n}\\,,}"}] | — |
modifiedCompleteness of ℓ²70f1f4bb98b8
| Field | From #1290 | To #1836 |
|---|
| anchor.snippet | Completeness of the space holds provided that whenever a series of elements | Completeness of the space holds provided that whenever a series of elements from |
| mathlib.decl | lp.instCompleteSpace | lp.completeSpace |
| note | `lp` spaces are complete via the standard `CompleteSpace` instance. | `lp.completeSpace` provides `CompleteSpace (lp E p)` for `p ≥ 1`. |
modifiedLebesgue space L²(X, μ)c8468bd6e9cf
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Lebesgue spaces","snippet":"Lebesgue spaces are function spaces associated to measure spaces"},{"type":"math_alttext","value":"{\\displaystyle \\int _{X}|f|^{2}\\,\\mathrm {d} \\mu <\\infty \\,,}"}] | — |
modifiedInner product on L²b6b3408fb8f5
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Lebesgue spaces","snippet":"The inner product of functions f and g in L 2 ( X , μ ) is then defined as"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle =\\int _{X}f(t){\\overline {g(t)}}\\,\\mathrm {d} \\mu (t)}"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle =\\int _{X}{\\overline {f(t)}}g(t)\\,\\mathrm {d} \\mu (t)\\,,}"}] | — |
modifiedCompleteness of L²131473e830b5
| Field | From #1290 | To #1836 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Function.LpSpace.Basic | Mathlib.MeasureTheory.Function.LpSpace.Complete |
modifiedWeighted L² space278b55b3f1ac
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Lebesgue spaces","snippet":"is called the weighted L 2 space"},{"type":"math_alttext","value":"{\\displaystyle \\int _{0}^{1}{\\bigl |}f(t){\\bigr |}^{2}w(t)\\,\\mathrm {d} t<\\infty }"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle =\\int _{0}^{1}f(t){\\overline {g(t)}}w(t)\\,\\mathrm {d} t\\,.}"}] | — |
modifiedSobolev space H^s0ae6b75ff169
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sobolev spaces","snippet":"the Sobolev space H s (Ω) contains L 2 functions whose weak derivatives of order up to s are also L 2"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle =\\int _{\\Omega }f(x){\\bar {g}}(x)\\,\\mathrm {d} x+\\int _{\\Omega }Df(x)\\cdot D{\\bar {g}}(x)\\,\\mathrm {d} x+\\cdots +\\int _{\\Omega }D^{s}f(x)\\cdot D^{s}{\\bar {g}}(x)\\,\\mathrm {d} x}"}] | — |
modifiedSobolev space as Bessel potentials551c1af565d0
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sobolev spaces","snippet":"one can define the Sobolev space H s (Ω) as the space of Bessel potentials"},{"type":"math_alttext","value":"{\\displaystyle H^{s}(\\Omega )=\\left\\{(1-\\Delta )^{-s/2}f\\mathrel {\\Big |} f\\in L^{2}(\\Omega )\\right\\}\\,.}"}] | — |
modifiedHardy space H²(U)63a14693f536
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Hardy spaces","snippet":"the Hardy space H 2 ( U ) is defined as the space of holomorphic functions f on U such that the means"},{"type":"math_alttext","value":"{\\displaystyle M_{r}(f)={\\frac {1}{2\\pi }}\\int _{0}^{2\\pi }\\left|f{\\bigl (}re^{i\\theta }{\\bigr )}\\right|^{2}\\,\\mathrm {d} \\theta }"},{"type":"math_alttext","value":"{\\displaystyle \\left\\|f\\right\\|_{2}=\\lim _{r\\to 1}{\\sqrt {M_{r}(f)}}\\,.}"}] | — |
modifiedBergman spaceb210a656dce1
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bergman spaces","snippet":"let L 2, h ( D ) be the space of holomorphic functions f in D that are also in L 2 ( D )"},{"type":"math_alttext","value":"{\\displaystyle \\|f\\|^{2}=\\int _{D}|f(z)|^{2}\\,\\mathrm {d} \\mu (z)<\\infty \\,,}"},{"type":"math_alttext","value":"{\\displaystyle \\sup _{z\\in K}\\left|f(z)\\right|\\leq C_{K}\\left\\|f\\right\\|_{2}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle f(z)=\\int _{D}f(\\zeta ){\\overline {\\eta _{z}(\\zeta )}}\\,\\mathrm {d} \\mu (\\zeta )}"},{"type":"math_alttext","value":"{\\displaystyle K(\\zeta ,z)={\\overline {\\eta _{z}(\\zeta )}}}"},{"type":"math_alttext","value":"{\\displaystyle f(z)=\\int _{D}f(\\zeta )K(\\zeta ,z)\\,\\mathrm {d} \\mu (\\zeta )\\,.}"}] | — |
modifiedBergman kernel reproducing property086cb2cc967b
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bergman spaces","snippet":"is known as the Bergman kernel of D"},{"type":"math_alttext","value":"{\\displaystyle \\|f\\|^{2}=\\int _{D}|f(z)|^{2}\\,\\mathrm {d} \\mu (z)<\\infty \\,,}"},{"type":"math_alttext","value":"{\\displaystyle \\sup _{z\\in K}\\left|f(z)\\right|\\leq C_{K}\\left\\|f\\right\\|_{2}\\,,}"},{"type":"math_alttext","value":"{\\displaystyle f(z)=\\int _{D}f(\\zeta ){\\overline {\\eta _{z}(\\zeta )}}\\,\\mathrm {d} \\mu (\\zeta )}"},{"type":"math_alttext","value":"{\\displaystyle K(\\zeta ,z)={\\overline {\\eta _{z}(\\zeta )}}}"},{"type":"math_alttext","value":"{\\displaystyle f(z)=\\int _{D}f(\\zeta )K(\\zeta ,z)\\,\\mathrm {d} \\mu (\\zeta )\\,.}"}] | — |
modifiedReproducing kernel Hilbert spacea0e4e993e716
| Field | From #1290 | To #1836 |
|---|
| mathlib.decl | InnerProductSpace.Reproducing | RKHS |
| mathlib.match_kind | generalization | exact |
| note | `Reproducing.lean` develops a reproducing-kernel framework on Hilbert spaces. | `RKHS` in `Reproducing.lean` is the class of reproducing kernel Hilbert spaces. |
| status | partial | formalized |
modifiedSturm–Liouville problem5a2f5a9d6014
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sturm–Liouville theory","snippet":"the Sturm–Liouville problem arises in the study of the harmonics of waves in a violin string or a drum"},{"type":"math_alttext","value":"{\\displaystyle -{\\frac {\\mathrm {d} }{\\mathrm {d} x}}\\left[p(x){\\frac {\\mathrm {d} y}{\\mathrm {d} x}}\\right]+q(x)y=\\lambda w(x)y}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{cases}\\alpha y(a)+\\alpha 'y'(a)&=0\\\\\\beta y(b)+\\beta 'y'(b)&=0\\,.\\end{cases}}}"}] | — |
modifiedPoisson equation weak formulationab7fdee7b315
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Partial differential equations","snippet":"An example is the Poisson equation"},{"type":"math_alttext","value":"{\\displaystyle \\int _{\\Omega }\\nabla u\\cdot \\nabla v=\\int _{\\Omega }gv\\,.}"}] | — |
modifiedErgodic dynamical system94d109c06910
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Ergodic theory","snippet":"An ergodic dynamical system is one for which, apart from the energy"},{"type":"math_alttext","value":"{\\displaystyle f(T_{t}w)=f(w)}"},{"type":"math_alttext","value":"{\\displaystyle \\left\\langle f,g\\right\\rangle _{L^{2}\\left(\\Omega _{E},\\mu \\right)}=\\int _{\\Omega _{E}}f{\\bar {g}}\\,\\mathrm {d} \\mu \\,.}"}] | — |
modifiedVon Neumann mean ergodic theorem0e3f82f52b1d
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Ergodic theory","snippet":"The von Neumann mean ergodic theorem"},{"type":"math_alttext","value":"{\\displaystyle Px=\\lim _{T\\to \\infty }{\\frac {1}{T}}\\int _{0}^{T}U_{t}x\\,\\mathrm {d} t\\,.}"}] | — |
modifiedOrthonormal basis of exponentials in L²([0,1])ceb46c191308
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Fourier analysis","snippet":"form an orthogonal basis of the Hilbert space"},{"type":"math_alttext","value":"{\\displaystyle f(\\theta )=\\sum _{n}a_{n}e_{n}(\\theta )\\,,\\quad a_{n}=\\langle f,e_{n}\\rangle }"}] | — |
modifiedBest L² approximation via orthogonal projection411340eb32ff
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Fourier analysis","snippet":"Geometrically, the best approximation is the orthogonal projection of f onto the subspace"},{"type":"math_alttext","value":"{\\displaystyle a_{j}=\\int _{0}^{1}{\\overline {e_{j}(x)}}f(x)\\,\\mathrm {d} x\\,.}"}] | — |
modifiedPythagorean theorem of statisticsc63b731dd560
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Probability theory","snippet":"sometimes called the Pythagorean theorem of statistics"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Var} (X+Y)=\\operatorname {Var} (X)+\\operatorname {Var} (Y),}"}] | — |
| mathlib.decl | MeasureTheory.condexpL2 | MeasureTheory.condExpL2 |
| note | The L² conditional expectation as orthogonal projection encodes this identity, though not stated as a labeled "Pythagorean theorem of statistics". | The L² conditional expectation `condExpL2` as orthogonal projection encodes this identity, though not labeled as a "Pythagorean theorem of statistics". |
modifiedItô isometry8788cafe723e
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Probability theory","snippet":"A noteworthy result is then the Itô isometry"},{"type":"math_alttext","value":"{\\displaystyle E\\left[\\left(\\int _{0}^{t}H_{s}\\,dM_{s}\\right)^{2}\\right]=E\\left[\\int _{0}^{t}H_{s}^{2}\\,d\\langle M\\rangle _{s}\\right]}"}] | — |
modifiedPythagorean identity in Hilbert spacec5ce707c9138
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Pythagorean identity","snippet":"Whereas the Pythagorean identity as stated is valid in any inner product space"},{"type":"math_alttext","value":"{\\displaystyle {\\Biggl \\|}\\sum _{k=0}^{\\infty }u_{k}{\\Biggr \\|}^{2}=\\sum _{k=0}^{\\infty }\\left\\|u_{k}\\right\\|^{2}\\,.}"}] | — |
| note | Pythagorean identities are stated in several forms in `InnerProductSpace.Basic` (lines 553–592). | Pythagorean identities are stated in several forms in `InnerProductSpace.Basic`. |
modifiedParallelogram identityae6f3209eb4b
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Parallelogram identity and polarization","snippet":"in every Hilbert space the following parallelogram identity holds"},{"type":"math_alttext","value":"{\\displaystyle \\|u+v\\|^{2}+\\|u-v\\|^{2}=2{\\bigl (}\\|u\\|^{2}+\\|v\\|^{2}{\\bigr )}\\,.}"}] | — |
modifiedPolarization identity characterization of Hilbert spaces58c43dbbf84a
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Parallelogram identity and polarization","snippet":"Conversely, every Banach space in which the parallelogram identity holds is a Hilbert space"},{"type":"math_alttext","value":"{\\displaystyle \\langle u,v\\rangle ={\\tfrac {1}{4}}{\\bigl (}\\|u+v\\|^{2}-\\|u-v\\|^{2}{\\bigr )}\\,.}"}] | — |
modifiedHilbert projection theorem438c2f2fda77
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Best approximation","snippet":"This subsection employs the Hilbert projection theorem"},{"type":"math_alttext","value":"{\\displaystyle y\\in C\\,,\\quad \\|x-y\\|=\\operatorname {dist} (x,C)=\\min {\\bigl \\{}\\|x-z\\|\\mathrel {\\big |} z\\in C{\\bigr \\}}\\,.}"}] | — |
modifiedCharacterization of closest point in closed subspaced7d109d87b64
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Best approximation","snippet":"When this result is applied to a closed subspace F of H , it can be shown that the point"},{"type":"math_alttext","value":"{\\displaystyle y\\in F\\,,\\quad x-y\\perp F\\,.}"}] | — |
modifiedDual space of a Hilbert spacecbdb7646f2cc
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Duality","snippet":"The dual space H * is the space of all continuous linear functions from the space H into the base field"},{"type":"math_alttext","value":"{\\displaystyle \\|\\varphi \\|=\\sup _{\\|x\\|=1,x\\in H}|\\varphi (x)|\\,.}"},{"type":"math_alttext","value":"{\\displaystyle \\langle f,g\\rangle _{H^{*}}=\\sum _{i\\in I}f(e_{i}){\\overline {g(e_{i})}}}"}] | — |
| mathlib.module | Mathlib.Analysis.Normed.Module.Dual | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedRiesz representation theoremb3640cff4c60
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Duality","snippet":"The Riesz representation theorem states that the map from H to H * defined by"},{"type":"math_alttext","value":"{\\displaystyle \\langle x,u_{\\varphi }\\rangle =\\varphi (x)}"},{"type":"math_alttext","value":"{\\displaystyle \\langle \\varphi ,\\psi \\rangle =\\langle u_{\\psi },u_{\\varphi }\\rangle \\,.}"}] | — |
modifiedWeak convergence in Hilbert space597bd61953a8
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Weakly convergent sequences","snippet":"a sequence { x n } is weakly convergent to a vector"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n}\\langle x_{n},v\\rangle =\\langle x,v\\rangle }"}] | — |
| mathlib.module | Mathlib.Analysis.LocallyConvex.WeakSpace | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedBounded linear operator and operator normd16e16772f00
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bounded operators","snippet":"The space of such bounded linear operators has a norm , the operator norm given by"},{"type":"math_alttext","value":"{\\displaystyle \\lVert A\\rVert =\\sup {\\bigl \\{}\\|Ax\\|\\mathrel {\\big |} \\|x\\|\\leq 1{\\bigr \\}}\\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.NormedSpace.OperatorNorm.Basic | Mathlib.Analysis.Normed.Operator.Basic |
modifiedAdjoint of a bounded operatorab3735942378
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bounded operators","snippet":"This defines another bounded linear operator"},{"type":"math_alttext","value":"{\\displaystyle \\left\\langle x,A^{*}y\\right\\rangle =\\langle Ax,y\\rangle }"}] | — |
modifiedB(H) is a C*-algebraeeb2575a9495
| Field | From #1290 | To #1836 |
|---|
| mathlib.decl | ContinuousLinearMap.instCStarAlgebra | instCStarAlgebraContinuousLinearMapComplexIdOfCompleteSpace |
| mathlib.match_kind | exact | special_case |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Adjoint | Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap |
| note | `Adjoint.lean` upgrades `E →L[𝕜] E` to a C*-algebra. | The C*-algebra instance on `E →L[ℂ] E` (for ℂ-Hilbert E) is in `CStarAlgebra/ContinuousLinearMap.lean`. |
modifiedSelf-adjoint and positive operators1e0d00f727f1
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bounded operators","snippet":"An element A of B( H ) is called 'self-adjoint' or 'Hermitian' if"},{"type":"math_alttext","value":"{\\displaystyle A=B^{2}=B^{*}B\\,.}"}] | — |
modifiedSquare root of a positive operator7c3175e69594
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bounded operators","snippet":"for a positive operator A , there exists a unique non-negative square root"},{"type":"math_alttext","value":"{\\displaystyle A=B^{2}=B^{*}B\\,.}"}] | — |
modifiedSpectral theorem for bounded self-adjoint operatorsb0f3c73929e1
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bounded operators","snippet":"The spectral theorem gives a precise sense in which self-adjoint operators play the role of real-valued functions"},{"type":"math_alttext","value":"{\\displaystyle A=\\operatorname {Re} A+i\\operatorname {Im} A={\\frac {A+A^{*}}{2}}+i{\\frac {A-A^{*}}{2i}}.}"}] | — |
| mathlib.module | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital |
addedHilbert–Schmidt operatoraa766fc0ad8a
modifiedFredholm operator and indexdc526f40b271
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bounded operators","snippet":"Fredholm operators are bounded operators that are invertible modulo compact operators"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {index} T=\\dim \\ker T-\\dim \\operatorname {coker} T\\,.}"}] | — |
modifiedUnbounded operatord761afb7cd91
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Unbounded operators","snippet":"An unbounded operator on a Hilbert space H is a linear map"},{"type":"math_alttext","value":"{\\displaystyle T:D(T)\\to H}"}] | — |
modifiedDensely defined operatordb45d98dfc53
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Unbounded operators","snippet":"then T is called a densely defined operator"},{"type":"math_alttext","value":"{\\displaystyle T:D(T)\\to H}"}] | — |
modifiedAdjoint of an unbounded operatorc158d48fd945
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Unbounded operators","snippet":"If T is densely defined, its adjoint"},{"type":"math_alttext","value":"{\\displaystyle x\\mapsto \\langle Tx,y\\rangle ,\\qquad x\\in D(T),}"},{"type":"math_alttext","value":"{\\displaystyle \\langle Tx,y\\rangle =\\langle x,T^{*}y\\rangle }"}] | — |
modifiedSymmetric and self-adjoint operatorsb6b57430e49d
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Unbounded operators","snippet":"A densely defined operator is called symmetric if"},{"type":"math_alttext","value":"{\\displaystyle x\\mapsto \\langle Tx,y\\rangle ,\\qquad x\\in D(T),}"},{"type":"math_alttext","value":"{\\displaystyle \\langle Tx,y\\rangle =\\langle x,T^{*}y\\rangle }"}] | — |
modifiedPosition and momentum operators on L²(R)a42d51c75efb
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Unbounded operators","snippet":"the position operator is the multiplication operator"},{"type":"math_alttext","value":"{\\displaystyle (Qf)(x)=xf(x),}"},{"type":"math_alttext","value":"{\\displaystyle D(Q)=\\{f\\in L^{2}(\\mathbf {R} ):xf(x)\\in L^{2}(\\mathbf {R} )\\}.}"},{"type":"math_alttext","value":"{\\displaystyle (Pf)(x)=-i{\\frac {d}{dx}}f(x),}"}] | — |
modifiedDirect sum of Hilbert spacescf8221a2fcfa
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Direct sums","snippet":"Two Hilbert spaces H 1 and H 2 can be combined into another Hilbert space, called the (orthogonal) direct sum"},{"type":"math_alttext","value":"{\\displaystyle H_{1}\\oplus H_{2}\\,,}"}] | — |
| mathlib.decl | WithLp.prod | WithLp.instProdInnerProductSpace |
| note | Finite/infinite Hilbert direct sums are realized by `WithLp 2 (E × F)`, `PiLp 2`, or `lp G 2`. | Finite/infinite Hilbert direct sums are realized by `WithLp 2 (E × F)` (instance `WithLp.instProdInnerProductSpace`), `PiLp 2`, or `lp G 2`. |
modifiedInternal direct sum of closed subspacesb60491db1710
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Direct sums","snippet":"if there is a system of closed subspaces"},{"type":"math_alttext","value":"{\\displaystyle E_{i}E_{j}=0,\\quad i\\neq j\\,.}"}] | — |
modifiedTensor product of L² with itselfa4104d931a05
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Tensor products","snippet":"An example is provided by the Hilbert space"},{"type":"math_alttext","value":"{\\displaystyle (s,t)\\mapsto f_{1}(s)\\,f_{2}(t)}"}] | — |
modifiedCompleteness criterion for orthonormal systemsa3a33727faea
| Field | From #1290 | To #1836 |
|---|
| mathlib.decl | Orthonormal.orthonormalBasis_of_dense_span | HilbertBasis.mkOfOrthogonalEqBot |
| note | The orthogonal-complement-trivial / dense-span equivalences are in `l2Space.lean` (via `HilbertBasis.mkOfOrthogonalEqBot`). | `HilbertBasis.mkOfOrthogonalEqBot` builds a Hilbert basis from an orthonormal family whose span has trivial orthogonal complement. |
modifiedSquare-summable sequence space ℓ²7d6f7186c801
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sequence spaces (2)","snippet":"is the set of infinite sequences"},{"type":"math_alttext","value":"{\\displaystyle (c_{1},c_{2},c_{3},\\dots )}"},{"type":"math_alttext","value":"{\\displaystyle \\left|c_{1}\\right|^{2}+\\left|c_{2}\\right|^{2}+\\left|c_{3}\\right|^{2}+\\cdots <\\infty \\,.}"}] | — |
modifiedGeneralized ℓ²(B)2e0d05342b24
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Sequence spaces (2)","snippet":"One can generalize the space"},{"type":"math_alttext","value":"{\\displaystyle \\ell ^{2}(B)={\\biggl \\{}x:B\\xrightarrow {x} \\mathbf {C} \\mathrel {\\bigg |} \\sum _{b\\in B}\\left|x(b)\\right|^{2}<\\infty {\\biggr \\}}\\,.}"}] | — |
modifiedBessel's inequalitya7824d49cfb9
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bessel's inequality and Parseval's formula","snippet":"Applying the preceding inequality to every finite subset J of I gives Bessel's inequality"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i\\in I}{\\bigl |}\\langle x,f_{i}\\rangle {\\bigr |}^{2}\\leq \\|x\\|^{2},\\quad x\\in H}"}] | — |
modifiedFourier expansion and Fourier coefficients9a037cb92d64
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bessel's inequality and Parseval's formula","snippet":"This sum is called the Fourier expansion of x , and the individual coefficients"},{"type":"math_alttext","value":"{\\displaystyle \\|x\\|^{2}=\\sum _{k\\in B}|\\langle x,e_{k}\\rangle |^{2}\\,.}"}] | — |
modifiedParseval's identity9d26734ed068
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Bessel's inequality and Parseval's formula","snippet":"Parseval's identity then asserts that"},{"type":"math_alttext","value":"{\\displaystyle \\|x\\|^{2}=\\sum _{k\\in B}|\\langle x,e_{k}\\rangle |^{2}\\,.}"}] | — |
modifiedIsometric isomorphism with ℓ²(B)ddb2f2857a4f
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Hilbert dimension","snippet":"every Hilbert space is isometrically isomorphic to a sequence space"},{"type":"math_alttext","value":"{\\displaystyle {\\bigl \\langle }\\Phi (x),\\Phi (y){\\bigr \\rangle }_{l^{2}(B)}=\\left\\langle x,y\\right\\rangle _{H}}"}] | — |
modifiedMutually orthogonal projections843b80499e28
| Field | From #1290 | To #1836 |
|---|
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Orthogonal | Mathlib.Analysis.InnerProductSpace.Subspace |
modifiedClosure equals double orthogonal complement5d344c39c91b
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Orthogonal complements and projections","snippet":"the closure of a subspace can be completely characterized in terms of the orthogonal complement"},{"type":"math_alttext","value":"{\\displaystyle {\\biggl (}\\sum _{i}V_{i}{\\biggr )}^{\\perp }=\\bigcap _{i}V_{i}^{\\perp }\\,.}"}] | — |
modifiedSpectrum of an operatorf58adaecf4f5
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Spectral theory","snippet":"The spectrum of an operator T , denoted σ ( T ) , is the set of complex numbers"},{"type":"math_alttext","value":"{\\displaystyle m=\\inf _{\\|x\\|=1}\\langle Tx,x\\rangle \\,,\\quad M=\\sup _{\\|x\\|=1}\\langle Tx,x\\rangle \\,.}"}] | — |
| mathlib.module | Mathlib.FieldTheory.Spectrum | Mathlib.Algebra.Algebra.Spectrum.Basic |
| provenance | ai | ai-moderated |
modifiedSpectrum of self-adjoint operators is real and bounded25ffc151d90a
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Spectral theory","snippet":"If T is self-adjoint, then the spectrum is real"},{"type":"math_alttext","value":"{\\displaystyle m=\\inf _{\\|x\\|=1}\\langle Tx,x\\rangle \\,,\\quad M=\\sup _{\\|x\\|=1}\\langle Tx,x\\rangle \\,.}"}] | — |
modifiedSpectral theorem for compact self-adjoint operators804de3f23f67
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Spectral theory","snippet":"A compact self-adjoint operator T has only countably (or finitely) many spectral values"},{"type":"math_alttext","value":"{\\displaystyle H=\\bigoplus _{\\lambda \\in \\sigma (T)}H_{\\lambda }\\,.}"},{"type":"math_alttext","value":"{\\displaystyle T=\\sum _{\\lambda \\in \\sigma (T)}\\lambda E_{\\lambda }\\,,}"}] | — |
modifiedSpectral theorem for bounded self-adjoint operators via spectral family4e3c7e3f16d0
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Spectral theory","snippet":"The general spectral theorem for self-adjoint operators involves a kind of operator-valued Riemann–Stieltjes integral"},{"type":"math_alttext","value":"{\\displaystyle A^{+}={\\tfrac {1}{2}}{\\Bigl (}{\\sqrt {A^{2}}}+A{\\Bigr )}\\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital |
modifiedSpectral mapping theorem8b98fb79c7d6
| Field | From #1290 | To #1836 |
|---|
| anchors | [{"section":"Spectral theory","snippet":"A major application of spectral methods is the spectral mapping theorem"},{"type":"math_alttext","value":"{\\displaystyle f(T)=\\int _{\\sigma (T)}f(\\lambda )\\,\\mathrm {d} E_{\\lambda }\\,.}"}] | — |
| mathlib.module | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic | Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital |
addedEigenspaces of an operator614d1693e0bc