English
The discrete grid-lines lemma asserts that the transformed quantity decreases when the index-set is enlarged; i.e., T is antitone with respect to the index set.
Русский
Лемма сеточных линий утверждает, что полученная величина уменьшается при увеличении набора индексов; T в порядке убывания по включению.
LaTeX
$$$T_{μ,p}(f,s) \\text{ is Antitone in } s$$$
Lean4
/-- Special case of the grid-lines lemma `lintegral_mul_prod_lintegral_pow_le`, taking the extremal
exponent `p = (#ι - 1)⁻¹`. -/
theorem lintegral_prod_lintegral_pow_le [Fintype ι] [∀ i, SigmaFinite (μ i)] {p : ℝ} (hp : Real.HolderConjugate (#ι) p)
{f} (hf : Measurable f) :
∫⁻ x, ∏ i, (∫⁻ xᵢ, f (update x i xᵢ) ∂μ i) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) ∂.pi μ ≤ (∫⁻ x, f x ∂.pi μ) ^ p :=
by
have : Nontrivial ι := Fintype.one_lt_card_iff_nontrivial.mp (by exact_mod_cast hp.lt)
have h0 : (1 : ℝ) < #ι := by norm_cast; exact Fintype.one_lt_card
have h1 : (0 : ℝ) < #ι - 1 := by linarith
have h2 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
have h3 : (#ι - 1 : ℝ) * ((1 : ℝ) / (#ι - 1 : ℝ)) ≤ 1 := by field_simp; rfl
have h4 : p = 1 + 1 / (↑#ι - 1) := by simp [field]; rw [mul_comm, hp.sub_one_mul_conj]
rw [h4]
convert lintegral_mul_prod_lintegral_pow_le μ h2 h3 hf using 2
field_simp
simp
