English
The operator norm of the map toLp is equal to the operator norm of the Lp-map for bounded continuous functions, reflecting compatibility of two realizations.
Русский
Нормa оператора отображения в Lp равна норме соответствующего отображения в Lp для ограниченно непрерывных функций; это отражает совместимость реализаций.
LaTeX
$$$\|toLp(p μ 𝕜)\| = \|BoundedContinuousFunction.toLp(p μ 𝕜)\|$$$
Lean4
/-- If a sum of continuous functions `g n` is convergent, and the same sum converges in `Lᵖ` to `h`,
then in fact `g n` converges uniformly to `h`. -/
theorem hasSum_of_hasSum_Lp {β : Type*} [μ.IsOpenPosMeasure] {g : β → C(α, E)} {f : C(α, E)} (hg : Summable g)
(hg2 : HasSum (toLp (E := E) p μ 𝕜 ∘ g) (toLp (E := E) p μ 𝕜 f)) : HasSum g f :=
by
convert Summable.hasSum hg
exact toLp_injective μ (hg2.unique ((toLp p μ 𝕜).hasSum <| Summable.hasSum hg))
