L2 inner product of finite sequences

This file defines the weighted L2 inner product of functions f g : ι → R where ι is a fintype as ∑ i, conj (f i) * g i. This convention (conjugation on the left) matches the inner product coming from RCLike.innerProductSpace.

TODO

• Build a non-instance InnerProductSpace from wInner.
• cWeight is a poor name. Can we find better? It doesn't hugely matter for typing, since it's hidden behind the ⟪f, g⟫ₙ_[𝕝] notation, but it does show up in lemma names ⟪f, g⟫_[𝕝, cWeight] is called wInner_cWeight. Maybe we should introduce some naming convention, similarly to MeasureTheory.average?

def RCLike.wInner {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g : (i : ι) → E i) : 𝕜

Weighted inner product giving rise to the L2 norm, denoted as ⟪g, f⟫_[𝕜, w].

@[reducible, inline]

noncomputable abbrev RCLike.cWeight {ι : Type u_1} [Fintype ι] : ι → ℝ

The weight function making wInner into the compact inner product.

def RCLike.«term⟪_,_⟫_[_,_]» : Lean.ParserDescr

Weighted inner product giving rise to the L2 norm, denoted as ⟪g, f⟫_[𝕜, w].

def RCLike.«term⟪_,_⟫_[_]» : Lean.ParserDescr

Discrete inner product giving rise to the discrete L2 norm.

def RCLike.«term⟪_,_⟫ₙ_[_]» : Lean.ParserDescr

Compact inner product giving rise to the compact L2 norm.

theorem RCLike.wInner_cWeight_eq_smul_wInner_one {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (f g : (i : ι) → E i) : wInner cWeight f g = (↑(Fintype.card ι))⁻¹ • wInner 1 f g

@[simp]

theorem RCLike.conj_wInner_symm {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g : (i : ι) → E i) : (starRingEnd 𝕜) (wInner w f g) = wInner w g f

@[simp]

theorem RCLike.wInner_zero_left {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (g : (i : ι) → E i) : wInner w 0 g = 0

@[simp]

theorem RCLike.wInner_zero_right {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f : (i : ι) → E i) : wInner w f 0 = 0

theorem RCLike.wInner_add_left {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f₁ f₂ g : (i : ι) → E i) : wInner w (f₁ + f₂) g = wInner w f₁ g + wInner w f₂ g

theorem RCLike.wInner_add_right {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g₁ g₂ : (i : ι) → E i) : wInner w f (g₁ + g₂) = wInner w f g₁ + wInner w f g₂

@[simp]

theorem RCLike.wInner_neg_left {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g : (i : ι) → E i) : wInner w (-f) g = -wInner w f g

@[simp]

theorem RCLike.wInner_neg_right {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g : (i : ι) → E i) : wInner w f (-g) = -wInner w f g

theorem RCLike.wInner_sub_left {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f₁ f₂ g : (i : ι) → E i) : wInner w (f₁ - f₂) g = wInner w f₁ g - wInner w f₂ g

theorem RCLike.wInner_sub_right {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ) (f g₁ g₂ : (i : ι) → E i) : wInner w f (g₁ - g₂) = wInner w f g₁ - wInner w f g₂

@[simp]

theorem RCLike.wInner_of_isEmpty {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] [IsEmpty ι] (w : ι → ℝ) (f g : (i : ι) → E i) : wInner w f g = 0

theorem RCLike.wInner_smul_left {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] {𝕝 : Type u_5} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜] [SMulCommClass ℝ 𝕝 𝕜] [(i : ι) → Module 𝕝 (E i)] [∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : (i : ι) → E i) : wInner w (c • f) g = star c • wInner w f g

theorem RCLike.wInner_smul_right {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] {𝕝 : Type u_5} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜] [(i : ι) → Module 𝕝 (E i)] [∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : (i : ι) → E i) : wInner w f (c • g) = c • wInner w f g

theorem RCLike.mul_wInner_left {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (c : 𝕜) (w : ι → ℝ) (f g : (i : ι) → E i) : c * wInner w f g = wInner w (star c • f) g

theorem RCLike.wInner_one_eq_sum {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (f g : (i : ι) → E i) : wInner 1 f g = ∑ i : ι, inner 𝕜 (f i) (g i)

theorem RCLike.wInner_cWeight_eq_expect {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [Fintype ι] [RCLike 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (f g : (i : ι) → E i) : wInner cWeight f g = Finset.univ.expect fun (i : ι) => inner 𝕜 (f i) (g i)

theorem RCLike.wInner_const_left {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {w : ι → ℝ} (a : 𝕜) (f : ι → 𝕜) : wInner w (Function.const ι a) f = (∑ i : ι, w i • f i) * (starRingEnd 𝕜) a

theorem RCLike.wInner_const_right {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {w : ι → ℝ} (f : ι → 𝕜) (a : 𝕜) : wInner w f (Function.const ι a) = a * ∑ i : ι, w i • (starRingEnd 𝕜) (f i)

@[simp]

theorem RCLike.wInner_one_const_left {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (a : 𝕜) (f : ι → 𝕜) : wInner 1 (Function.const ι a) f = (∑ i : ι, f i) * (starRingEnd 𝕜) a

@[simp]

theorem RCLike.wInner_one_const_right {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (f : ι → 𝕜) (a : 𝕜) : wInner 1 f (Function.const ι a) = a * ∑ i : ι, (starRingEnd 𝕜) (f i)

@[simp]

theorem RCLike.wInner_cWeight_const_left {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (a : 𝕜) (f : ι → 𝕜) : wInner cWeight (Function.const ι a) f = Finset.univ.expect fun (i : ι) => f i * (starRingEnd 𝕜) a

@[simp]

theorem RCLike.wInner_cWeight_const_right {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (f : ι → 𝕜) (a : 𝕜) : wInner cWeight f (Function.const ι a) = a * Finset.univ.expect fun (i : ι) => (starRingEnd 𝕜) (f i)

theorem RCLike.wInner_one_eq_inner {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (f g : ι → 𝕜) : wInner 1 f g = inner 𝕜 (WithLp.toLp 2 f) (WithLp.toLp 2 g)

theorem RCLike.inner_eq_wInner_one {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (f g : PiLp 2 fun (_i : ι) => 𝕜) : inner 𝕜 f g = wInner 1 f.ofLp g.ofLp

theorem RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero {ι : Type u_1} {κ : Type u_2} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {f : κ → ι → 𝕜} (hf : ∀ (k : κ), f k ≠ 0) (hinner : Pairwise fun (k₁ k₂ : κ) => wInner 1 (f k₁) (f k₂) = 0) : LinearIndependent 𝕜 f

theorem RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero {ι : Type u_1} {κ : Type u_2} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {f : κ → ι → 𝕜} (hf : ∀ (k : κ), f k ≠ 0) (hinner : Pairwise fun (k₁ k₂ : κ) => wInner cWeight (f k₁) (f k₂) = 0) : LinearIndependent 𝕜 f

theorem RCLike.wInner_nonneg {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {w : ι → ℝ} {f g : ι → 𝕜} (hw : 0 ≤ w) (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ wInner w f g

theorem RCLike.norm_wInner_le {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {w : ι → ℝ} {f g : ι → 𝕜} (hw : 0 ≤ w) : ‖wInner w f g‖ ≤ wInner w (fun (i : ι) => ‖f i‖) fun (i : ι) => ‖g i‖

theorem RCLike.abs_wInner_le {ι : Type u_1} [Fintype ι] {w f g : ι → ℝ} (hw : 0 ≤ w) : |wInner w f g| ≤ wInner w |f| |g|