English
Hölder inequality with many factors: for a finite set s and measurable functions f_i: X→ℝ≥0∞ with exponents p_i summing to 1, the integral of the product ∏ f_i^{p_i} is bounded by ∏ (∫ f_i dμ)^{p_i}.
Русский
Неравенство Хольдера для множества функций: для конечного множества i, функций f_i с p_i≥0, сумма p_i = 1, получаем: ∫ ∏ f_i^{p_i} ≤ ∏ (∫ f_i)^{p_i}.
LaTeX
$$$\\forall s\\subseteq\\iota,\\; f_i:\\iota\\to X\\to\\mathbb{R}_{\\ge 0}^{∞},\\; (hf:\\forall i\\in s, AEMeasurable f_i μ),\\; p_i: s→\\mathbb{R},\\; \\sum_{i\\in s} p_i = 1,\\; p_i \\ge 0\\,\\Rightarrow \\\\ \\int \\prod_{i\\in s} f_i^{p_i} dμ ≤ \\prod_{i\\in s} (\\int f_i dμ)^{p_i}$$$
Lean4
/-- A different formulation of Hölder's inequality for two functions, with two exponents that sum to
1, instead of reciprocals of -/
theorem lintegral_mul_norm_pow_le {α} [MeasurableSpace α] {μ : Measure α} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
(hg : AEMeasurable g μ) {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) :
∫⁻ a, f a ^ p * g a ^ q ∂μ ≤ (∫⁻ a, f a ∂μ) ^ p * (∫⁻ a, g a ∂μ) ^ q :=
by
rcases hp.eq_or_lt with rfl | hp
· rw [zero_add] at hpq
simp [hpq]
rcases hq.eq_or_lt with rfl | hq
· rw [add_zero] at hpq
simp [hpq]
have h2p : 1 < 1 / p := by
rw [one_div, one_lt_inv₀ hp]
linarith
have h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1 := by simp [hpq]
have :=
ENNReal.lintegral_mul_le_Lp_mul_Lq μ (Real.holderConjugate_iff.mpr ⟨h2p, h2pq⟩) (hf.pow_const p) (hg.pow_const q)
simpa [← ENNReal.rpow_mul, hp.ne', hq.ne'] using this
