sum_mul_Ico_le_integral_of_monotone_antitone

English

Suppose a ≤ b, f: R→R is monotone on Icc(a,b) and g: R→R is antitone on Icc(a-1,b-1). If f(a) ≥ 0 and g(b-1) ≥ 0, then the sum over i in Ico(a,b) of f(i)g(i) is bounded above by the integral ∫_a^b f(x)g(x-1) dx.

Русский

Пусть a ≤ b, f: R→R монотонна на Icc(a,b), а g: R→R антимонотонна на Icc(a−1,b−1). При неотрицательности f(a) и g(b−1) имеем: ∑_{i∈Ico(a,b)} f(i)g(i) ≤ ∫_a^b f(x)g(x−1) dx.

LaTeX

$$$\\forall a,b\\in\\mathbb{N}, a \\le b,\\ \\forall f,g:\\mathbb{R}\\to\\mathbb{R},\\; \\operatorname{MonotoneOn} f (\\mathrm{Icc}\\ a\\ b) \\land \\operatorname{AntitoneOn} g (\\mathrm{Icc}(a-1)(b-1))\\Rightarrow\\; \\sum_{i\\in \\mathrm{Ico} a b} f(i)g(i) \\le \\int_{a}^{b} f(x)g(x-1)\\, dx.$$$$

Lean4

theorem sum_mul_Ico_le_integral_of_monotone_antitone (hab : a ≤ b) (hf : MonotoneOn f (Icc a b))
    (hg : AntitoneOn g (Icc (a - 1) (b - 1))) (fpos : 0 ≤ f a) (gpos : 0 ≤ g (b - 1)) :
    ∑ i ∈ Finset.Ico a b, f i * g i ≤ ∫ x in a..b, f x * g (x - 1) :=
  by
  apply sum_Ico_le_integral_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 I1 (by simp [hab]) I0
    · apply fpos.trans
      apply hf (by simp [hab]) I2
      exact le_trans (mod_cast hi.1) hx.1
  · 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 AntitoneOn.memLp_isCompact isCompact_Icc
      intro x hx y hy hxy
      apply hg
      · simpa using hx
      · simpa using hy
      · simpa using hxy

Похожие утверждения