integral_le_sum_mul_Ico_of_antitone_monotone

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

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