Normalized finite-dimensional Hilbert spaces

Theorem 2.1 uses the uniform probability inner product, rather than the counting inner product on Euclidean space. This file transfers mathlib's Bessel inequality and Gram–Schmidt theorem through the explicit normalization by √|Ω|.

noncomputable def Chvatal.uniformInner {Ω : Type u_1} [Fintype Ω] (f g : Ω → ℝ) : ℝ

The uniform probability inner product in Section 2, generalized to any nonempty finite sample space.

Equations

• Chvatal.uniformInner f g = (∑ x : Ω, f x * g x) / ↑(Fintype.card Ω)

noncomputable def Chvatal.uniformEuclidean {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] : (Ω → ℝ) ≃ₗ[ℝ] EuclideanSpace ℝ Ω

The normalization which identifies the paper's probability inner product with mathlib's Euclidean inner product.

Equations

• Chvatal.uniformEuclidean = (LinearEquiv.smulOfNeZero ℝ (Ω → ℝ) (√↑(Fintype.card Ω))⁻¹ ⋯).trans (WithLp.linearEquiv 2 ℝ (Ω → ℝ)).symm

@[simp]

theorem Chvatal.uniformEuclidean_apply {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] (f : Ω → ℝ) (x : Ω) : (uniformEuclidean f).ofLp x = (√↑(Fintype.card Ω))⁻¹ * f x

Coordinate formula for the normalization used in Theorem 2.1.

theorem Chvatal.inner_uniformEuclidean {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] (f g : Ω → ℝ) : inner ℝ (uniformEuclidean f) (uniformEuclidean g) = uniformInner f g

The normalization preserves exactly the probability inner product of Section 2.

def Chvatal.UniformOrthonormal {Ω : Type u_1} [Fintype Ω] {κ : Type u_2} (u : κ → Ω → ℝ) : Prop

Orthonormality with respect to uniform probability, as in Theorem 2.1 and Corollary 3.2. The index type may be empty.

Equations

• Chvatal.UniformOrthonormal u = ∀ (i j : κ), Chvatal.uniformInner (u i) (u j) = if i = j then 1 else 0

theorem Chvatal.uniformOrthonormal_iff {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {κ : Type u_2} (u : κ → Ω → ℝ) : UniformOrthonormal u ↔ Orthonormal ℝ fun (i : κ) => uniformEuclidean (u i)

Uniform orthonormality is ordinary orthonormality after normalization.

theorem Chvatal.bessel_inequality {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {κ : Type u_2} [Fintype κ] (u : κ → Ω → ℝ) (hu : UniformOrthonormal u) (h : Ω → ℝ) : ∑ i : κ, uniformInner (u i) h ^ 2 ≤ uniformInner h h

Theorem 2.1 (Bessel's inequality), with the paper's normalized inner product.

theorem Chvatal.exists_uniformOrthonormal_in_submodule {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {κ : Type u_2} [Finite κ] (W : Submodule ℝ (Ω → ℝ)) (f : κ → Ω → ℝ) (hli : LinearIndependent ℝ f) (hf : ∀ (i : κ), f i ∈ W) : ∃ (u : κ → Ω → ℝ), UniformOrthonormal u ∧ ∀ (i : κ), u i ∈ W

The linear algebra step in Corollary 3.2: a finite independent family contained in a subspace can be orthonormalized inside that same subspace. Thus simultaneous physical and Fourier support restrictions, which define subspaces, are preserved.