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.

Equations

• RCLike.wInner w f g = ∑ i : ι, w i • inner (f i) (g i)

@[reducible, inline]

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

The weight function making wInner into the compact inner product.

Equations

• RCLike.cWeight = Function.const ι (↑(Fintype.card ι))⁻¹

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

Weighted inner product giving rise to the L2 norm.

Equations

• One or more equations did not get rendered due to their size.

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

Discrete inner product giving rise to the discrete L2 norm.

Equations

• One or more equations did not get rendered due to their size.

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

Compact inner product giving rise to the compact L2 norm.

Equations

• One or more equations did not get rendered due to their size.

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) : RCLike.wInner RCLike.cWeight f g = (↑(Fintype.card ι))⁻¹ • RCLike.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 𝕜) (RCLike.wInner w f g) = RCLike.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) : RCLike.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) : RCLike.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) : RCLike.wInner w (f₁ + f₂) g = RCLike.wInner w f₁ g + RCLike.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) : RCLike.wInner w f (g₁ + g₂) = RCLike.wInner w f g₁ + RCLike.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) : RCLike.wInner w (-f) g = -RCLike.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) : RCLike.wInner w f (-g) = -RCLike.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) : RCLike.wInner w (f₁ - f₂) g = RCLike.wInner w f₁ g - RCLike.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) : RCLike.wInner w f (g₁ - g₂) = RCLike.wInner w f g₁ - RCLike.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) : RCLike.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) : RCLike.wInner w (c • f) g = star c • RCLike.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 𝕝 𝕜] [SMulCommClass ℝ 𝕝 𝕜] [(i : ι) → Module 𝕝 (E i)] [∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : (i : ι) → E i) : RCLike.wInner w f (c • g) = c • RCLike.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 * RCLike.wInner w f g = RCLike.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) : RCLike.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) : RCLike.wInner RCLike.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 : ι → 𝕜) : RCLike.wInner w (Function.const ι a) f = (starRingEnd 𝕜) a * ∑ i : ι, w i • f i

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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₂ : κ) => RCLike.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₂ : κ) => RCLike.wInner RCLike.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 ≤ RCLike.wInner w f g

theorem RCLike.norm_wInner_le {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {w : ι → ℝ} {f g : ι → 𝕜} (hw : 0 ≤ w) : ‖RCLike.wInner w f g‖ ≤ RCLike.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) : |RCLike.wInner w f g| ≤ RCLike.wInner w |f| |g|