inner_le_weight_mul_Lp_of_nonneg — Mathlib

English

Hölder inequality for real-valued functions with weights, using abs in the Lp-norms.

Русский

Неравенство Хольдера для вещественных функций с весами с модулем внутри норм Lp.

LaTeX

$$$\sum_{i\in s} w_i f_i \le \left(\sum_{i\in s} w_i\right)^{1-\frac{1}{p}} \left(\sum_{i\in s} w_i |f_i|^p\right)^{\frac{1}{p}}$$$

Lean4

/-- **Weighted Hölder inequality**. -/
theorem inner_le_weight_mul_Lp_of_nonneg (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hf : ∀ i, 0 ≤ f i) : ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ :=
  by
  lift w to ι → ℝ≥0 using hw
  lift f to ι → ℝ≥0 using hf
  beta_reduce  at *
  norm_cast at *
  exact NNReal.inner_le_weight_mul_Lp _ hp _ _

Похожие утверждения