-- Mathlib/Analysis/SumIntegralComparisons.lean
lemma 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)

Proof state:
a b : ℕ
f g : ℝ → ℝ
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)
⊢ Integrable (fun x => f x * g (x - 1)) (volume.restrict (Icc ↑a ↑b))

Tactic:
apply Integrable.mul_of_top_left

Result:
case hφ
a b : ℕ
f g : ℝ → ℝ
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)
⊢ Integrable f (volume.restrict (Icc ↑a ↑b))

case hf
a b : ℕ
f g : ℝ → ℝ
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)
⊢ MemLp (fun x => g (x - 1)) ⊤ (volume.restrict (Icc ↑a ↑b))

Proof state:
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑a ∈ Icc ↑a ↑b

Tactic:
simp [hab]

Result:
no goals

Proof state:
case h
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi

Result:
case h
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Proof state:
case h.c0
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ 0 ≤ g ↑i

Tactic:
apply gpos.trans

Result:
case h.c0
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ g (↑b - 1) ≤ g ↑i

Proof state:
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ ↑i + 1 ≤ ↑b

Tactic:
norm_cast

Result:
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ i + 1 ≤ b

Proof state:
case h
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) := by
  simp only [mem_Icc, tsub_le_iff_right]
  exact ⟨by norm_cast; omega, I0⟩

Result:
case h
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Proof state:
case h.h₁.x
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑i ∈ Icc ↑a ↑b

Tactic:
simp only [mem_Icc, Nat.cast_le]

Result:
case h.h₁.x
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ a ≤ i ∧ i ≤ b

Proof state:
case h.h₁.x
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ x ∈ Icc ↑a ↑b

Tactic:
exact I2

Result:
no goals

Proof state:
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ ↑a ≤ ↑i + 1 ∧ ↑i ≤ ↑b - 1

Tactic:
exact ⟨by norm_cast; omega, I0⟩

Result:
no goals

Proof state:
case hf
a b : ℕ
f g : ℝ → ℝ
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)
⊢ MemLp (fun x => g (x - 1)) ⊤ (volume.restrict (Icc ↑a ↑b))

Tactic:
apply AntitoneOn.memLp_isCompact isCompact_Icc

Result:
case hf
a b : ℕ
f g : ℝ → ℝ
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)
⊢ AntitoneOn (fun x => g (x - 1)) (Icc ↑a ↑b)

Proof state:
case h
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
have I2 : x ∈ Icc (a : ℝ) b := by
  refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
  norm_cast
  omega

Result:
case h
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ f ↑i * g ↑i ≤ f x * g (x - 1)

Proof state:
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ ↑i ≤ ↑b - 1

Tactic:
simp only [le_sub_iff_add_le]

Result:
a b : ℕ
f g : ℝ → ℝ
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 : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ ↑i + 1 ≤ ↑b

Proof state:
case hg
a b : ℕ
f g : ℝ → ℝ
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)
⊢ IntegrableOn (fun x => f x * g (x - 1)) (Ico ↑a ↑b) volume

Tactic:
apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)

Result:
a b : ℕ
f g : ℝ → ℝ
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)
⊢ Integrable (fun x => f x * g (x - 1)) (volume.restrict (Icc ↑a ↑b))