Pointwise bounds for infinite sums in Lᵖ #
If a family u in Lᵖ has sum v in the Lᵖ norm, then ‖v x‖ₑ ≤ ∑' i, ‖u i x‖ₑ at almost
every point. Unlike MeasureTheory.Lp.hasSum_coeFn_tsum, this needs neither a countable index
type nor summability of the norms ‖u i‖: it only uses that some sequence of finite partial sums
converges to v almost everywhere. A typical use is a sum of functions with disjoint supports in
L², whose norms are square-summable but need not be summable.
Main declarations #
MeasureTheory.Lp.ae_enorm_le_tsum_enorm_of_hasSum: the pointwise bound.
theorem
MeasureTheory.Lp.ae_enorm_le_tsum_enorm_of_hasSum
{α : Type u_1}
{E : Type u_2}
{κ : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup E]
{p : ENNReal}
[Fact (1 ≤ p)]
{u : κ → ↥(Lp E p μ)}
{v : ↥(Lp E p μ)}
(h : HasSum u v)
:
If a family u in Lᵖ has sum v, then at almost every point the extended norm of v is at
most the sum of the extended norms of the u i.