internlm/Lean-Github huggingface dataset:
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l3 := @AntitoneOn.sum_le_integral_Ico 1 (n + 1) (fun x => f (x₀ + x)) (by simp) (by simpa using l2)
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ i ∈ Finset.Ico 1 (n + 1), (fun x => f (x₀ + x)) ↑(i + 1) ≤ ∫ (x : ℝ) in ↑1 ..↑(n + 1), (fun x => f (x₀ + x)) x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ i ∈ Finset.Ico 1 (n + 1), (fun x => f (x₀ + x)) ↑(i + 1) ≤ ∫ (x : ℝ) in ↑1 ..↑(n + 1), (fun x => f (x₀ + x)) x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
simp at l3
Proof state after:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
convert _root_.add_le_add l1 l3
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
Theorem: sum_le_integral
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
Tactic:
have := @intervalIntegral.integral_comp_mul_add ℝ _ _ 1 (n + 1) 1 f one_ne_zero x₀
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (1 * x + x₀) = 1⁻¹ • ∫ (x : ℝ) in 1 * 1 + x₀..1 * (↑n + 1) + x₀, f x
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
Theorem: sum_le_integral
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (1 * x + x₀) = 1⁻¹ • ∫ (x : ℝ) in 1 * 1 + x₀..1 * (↑n + 1) + x₀, f x
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
Tactic:
simp [add_comm _ x₀] at this
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x) = ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
Theorem: sum_le_integral
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x) = ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
Tactic:
rw [this]
Proof state after:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x) = ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
Theorem: sum_le_integral
Proof state before:
case h.e'_4
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x) = ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
⊢ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x = (∫ (x : ℝ) in x₀..x₀ + 1, f x) + ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
Tactic:
rw [intervalIntegral.integral_add_adjacent_intervals]
Proof state after:
case h.e'_4.hab
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x) = ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
⊢ IntervalIntegrable (fun x => f x) volume x₀ (x₀ + 1)

case h.e'_4.hbc
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this✝ : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
l2 : AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
l3 : ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x)
this : ∫ (x : ℝ) in 1 ..↑n + 1, f (x₀ + x) = ∫ (x : ℝ) in x₀ + 1 ..x₀ + (↑n + 1), f x
⊢ IntervalIntegrable (fun x => f x) volume (x₀ + 1) (x₀ + (↑n + 1))
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
⊢ Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
Tactic:
ext i
Proof state after:
case a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
i : ℕ
⊢ i ∈ Finset.range (n + 1) ↔ i ∈ {0} ∪ Finset.Ico 1 (n + 1)
Theorem: sum_le_integral
Proof state before:
case a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
i : ℕ
⊢ i ∈ Finset.range (n + 1) ↔ i ∈ {0} ∪ Finset.Ico 1 (n + 1)
Tactic:
by_cases hi : i = 0 <;> simp [hi]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
i : ℕ
hi : ¬i = 0
⊢ i < n + 1 → 1 ≤ i
Theorem: sum_le_integral
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
i : ℕ
hi : ¬i = 0
⊢ i < n + 1 → 1 ≤ i
Tactic:
omega
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ IntervalIntegrable f volume x₀ (x₀ + 1)
Tactic:
apply IntegrableOn.intervalIntegrable
Proof state after:
case hf
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ IntegrableOn f (uIcc x₀ (x₀ + 1)) volume
Theorem: sum_le_integral
Proof state before:
case hf
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ IntegrableOn f (uIcc x₀ (x₀ + 1)) volume
Tactic:
simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le]
Proof state after:
case hf
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ IntegrableOn f (Icc x₀ (x₀ + 1)) volume
Theorem: sum_le_integral
Proof state before:
case hf
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ IntegrableOn f (Icc x₀ (x₀ + 1)) volume
Tactic:
apply hfi.mono_set
Proof state after:
case hf
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ Icc x₀ (x₀ + 1) ⊆ Icc x₀ (x₀ + ↑(n + 1))
Theorem: sum_le_integral
Proof state before:
case hf
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ Icc x₀ (x₀ + 1) ⊆ Icc x₀ (x₀ + ↑(n + 1))
Tactic:
apply Icc_subset_Icc
Proof state after:
case hf.h₁
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ x₀ ≤ x₀

case hf.h₂
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ x₀ + 1 ≤ x₀ + ↑(n + 1)
Theorem: sum_le_integral
Proof state before:
case hf.h₁
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ x₀ ≤ x₀

case hf.h₂
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ x₀ + 1 ≤ x₀ + ↑(n + 1)
Tactic:
linarith
Proof state after:
case hf.h₂
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ x₀ + 1 ≤ x₀ + ↑(n + 1)
Theorem: sum_le_integral
Proof state before:
case hf.h₂
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
⊢ x₀ + 1 ≤ x₀ + ↑(n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
x : ℝ
hx : x ∈ Ioc x₀ (x₀ + 1)
⊢ (fun x => f (x₀ + 1)) x ≤ f x
Tactic:
rcases hx with ⟨hx1, hx2⟩
Proof state after:
case intro
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
x : ℝ
hx1 : x₀ < x
hx2 : x ≤ x₀ + 1
⊢ (fun x => f (x₀ + 1)) x ≤ f x
Theorem: sum_le_integral
Proof state before:
case intro
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
x : ℝ
hx1 : x₀ < x
hx2 : x ≤ x₀ + 1
⊢ (fun x => f (x₀ + 1)) x ≤ f x
Tactic:
refine hf ⟨hx1, by linarith⟩ ⟨by linarith, by linarith⟩ hx2
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
x : ℝ
hx1 : x₀ < x
hx2 : x ≤ x₀ + 1
⊢ x ≤ x₀ + (↑n + 1)
Tactic:
linarith
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
x : ℝ
hx1 : x₀ < x
hx2 : x ≤ x₀ + 1
⊢ x₀ < x₀ + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
x : ℝ
hx1 : x₀ < x
hx2 : x ≤ x₀ + 1
⊢ x₀ + 1 ≤ x₀ + (↑n + 1)
Tactic:
linarith
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
⊢ ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
⊢ f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
Tactic:
rw [← l6]
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
l6 : ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1)
⊢ ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x