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].

Equations

• ⟪f, g⟫_[𝕜, w] = ∑ 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, denoted as ⟪g, f⟫_[𝕜, w].

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) : ⟪f, g⟫ₙ_[𝕜] = (↑(Fintype.card ι))⁻¹ • ⟪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 𝕜) ⟪f, g⟫_[𝕜, w] = ⟪g, f⟫_[𝕜, w]

@[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) : ⟪0, g⟫_[𝕜, w] = 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) : ⟪f, 0⟫_[𝕜, w] = 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) : ⟪f₁ + f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + ⟪f₂, g⟫_[𝕜, w]

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) : ⟪f, g₁ + g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] + ⟪f, g₂⟫_[𝕜, w]

@[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) : ⟪-f, g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w]

@[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) : ⟪f, -g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w]

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) : ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w]

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) : ⟪f, g₁ - g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] - ⟪f, g₂⟫_[𝕜, w]

@[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) : ⟪f, g⟫_[𝕜, w] = 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) : ⟪c • f, g⟫_[𝕜, w] = star c • ⟪f, g⟫_[𝕜, w]

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) : ⟪f, c • g⟫_[𝕜, w] = c • ⟪f, g⟫_[𝕜, w]

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 * ⟪f, g⟫_[𝕜, w] = ⟪star c • f, g⟫_[𝕜, w]

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) : ⟪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) : ⟪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 : ι → 𝕜) : ⟪Function.const ι a, f⟫_[𝕜, w] = (∑ i : ι, w i • f i) * (starRingEnd 𝕜) a

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

@[simp]

theorem RCLike.wInner_one_const_left {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] (a : 𝕜) (f : ι → 𝕜) : ⟪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 : 𝕜) : ⟪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 : ι → 𝕜) : ⟪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 : 𝕜) : ⟪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 : ι → 𝕜) : ⟪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 = ⟪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₂ : κ) => ⟪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₂ : κ) => ⟪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 ≤ ⟪f, g⟫_[𝕜, w]

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

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