Theorems · Theorem · functional analysis

lp.norm_le_of_forall_sum_le

∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal →
    ∀ {C : ℝ}, 0 ≤ C → ∀ {f : ↥(lp E p)}, (∀ (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal) → ‖f‖ ≤ C

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

2 results in Mathlib

Foundations

Depth 220 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup