theorem MemLp.toLp_sum {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_3} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) : MeasureTheory.MemLp.toLp (∑ i ∈ s, f i) ⋯ = ∑ i : ↥s, MeasureTheory.MemLp.toLp (f ↑i) ⋯

theorem MeasureTheory.one_le_LpAddConst {p : ENNReal} : 1 ≤ p.LpAddConst