case h.e'_6
α : Type u_2
E : Type u_4
F : Type ?u.15733246
G : Type ?u.15733249
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
β : Type u_1
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (↑(toLp p μ 𝕜) ∘ g) (↑(toLp p μ 𝕜) f)
⊢ f = ∑' (b : β), g b
α : Type u_2
E : Type u_4
F : Type ?u.15733246
G : Type ?u.15733249
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
β : Type u_1
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (↑(toLp p μ 𝕜) ∘ g) (↑(toLp p μ 𝕜) f)
⊢ HasSum g f
convert Summable.hasSum hg
no goals
case h.e'_6
α : Type u_2
E : Type u_4
F : Type ?u.15733246
G : Type ?u.15733249
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
β : Type u_1
inst✝² : Measure.IsOpenPosMeasure μ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (↑(toLp p μ 𝕜) ∘ g) (↑(toLp p μ 𝕜) f)
⊢ f = ∑' (b : β), g b
exact toLp_injective μ (hg2.unique ((toLp p μ 𝕜).hasSum <| Summable.hasSum hg))