English
Under Holder conjugacy hpq, for f ∈ lp E p and g ∈ lp E q, the series ∑ ‖f_i‖·‖g_i‖ is summable and bounded by ‖f‖·‖g‖.
Русский
При паре Холдера hpq, для f ∈ lp E p и g ∈ lp E q, серия ∑ ‖f_i‖·‖g_i‖ сходится и ее сумма не превосходит ‖f‖·‖g‖.
LaTeX
$$$$ \left( \sum_i \|f_i\| \cdot \|g_i\| \right) \le \|f\| \cdot \|g\|, \quad \text{при условии } p^{\mathrm{toReal}} \text{ и } q^{\mathrm{toReal}} \явHolderConjugate. $$$$
Lean4
/-- Hölder inequality -/
protected theorem tsum_mul_le_mul_norm {p q : ℝ≥0∞} (hpq : 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‖ :=
by
have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _
have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _
have hf₂ := lp.hasSum_norm hpq.pos f
have hg₂ := lp.hasSum_norm hpq.symm.pos g
obtain ⟨C, -, hC', hC⟩ :=
Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg hpq (norm_nonneg' _) (norm_nonneg' _) hf₁ hg₁ hf₂ hg₂
rw [← hC.tsum_eq] at hC'
exact ⟨hC.summable, hC'⟩
