English
The space lp G 2 is equipped with the inner product ⟪f,g⟫ = ∑' i ⟪f(i), g(i)⟫, making it a real/complex Hilbert space depending on 𝕜.
Русский
Пространство lp G 2 оснащено внут. произведением ⟪f,g⟫ = ∑' i ⟪f(i), g(i)⟫, образуя гильбертово пространство (в зависимости от 𝕜).
LaTeX
$$$ \\langle f,g \\rangle = \\sum\\_' i \\langle f(i), g(i) \\rangle $$$
Lean4
instance instInnerProductSpace : InnerProductSpace 𝕜 (lp G 2) :=
{
lp.normedAddCommGroup (E := G) (p :=
2) with
inner := fun f g => ∑' i, ⟪f i, g i⟫
norm_sq_eq_re_inner := fun f =>
by
calc
‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
_ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := (lp.norm_rpow_eq_tsum ?_ f)
_ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
_ = ∑' i, re ⟪f i, f i⟫ := by simp [norm_sq_eq_re_inner (𝕜 := 𝕜)]
_ = re (∑' i, ⟪f i, f i⟫) := (RCLike.reCLM.map_tsum ?_).symm
· norm_num
· exact summable_inner f f
conj_inner_symm := fun f g => by
calc
conj _ = conj (∑' i, ⟪g i, f i⟫) := by congr
_ = ∑' i, conj ⟪g i, f i⟫ := RCLike.conjCLE.map_tsum
_ = ∑' i, ⟪f i, g i⟫ := by simp only [inner_conj_symm]
_ = _ := by congr
add_left := fun f₁ f₂ g =>
by
calc
_ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
_ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by simp only [inner_add_left, Pi.add_apply, coeFn_add]
_ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := (Summable.tsum_add ?_ ?_)
_ = _ := by congr
· congr
· exact summable_inner f₁ g
· exact summable_inner f₂ g
smul_left := fun f g c =>
by
calc
_ = ∑' i, ⟪c • f i, g i⟫ := ?_
_ = ∑' i, conj c * ⟪f i, g i⟫ := by simp only [inner_smul_left]
_ = conj c * ∑' i, ⟪f i, g i⟫ := tsum_mul_left
_ = _ := ?_
· simp only [coeFn_smul, Pi.smul_apply]
· congr }