English
If the marginals of f and g over s are equal, then their global integrals against the product measure agree: ∫ (π μ) f = ∫ (π μ) g.
Русский
Если маргиналы функций f и g по s совпадают, то их глобальные интегралы по произведению меры совпадают.
LaTeX
$$$\\text{lmarginal}_{μ} s f = \\text{lmarginal}_{μ} s g \\Rightarrow \\int⁻ f d( Measure.pi μ) = \\int⁻ g d( Measure.pi μ)$$$
Lean4
theorem lintegral_mul_le_one_of_lintegral_rpow_eq_one {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ≥0∞}
(hf : AEMeasurable f μ) (hf_norm : ∫⁻ a, f a ^ p ∂μ = 1) (hg_norm : ∫⁻ a, g a ^ q ∂μ = 1) :
(∫⁻ a, (f * g) a ∂μ) ≤ 1 := by
calc
(∫⁻ a : α, (f * g) a ∂μ) ≤ ∫⁻ a : α, f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ :=
lintegral_mono fun a => young_inequality (f a) (g a) hpq
_ = 1 := by
simp only [div_eq_mul_inv]
rw [lintegral_add_left']
· rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm, one_mul, one_mul,
hpq.inv_add_inv_ennreal]
simp [hpq.symm.pos]
· exact (hf.pow_const _).mul_const _
