Revision #2525 → #3141 · back to history
modifiedBanach space8d3ff30d3808
| Field | From #2525 | To #3141 |
|---|
| anchor.snippet | A Banach space is a complete normed space | A complete normed space |
| anchors | [{"section":"Definition","snippet":"A Banach space is a complete normed space"},{"type":"math_alttext","value":"{\\displaystyle d(x,y):=\\|y-x\\|=\\|x-y\\|.}"},{"type":"math_alttext","value":"{\\displaystyle d(x_{n},x_{m})=\\|x_{n}-x_{m}\\|<r.}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }x_{n}=x\\;{\\text{ in }}(X,d),}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }\\|x_{n}-x\\|=0\\;{\\text{ in }}\\mathbb {R} .}"}] | — |
modifiedNormed space7ac53cdabe25
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Definition","snippet":"A normed space is a pair"},{"type":"math_alttext","value":"{\\displaystyle d(x,y):=\\|y-x\\|=\\|x-y\\|.}"},{"type":"math_alttext","value":"{\\displaystyle d(x_{n},x_{m})=\\|x_{n}-x_{m}\\|<r.}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }x_{n}=x\\;{\\text{ in }}(X,d),}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }\\|x_{n}-x\\|=0\\;{\\text{ in }}\\mathbb {R} .}"}] | — |
modifiedNorm-induced (canonical) metric5feadb68f62f
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Definition","snippet":"called the canonical or"},{"type":"math_alttext","value":"{\\displaystyle d(x,y):=\\|y-x\\|=\\|x-y\\|.}"},{"type":"math_alttext","value":"{\\displaystyle d(x_{n},x_{m})=\\|x_{n}-x_{m}\\|<r.}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }x_{n}=x\\;{\\text{ in }}(X,d),}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }\\|x_{n}-x\\|=0\\;{\\text{ in }}\\mathbb {R} .}"}] | — |
| mathlib.module | Mathlib.Analysis.Normed.Group.Defs | Mathlib.Analysis.Normed.Group.Basic |
modifiedCauchy sequence045cfc569922
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Definition","snippet":"is called Cauchy in"},{"type":"math_alttext","value":"{\\displaystyle d(x,y):=\\|y-x\\|=\\|x-y\\|.}"},{"type":"math_alttext","value":"{\\displaystyle d(x_{n},x_{m})=\\|x_{n}-x_{m}\\|<r.}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }x_{n}=x\\;{\\text{ in }}(X,d),}"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }\\|x_{n}-x\\|=0\\;{\\text{ in }}\\mathbb {R} .}"}] | — |
modifiedSeries characterization of completeness85a52baa11e4
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Characterization in terms of series","snippet":"is a Banach space if and only if each absolutely convergent series"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{n=1}^{\\infty }\\|v_{n}\\|<\\infty \\implies \\sum _{n=1}^{\\infty }v_{n}{\\text{ converges in }}X.}"}] | — |
modifiedBanach space is a Baire spaced99fbd5127af
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Topology.Baire.CompleteMetrizable | Mathlib.Topology.Defs.Basic |
modifiedOpen and closed balls100db1d956f6
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Topology","snippet":"The open and closed balls of radius"},{"type":"math_alttext","value":"{\\displaystyle B_{r}(x):=\\{z\\in X\\mid \\|z-x\\|<r\\}\\qquad {\\text{ and }}\\qquad C_{r}(x):=\\{z\\in X\\mid \\|z-x\\|\\leq r\\}.}"},{"type":"math_alttext","value":"{\\displaystyle x_{0}+s\\,B_{r}(x)=B_{|s|r}(x_{0}+sx)\\qquad {\\text{ and }}\\qquad x_{0}+s\\,C_{r}(x)=C_{|s|r}(x_{0}+sx).}"},{"type":"math_alttext","value":"{\\displaystyle \\{B_{r}(0)\\mid r>0\\},\\qquad \\{C_{r}(0)\\mid r>0\\},\\qquad \\{B_{r_{n}}(0)\\mid n\\in \\mathbb {N} \\},\\qquad {\\text{ and }}\\qquad \\{C_{r_{n}}(0)\\mid n\\in \\mathbb {N} \\},}"},{"type":"math_alttext","value":"{\\displaystyle U=\\bigcup _{x\\in I}B_{r_{x}}(x)=\\bigcup _{x\\in I}x+B_{r_{x}}(0)=\\bigcup _{x\\in I}x+r_{x}\\,B_{1}(0)}"}] | — |
modifiedCompact ball iff finite-dimensional5afd2eee0573
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Topology","snippet":"a compact ball/ neighborhood exists if and only if"},{"type":"math_alttext","value":"{\\displaystyle B_{r}(x):=\\{z\\in X\\mid \\|z-x\\|<r\\}\\qquad {\\text{ and }}\\qquad C_{r}(x):=\\{z\\in X\\mid \\|z-x\\|\\leq r\\}.}"},{"type":"math_alttext","value":"{\\displaystyle x_{0}+s\\,B_{r}(x)=B_{|s|r}(x_{0}+sx)\\qquad {\\text{ and }}\\qquad x_{0}+s\\,C_{r}(x)=C_{|s|r}(x_{0}+sx).}"},{"type":"math_alttext","value":"{\\displaystyle \\{B_{r}(0)\\mid r>0\\},\\qquad \\{C_{r}(0)\\mid r>0\\},\\qquad \\{B_{r_{n}}(0)\\mid n\\in \\mathbb {N} \\},\\qquad {\\text{ and }}\\qquad \\{C_{r_{n}}(0)\\mid n\\in \\mathbb {N} \\},}"},{"type":"math_alttext","value":"{\\displaystyle U=\\bigcup _{x\\in I}B_{r_{x}}(x)=\\bigcup _{x\\in I}x+B_{r_{x}}(0)=\\bigcup _{x\\in I}x+r_{x}\\,B_{1}(0)}"}] | — |
modifiedFinite-dimensional spaces are separable Banach spaces4ef7e8845bdb
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.FiniteDimension | Mathlib.Topology.Algebra.Module.FiniteDimension |
modifiedTopological vector spacecb84261d8588
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.Basic | Mathlib.Topology.Algebra.MulAction |
modifiedAll norms equivalent in finite dimension28b566b3d676
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.FiniteDimension | Mathlib.Topology.Algebra.Module.FiniteDimension |
modifiedCompletion of a normed space1e321f7c1ffa
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.Completion | Mathlib.Topology.UniformSpace.Completion |
modifiedContinuity iff bounded on unit ball2195e91b2748
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Linear operators, isomorphisms","snippet":"is continuous if and only if it is bounded on the closed unit ball"},{"type":"math_alttext","value":"{\\displaystyle \\|T\\|=\\sup\\{\\|Tx\\|_{Y}\\mid x\\in X,\\ \\|x\\|_{X}\\leq 1\\}.}"}] | — |
modifiedProduct complete iff factors completeee06b056f06a
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Basic notions","snippet":"is complete if and only if the two factors are complete"},{"type":"math_alttext","value":"{\\displaystyle \\|(x,y)\\|_{1}=\\|x\\|+\\|y\\|,\\qquad \\|(x,y)\\|_{\\infty }=\\max(\\|x\\|,\\|y\\|)}"}] | — |
modifiedQuotient norm94cc673390f1
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Basic notions","snippet":"there is a natural norm on the quotient space"},{"type":"math_alttext","value":"{\\displaystyle \\|x+M\\|=\\inf \\limits _{m\\in M}\\|x+m\\|.}"}] | — |
modifiedComplemented subspace597931aa4603
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.Complemented | Mathlib.Topology.Algebra.Module.Complement |
modifiedCanonical factorization of bounded operator34e47a7278bd
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Basic notions","snippet":"There exists a canonical factorization of"},{"type":"math_alttext","value":"{\\displaystyle T=T_{1}\\circ \\pi ,\\quad T:X{\\overset {\\pi }{{}\\longrightarrow {}}}X/\\ker T{\\overset {T_{1}}{{}\\longrightarrow {}}}Y}"}] | — |
modifiedClassical Banach spaces67b8d88f125c
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Classical spaces","snippet":"Basic examples [ 25 ] of Banach spaces include"},{"type":"math_alttext","value":"{\\displaystyle \\|f\\|_{C(K)}=\\max\\{|f(x)|\\mid x\\in K\\},\\quad f\\in C(K).}"}] | — |
modifiedHilbert space as Banach space0ef5268cbaf0
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Classical spaces","snippet":"Any Hilbert space serves as an example of a Banach space"},{"type":"math_alttext","value":"{\\displaystyle \\|x\\|_{H}={\\sqrt {\\langle x,x\\rangle }},}"},{"type":"math_alttext","value":"{\\displaystyle \\langle \\cdot ,\\cdot \\rangle :H\\times H\\to \\mathbb {K} }"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\langle y,x\\rangle &={\\overline {\\langle x,y\\rangle }},\\quad {\\text{ for all }}x,y\\in H\\\\\\langle x,x\\rangle &\\geq 0,\\quad {\\text{ for all }}x\\in H\\\\\\langle x,x\\rangle =0{\\text{ if and only if }}x&=0.\\end{aligned}}}"}] | — |
| mathlib.module | Mathlib.Analysis.InnerProductSpace.Basic | Mathlib.Analysis.InnerProductSpace.Defs |
modifiedContinuous dual spacead45d94c4874
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.Dual | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedHahn–Banach extension of functionalsaaa68e58fe6b
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Dual space","snippet":"every continuous linear functional on a subspace of a normed space can be continuously extended"},{"type":"math_alttext","value":"{\\displaystyle f(x)=\\|x\\|_{X},\\quad \\|f\\|_{X'}\\leq 1.}"}] | — |
modifiedHahn–Banach separation theorema701472eb3f4
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.NormedSpace.HahnBanach.Separation | Mathlib.Analysis.LocallyConvex.Separation |
modifiedDual of a direct sum046704dd7cba
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Dual space","snippet":"is isomorphic to the direct sum of the duals of"},{"type":"math_alttext","value":"{\\displaystyle M^{\\bot }=\\{x'\\in X\\mid x'(m)=0{\\text{ for all }}m\\in M\\}.}"}] | — |
modifiedWeak topology15b87b3dcbff
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.LocallyConvex.WeakSpace | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedNorm-continuous maps are weakly continuousc9c42fffb2b6
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.LocallyConvex.WeakSpace | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedWeak* topologyffb1959b63f5
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.WeakDual | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedDual of ℓ¹d10318465a11
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Examples of dual spaces","snippet":"for every bounded linear functional"},{"type":"math_alttext","value":"{\\displaystyle f(x)=\\sum _{n\\in \\mathbb {N} }x_{n}y_{n},\\qquad x=\\{x_{n}\\}\\in c_{0},\\ \\ {\\text{and}}\\ \\ \\|f\\|_{(c_{0})'}=\\|y\\|_{\\ell _{1}}.}"}] | — |
modifiedMaximal ideals as Dirac measuresc0f1b2195833
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Examples of dual spaces","snippet":"the maximal ideals are precisely kernels of Dirac measures"},{"type":"math_alttext","value":"{\\displaystyle I_{x}=\\ker \\delta _{x}=\\{f\\in C(K)\\mid f(x)=0\\},\\quad x\\in K.}"}] | — |
modifiedBidual (second dual)76958b8115d0
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Bidual","snippet":"is called the bidual or second dual"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{cases}F_{X}\\colon X\\to X''\\\\F_{X}(x)(f)=f(x)&{\\text{ for all }}x\\in X,{\\text{ and for all }}f\\in X'\\end{cases}}}"}] | — |
modifiedGoldstine theorem76f691be86ed
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Bidual","snippet":"The Goldstine theorem states that the unit ball of a normed space is weakly*-dense"},{"type":"math_alttext","value":"{\\displaystyle \\sup _{i\\in I}\\|x_{i}\\|\\leq \\|x''\\|,\\ \\ x''(f)=\\lim _{i}f(x_{i}),\\quad f\\in X'.}"}] | — |
modifiedReflexive normed space719bc9426f62
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Reflexivity","snippet":"is called reflexive when the natural map"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{cases}F_{X}:X\\to X''\\\\F_{X}(x)(f)=f(x)&{\\text{ for all }}x\\in X,{\\text{ and for all }}f\\in X'\\end{cases}}}"}] | — |
modifiedReflexive normed spaces are Banach spacesba1fcea43035
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Reflexivity","snippet":"Reflexive normed spaces are Banach spaces."},{"type":"math_alttext","value":"{\\displaystyle {\\begin{cases}F_{X}:X\\to X''\\\\F_{X}(x)(f)=f(x)&{\\text{ for all }}x\\in X,{\\text{ and for all }}f\\in X'\\end{cases}}}"}] | — |
modifiedWeakly convergent sequence6903f96e748d
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.LocallyConvex.WeakSpace | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedWeakly Cauchy sequence728426826c2a
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.LocallyConvex.WeakSpace | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedWeakly* convergent sequence44fa3da3a153
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.WeakDual | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedWeakly sequentially complete spacedba381ed766e
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.LocallyConvex.WeakSpace | Mathlib.Topology.Algebra.Module.Spaces.WeakDual |
modifiedSchauder basis5869f1e05ad7
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Schauder bases","snippet":"A Schauder basis in a Banach space"},{"type":"math_alttext","value":"{\\displaystyle x=\\sum _{n=0}^{\\infty }x_{n}e_{n},\\quad {\\textit {i.e.,}}\\quad x=\\lim _{n}P_{n}(x),\\ P_{n}(x):=\\sum _{k=0}^{n}x_{k}e_{k}.}"}] | — |
modifiedTensor product and universal property1bef54bb4f97
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |
modifiedSimple tensor5f7b07f5db6a
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.TensorProduct.Basic | Mathlib.LinearAlgebra.TensorProduct.Defs |
modifiedInjectivity criterion and approximation property353ddc3385e6
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Tensor products and the approximation property","snippet":"is one-to-one if and only if"},{"type":"math_alttext","value":"{\\displaystyle Y{\\widehat {\\otimes }}_{\\pi }X\\to Y{\\widehat {\\otimes }}_{\\varepsilon }X}"},{"type":"math_alttext","value":"{\\displaystyle X'{\\widehat {\\otimes }}_{\\pi }X\\ \\longrightarrow X'{\\widehat {\\otimes }}_{\\varepsilon }X}"}] | — |
modifiedPolarization identity recovers inner product91895b80b8d7
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Characterizations of Hilbert space among Banach spaces","snippet":"the associated inner product is given by the polarization identity"},{"type":"math_alttext","value":"{\\displaystyle \\langle x,y\\rangle ={\\tfrac {1}{4}}(\\|x+y\\|^{2}-\\|x-y\\|^{2}).}"}] | — |
modifiedKwapień's theorem2a174a69c9f1
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Characterizations of Hilbert space among Banach spaces","snippet":"Kwapień proved that if"},{"type":"math_alttext","value":"{\\displaystyle c^{-2}\\sum _{k=1}^{n}\\|x_{k}\\|^{2}\\leq \\operatorname {Ave} _{\\pm }\\left\\|\\sum _{k=1}^{n}\\pm x_{k}\\right\\|^{2}\\leq c^{2}\\sum _{k=1}^{n}\\|x_{k}\\|^{2}}"}] | — |
modifiedFinite-dimensional homeomorphism classification43a1525ca8ad
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Module.FiniteDimension | Mathlib.Topology.Algebra.Module.FiniteDimension |
modifiedCountable compacta as ordinal intervals576f8d46f3cc
| Field | From #2525 | To #3141 |
|---|
| anchors | [{"section":"Spaces of continuous functions","snippet":"is homeomorphic to some closed interval of ordinal numbers"},{"type":"math_alttext","value":"{\\displaystyle \\langle 1,\\alpha \\rangle =\\{\\gamma \\mid 1\\leq \\gamma \\leq \\alpha \\}}"},{"type":"math_alttext","value":"{\\displaystyle C(\\langle 1,\\omega \\rangle ),\\ C(\\langle 1,\\omega ^{\\omega }\\rangle ),\\ C(\\langle 1,\\omega ^{\\omega ^{2}}\\rangle ),\\ C(\\langle 1,\\omega ^{\\omega ^{3}}\\rangle ),\\cdots ,C(\\langle 1,\\omega ^{\\omega ^{\\omega }}\\rangle ),\\cdots }"}] | — |
modifiedFréchet derivative on Banach spaces9edad3709514
| Field | From #2525 | To #3141 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.FDeriv.Basic | Mathlib.Analysis.Calculus.FDeriv.Defs |
addedGateaux derivative358e89ed8299