awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hφ : @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
⊢ @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
have hf₁ : MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
Tactic: apply Integrable.mul_of_top_left
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
have hf₁ : AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ g (x - 1)) (Icc (↑a : ℝ) (↑b : ℝ))
Tactic: apply AntitoneOn.memLp_isCompact isCompact_Icc
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) y) ((fun (x : ℝ) ↦ g (x - 1)) x)
have hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) y) ((fun (x : ℝ) ↦ g (x - 1)) x)
have hf₂ : y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hf₂ : y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) y) ((fun (x : ℝ) ↦ g (x - 1)) x)
have hf₃ : x - 1 ≤ y - 1
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x * g (x - 1)) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ) * g (↑i : ℝ))
have h : ∀ i ∈ Ico a b,
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
Tactic: apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
h :
  ∀ i ∈ Ico a b,
    ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x * g (x - 1)) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ) * g (↑i : ℝ))
have hg₁ : IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume
Tactic: apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have hx₁ : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi
Cleared hypotheses: hi, hx
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
hx₁ : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have hi₁ : a ≤ i ∧ i < b
Tactic: simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi
Cleared hypotheses: hi, hx
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
have simp : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
Tactic: simp only [le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
have norm_cast : i + 1 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
Tactic: have I0 : (i : ℝ) ≤ b - 1 := by
      simp only [le_sub_iff_add_le]
      norm_cast
      lia
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
have simp : (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ∧ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
Tactic: simp only [mem_Icc, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have norm_cast : a ≤ i + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) := by
      simp only [mem_Icc, tsub_le_iff_right]
      exact ⟨by norm_cast; lia, I0⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
have refine : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
Tactic: refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
have norm_cast : i + 1 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
Tactic: have I2 : x ∈ Icc (a : ℝ) b := by
      refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
      norm_cast
      lia
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have h : f x ≤ f (↑i : ℝ)
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f x ≤ f (↑i : ℝ)
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have h₁ : g (x - 1) ≤ g (↑i : ℝ)
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f x ≤ f (↑i : ℝ)
h₁ : g (x - 1) ≤ g (↑i : ℝ)
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have h₂ : 0 ≤ g (x - 1)
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f x ≤ f (↑i : ℝ)
h₁ : g (x - 1) ≤ g (↑i : ℝ)
h₂ : 0 ≤ g (x - 1)
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
have h₃ : 0 ≤ f (↑i : ℝ)
Tactic: apply mul_le_mul
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f x ≤ f (↑i : ℝ)
have h : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
h₁ : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ f x ≤ f (↑i : ℝ)
have h₂ : (↑i : ℝ) ≤ x
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
have h : a ≤ i ∧ i ≤ b
Tactic: simp only [mem_Icc, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ g (x - 1) ≤ g (↑i : ℝ)
have h : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
h₁ : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ g (x - 1) ≤ g (↑i : ℝ)
have h₂ : x - 1 ≤ (↑i : ℝ)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
have h : (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)
Tactic: simp only [mem_Icc, tsub_le_iff_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)
have h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
Tactic: refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
have h : i + 1 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ 0 ≤ g (x - 1)
have h : g (HSub.hSub (α := ℝ) (↑a : ℝ) 1) ≤ g (x - 1)
Tactic: apply gpos.trans
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ 0 ≤ f (↑i : ℝ)
have h : f (↑b : ℝ) ≤ f (↑i : ℝ)
Tactic: apply fpos.trans
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
⊢ IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume
have apply : @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1)) (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
Tactic: apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
⊢ @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
have hφ : @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
Tactic: apply Integrable.mul_of_top_left
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
hφ : @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
⊢ @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
have hf₁ : MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
Tactic: apply Integrable.mul_of_top_left
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
⊢ MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
have hf₁ : MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ g (x - 1)) (Icc (↑a : ℝ) (↑b : ℝ))
Tactic: apply MonotoneOn.memLp_isCompact isCompact_Icc