Lean4
theorem lintegral_Lp_mul_le_Lq_mul_Lr {α} [MeasurableSpace α] {p q r : ℝ} (hp0_lt : 0 < p) (hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r) (μ : Measure α) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
(∫⁻ a, (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ a, f a ^ q ∂μ) ^ (1 / q) * (∫⁻ a, g a ^ r ∂μ) ^ (1 / r) :=
by
have hp0_ne : p ≠ 0 := (ne_of_lt hp0_lt).symm
have hp0 : 0 ≤ p := le_of_lt hp0_lt
have hq0_lt : 0 < q := lt_of_le_of_lt hp0 hpq
have hq0_ne : q ≠ 0 := (ne_of_lt hq0_lt).symm
have h_one_div_r : 1 / r = 1 / p - 1 / q := by rw [hpqr]; simp
let p2 := q / p
let q2 := p2.conjExponent
have hp2q2 : p2.HolderConjugate q2 := .conjExponent (by simp [p2, _root_.lt_div_iff₀, hpq, hp0_lt])
calc
(∫⁻ a : α, (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ a : α, f a ^ p * g a ^ p ∂μ) ^ (1 / p) := by
simp_rw [Pi.mul_apply, ENNReal.mul_rpow_of_nonneg _ _ hp0]
_ ≤ ((∫⁻ a, f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ a, g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) :=
by
gcongr
simp_rw [ENNReal.rpow_mul]
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)
_ = (∫⁻ a : α, f a ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) :=
by
rw [@ENNReal.mul_rpow_of_nonneg _ _ (1 / p) (by simp [hp0]), ← ENNReal.rpow_mul, ← ENNReal.rpow_mul]
have hpp2 : p * p2 = q := by
symm
rw [mul_comm, ← div_eq_iff hp0_ne]
have hpq2 : p * q2 = r := by
rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
simp [field, p2, q2, Real.conjExponent]
simp_rw [div_mul_div_comm, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2]
