ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ HasSum (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) (inner a (↑f i))
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ inner (lp.single 2 i a) f = inner a (↑f i)
refine' (hasSum_inner (lp.single 2 i a) f).unique _
case h.e'_5
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) = fun b' => if b' = i then inner a (↑f i) else 0
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ HasSum (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) (inner a (↑f i))
convert hasSum_ite_eq i ⟪a, f i⟫ using 1
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
⊢ inner (↑(lp.single 2 i a) j) (↑f j) = if j = i then inner a (↑f i) else 0
case h.e'_5
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
⊢ (fun i_1 => inner (↑(lp.single 2 i a) i_1) (↑f i_1)) = fun b' => if b' = i then inner a (↑f i) else 0
ext j
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
⊢ inner (if h : j = i then (_ : i = j) ▸ a else 0) (↑f j) = if j = i then inner a (↑f i) else 0
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
⊢ inner (↑(lp.single 2 i a) j) (↑f j) = if j = i then inner a (↑f i) else 0
rw [lp.single_apply]
case h.e'_5.h.inl
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
h : j = i
⊢ inner ((_ : i = j) ▸ a) (↑f j) = inner a (↑f i)

case h.e'_5.h.inr
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
h : ¬j = i
⊢ inner 0 (↑f j) = 0
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
⊢ inner (if h : j = i then (_ : i = j) ▸ a else 0) (↑f j) = if j = i then inner a (↑f i) else 0
split_ifs with h
case h.e'_5.h.inl
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f : { x // x ∈ lp G 2 }
j : ι
a : G j
⊢ inner ((_ : j = j) ▸ a) (↑f j) = inner a (↑f j)
case h.e'_5.h.inl
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
h : j = i
⊢ inner ((_ : i = j) ▸ a) (↑f j) = inner a (↑f i)
subst h
no goals
case h.e'_5.h.inl
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f : { x // x ∈ lp G 2 }
j : ι
a : G j
⊢ inner ((_ : j = j) ▸ a) (↑f j) = inner a (↑f j)
rfl
no goals
case h.e'_5.h.inr
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.302267
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
i : ι
a : G i
f : { x // x ∈ lp G 2 }
j : ι
h : ¬j = i
⊢ inner 0 (↑f j) = 0
simp