English
Weighted Minkowski inequality in terms of Expectation; the expectation of the sum is bounded by sum of expectations.
Русский
Сжатое неравенство Минковского в терминах ожидания: математическое ожидание суммы не превышает сумму ожиданий.
LaTeX
$$$\mathbb{E}_{i\in s}[w_i f_i + w_i g_i] \le \mathbb{E}_{i\in s}[w_i]^{1-1/p} \mathbb{E}_{i\in s}[w_i f_i^p]^{1/p} + \cdots$$$
Lean4
/-- **Weighted Hölder inequality** in terms of `Finset.expect`. -/
theorem compact_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
simp_rw [expect_eq_sum_div_card]
rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]
· gcongr
exact inner_le_weight_mul_Lp_of_nonneg s hp _ _ hw hf
any_goals simp
· exact sum_nonneg fun i _ ↦ by have := hw i; have := hf i; positivity
· exact sum_nonneg fun i _ ↦ by have := hw i; positivity
