Hilbert spaces

TheoremHilbert projection theorem#

Existence of minimizers, aka the Hilbert projection theorem.

Let u be a point in a real inner product space, and let K be a nonempty complete convex subset. Then there exists a \(unique\) v in K that minimizes the distance ‖u - v‖ to u.

exists_norm_eq_iInf_of_complete_convex.{u_3} {F : Type u_3} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] {K : Set F} (ne : K.Nonempty) (h₁ : IsComplete K) (h₂ : Convex ℝ K)
  (u : F) : ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
Sources
Mathlibexists_norm_eq_iInf_of_complete_convex
Uses 11
Statement usesConvex subsets · Inner product space, over \(R\) or \(C\)
Proof usesCharacteristic zero · Continuity of monotone functions · Field \(\Q\) of rational numbers · Hausdorff space · Limits of sequences · Metric structure · Squeeze theorem · Topological module · Topological ring

InstanceInner product space \(l^2\)#

Mathlib states this as lp.instInnerProductSpace.

lp.instInnerProductSpace.{u_1, u_2, u_4} {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {G : ι → Type u_4}
  [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace 𝕜 (G i)] :
  InnerProductSpace 𝕜 ↥(lp G 2)
Sources
Mathliblp.instInnerProductSpace
Uses 2
Statement usesInfinite sum · Inner product space, over \(R\) or \(C\)

TheoremCompleteness of \(l^2\)#

Mathlib states this as lp.completeSpace.

lp.completeSpace.{u_3, u_4} {α : Type u_3} {E : α → Type u_4} {p : ENNReal}
  [(i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)] [∀ (a : α), CompleteSpace (E a)] :
  CompleteSpace ↥(lp E p)
Sources
Mathliblp.completeSpace
Uses 11 · Used by 2
Statement usesCompleteness · Infinite sum · Metric space
Proof usesCharacteristic zero · Complete metric spaces · Field \(\R\) of real numbers · Lipschitz continuity · Order topology · Ordered ring · Pointwise convergence · Topological ring
Used byFourier Series · Existence of Hilbert basis

InstanceInner product space \(L^2\)#

Mathlib states this as MeasureTheory.L2.innerProductSpace.

MeasureTheory.L2.innerProductSpace.{u_1, u_2, u_4} {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4}
  [RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 ↥(MeasureTheory.Lp E 2 μ)
Sources
MathlibMeasureTheory.L2.innerProductSpace
Uses 2 · Used by 2
Statement uses\(L^p\) space · Inner product space, over \(R\) or \(C\)
Used byConditional expectation · Example, the Hilbert basis of trigonometric polynomials

TheoremCompleteness of \(L^2\)#

Lp is complete for 1 ≤ p.

MeasureTheory.Lp.instCompleteSpace.{u_1, u_3} {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E]
  [hp : Fact (1 ≤ p)] : CompleteSpace ↥(MeasureTheory.Lp E p μ)
Sources
MathlibMeasureTheory.Lp.instCompleteSpace
Uses 13 · Used by 1
Statement uses\(L^p\) space · Completeness
Proof usesBorel sigma-algebra · Characteristic zero · Closure · Cluster point · Completeness of R · Hausdorff space · Measurable function · Metric structure · Order topology · Pointwise convergence · Topological ring
Used byFourier Series

StructureHilbert bases#

A Hilbert basis on ι for an inner product space E is an identification of E with the lp space ℓ²(ι, 𝕜).

HilbertBasis.{u_1, u_2, u_3} (ι : Type u_1) (𝕜 : Type u_2) [RCLike 𝕜] (E : Type u_3)
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Type (max (max u_1 u_2) u_3)
Sources
MathlibHilbertBasis
Uses 3 · Used by 2
Statement usesInfinite sum · Inner product space, over \(R\) or \(C\) · Linear map
Used byExistence of Hilbert basis · Example, the Hilbert basis of trigonometric polynomials

DefinitionExample, the Hilbert basis of trigonometric polynomials#

We define fourierBasis to be a ℤ-indexed Hilbert basis for Lp ℂ 2 haarAddCircle, which by definition is an isometric isomorphism from Lp ℂ 2 haarAddCircle to ℓ²(ℤ, ℂ).

fourierBasis {T : ℝ} [hT : Fact (0 < T)] :
  HilbertBasis ℤ ℂ ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)
Sources
MathlibfourierBasis
Uses 12 · Used by 1
Statement usesBorel sigma-algebra · Carathéodory's theorem (measure theory) · Closure · Compact open topology · Cos (extension of trigonometric functions to the complex plane) · Generating sets · Hilbert bases · Homeomorphisms · Inner product space \(L^2\) · Lipschitz continuity · Norm of a continuous linear map · Range of a linear map
Used byFourier Series

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.