English
Let a ≤ b, f: R→R be antitone on Icc(a,b) and g: R→R be monotone on Icc(a-1,b-1). If f(b) and g(a-1) are nonnegative, then ∫_a^b f(x)g(x-1) dx ≤ ∑_{i∈Ico(a,b)} f(i)g(i).
Русский
Пусть a ≤ b, f на Icc(a,b) антимонотонна, g на Icc(a-1,b-1) монотонна. При неотрицательности f(b) и g(a-1) имеем: ∫_a^b f(x)g(x-1) dx ≤ ∑_{i∈Ico(a,b)} f(i)g(i).
LaTeX
$$$\\forall a,b\\in\\mathbb{N}, a \\le b,\\ \\forall f,g:\\mathbb{R}\\to\\mathbb{R},\\; \\operatorname{AntitoneOn} f (\\mathrm{Icc} a b) \\land \\operatorname{MonotoneOn} g (\\mathrm{Icc}(a-1)(b-1))\\land 0\\le f(b)\\land 0\\le g(a-1)\\Rightarrow\\; \\int_{a}^{b} f(x)g(x-1) dx \\le \\sum_{i\\in \\mathrm{Ico} a b} f(i)g(i).$$$
Lean4
theorem integral_le_sum_mul_Ico_of_antitone_monotone (hab : a ≤ b) (hf : AntitoneOn f (Icc a b))
(hg : MonotoneOn g (Icc (a - 1) (b - 1))) (fpos : 0 ≤ f b) (gpos : 0 ≤ g (a - 1)) :
∫ x in a..b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f i * g i :=
by
apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab
· intro i hi x hx
simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi
have I0 : (i : ℝ) ≤ b - 1 := by
simp only [le_sub_iff_add_le]
norm_cast
omega
have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) :=
by
simp only [mem_Icc, tsub_le_iff_right]
exact ⟨by norm_cast; cutsat, I0⟩
have I2 : x ∈ Icc (a : ℝ) b :=
by
refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
norm_cast
omega
apply mul_le_mul
· apply hf
· simp only [mem_Icc, Nat.cast_le]
exact ⟨hi.1, hi.2.le⟩
· exact I2
· exact hx.1
· apply hg
· simp only [mem_Icc, tsub_le_iff_right, sub_add_cancel]
refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
norm_cast
cutsat
· exact I1
· simpa [sub_le_iff_le_add] using hx.2.le
· apply gpos.trans
apply hg (by simp [hab]) (by simpa using I2) (by simpa using I2.1)
· apply fpos.trans
apply hf ⟨mod_cast hi.1, mod_cast hi.2.le⟩ (by simpa using hab) (mod_cast hi.2.le)
· apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)
apply Integrable.mul_of_top_left
· exact hf.integrableOn_isCompact isCompact_Icc
· apply MonotoneOn.memLp_isCompact isCompact_Icc
intro x hx y hy hxy
apply hg
· simpa using hx
· simpa using hy
· simpa using hxy