internlm/Lean-Github huggingface dataset:
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)
⊢ ∫ (x : ℝ) in x₀..x₀ + 1, f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
Tactic:
apply intervalIntegral.integral_mono_ae_restrict (by linarith) (by simp) l4
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)
⊢ (fun u => f (x₀ + 1)) ≤ᶠ[ae (volume.restrict (Icc x₀ (x₀ + 1)))] f
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)
⊢ (fun u => f (x₀ + 1)) ≤ᶠ[ae (volume.restrict (Icc x₀ (x₀ + 1)))] f
Tactic:
apply eventually_of_mem _ l5
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)
⊢ Ioc x₀ (x₀ + 1) ∈ ae (volume.restrict (Icc x₀ (x₀ + 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)))
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)
⊢ Ioc x₀ (x₀ + 1) ∈ ae (volume.restrict (Icc x₀ (x₀ + 1)))
Tactic:
have : (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀} := by simp [← diff_eq_compl_inter]
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)
this : (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀}
⊢ Ioc x₀ (x₀ + 1) ∈ ae (volume.restrict (Icc x₀ (x₀ + 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)))
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)
this : (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀}
⊢ Ioc x₀ (x₀ + 1) ∈ ae (volume.restrict (Icc x₀ (x₀ + 1)))
Tactic:
simp [ae, this]
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)
⊢ 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)
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)
⊢ IntervalIntegrable (fun u => f (x₀ + 1)) volume x₀ (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)
⊢ (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀}
Tactic:
simp [← diff_eq_compl_inter]
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)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
⊢ AntitoneOn (fun x => f (x₀ + x)) (Icc 1 ↑(n + 1))
Tactic:
intro u ⟨hu1, _⟩ v ⟨_, hv2⟩ huv
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)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
u : ℝ
hu1 : 1 ≤ u
right✝ : u ≤ ↑(n + 1)
v : ℝ
left✝ : 1 ≤ v
hv2 : v ≤ ↑(n + 1)
huv : u ≤ v
⊢ (fun x => f (x₀ + x)) v ≤ (fun x => f (x₀ + x)) u
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)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
u : ℝ
hu1 : 1 ≤ u
right✝ : u ≤ ↑(n + 1)
v : ℝ
left✝ : 1 ≤ v
hv2 : v ≤ ↑(n + 1)
huv : u ≤ v
⊢ (fun x => f (x₀ + x)) v ≤ (fun x => f (x₀ + x)) u
Tactic:
push_cast at hv2
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)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
u : ℝ
hu1 : 1 ≤ u
right✝ : u ≤ ↑(n + 1)
v : ℝ
left✝ : 1 ≤ v
huv : u ≤ v
hv2 : v ≤ ↑n + 1
⊢ (fun x => f (x₀ + x)) v ≤ (fun x => f (x₀ + x)) u
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)
l1 : f (x₀ + 1) ≤ ∫ (x : ℝ) in x₀..x₀ + 1, f x
u : ℝ
hu1 : 1 ≤ u
right✝ : u ≤ ↑(n + 1)
v : ℝ
left✝ : 1 ≤ v
huv : u ≤ v
hv2 : v ≤ ↑n + 1
⊢ (fun x => f (x₀ + x)) v ≤ (fun x => f (x₀ + x)) u
Tactic:
refine hf ⟨?_, ?_⟩ ⟨?_, ?_⟩ ?_ <;> 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
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))
⊢ 1 ≤ 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)
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))
⊢ AntitoneOn (fun x => f (x₀ + x)) (Icc ↑1 ↑(n + 1))
Tactic:
simpa using l2
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
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)
Tactic:
apply IntegrableOn.intervalIntegrable
Proof state after:
case h.e'_4.hab.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)
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
⊢ IntegrableOn (fun x => f x) (uIcc x₀ (x₀ + 1)) volume
Theorem: sum_le_integral
Proof state before:
case h.e'_4.hab.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)
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
⊢ IntegrableOn (fun x => f x) (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 h.e'_4.hab.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)
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
⊢ IntegrableOn (fun x => f x) (Icc x₀ (x₀ + 1)) volume
Theorem: sum_le_integral
Proof state before:
case h.e'_4.hab.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)
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
⊢ IntegrableOn (fun x => f x) (Icc x₀ (x₀ + 1)) volume
Tactic:
apply hfi.mono_set
Proof state after:
case h.e'_4.hab.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)
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
⊢ Icc x₀ (x₀ + 1) ⊆ Icc x₀ (x₀ + ↑(n + 1))
Theorem: sum_le_integral
Proof state before:
case h.e'_4.hab.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)
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
⊢ Icc x₀ (x₀ + 1) ⊆ Icc x₀ (x₀ + ↑(n + 1))
Tactic:
apply Icc_subset_Icc
Proof state after:
case h.e'_4.hab.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)
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₀ ≤ x₀

case h.e'_4.hab.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)
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₀ + 1 ≤ x₀ + ↑(n + 1)
Theorem: sum_le_integral
Proof state before:
case h.e'_4.hab.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)
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₀ ≤ x₀

case h.e'_4.hab.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)
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₀ + 1 ≤ x₀ + ↑(n + 1)
Tactic:
linarith
Proof state after:
case h.e'_4.hab.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)
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₀ + 1 ≤ x₀ + ↑(n + 1)
Theorem: sum_le_integral
Proof state before:
case h.e'_4.hab.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)
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₀ + 1 ≤ x₀ + ↑(n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: sum_le_integral
Proof state before:
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))
Tactic:
apply IntegrableOn.intervalIntegrable
Proof state after:
case h.e'_4.hbc.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)
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
⊢ IntegrableOn (fun x => f x) (uIcc (x₀ + 1) (x₀ + (↑n + 1))) volume