Theorems · Theorem · functional analysis

lp.tsum_mul_le_mul_norm

∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal},
  p.toReal.HolderConjugate q.toReal →
    ∀ (f : ↥(lp E p)) (g : ↥(lp E q)), (Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

Hölder inequality

Defined in: Mathlib.Analysis.Normed.Lp.lpSpace
Cited by: 2 results in Mathlib
Foundations: Depth 219 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
ENNRealstatement and proof · cited by 9,879
Norm.normstatement and proof · cited by 5,413
AddSubgroupstatement · cited by 3,232
SummationFilter.unconditionalstatement and proof · cited by 2,068
tsumstatement · cited by 1,148
ENNReal.toRealstatement and proof · cited by 859
Summablestatement · cited by 778
norm_nonnegproof · cited by 725
HasSumproof · cited by 518
PreLpstatement and proof · cited by 163

Cited by2

Results whose statement or proof uses this declaration.

lp.summable_mulproof · cited by 1
lp.tsum_mul_le_mul_norm'proof · cited by 0