Theorem: sum_le_integral (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hf : AntitoneOn f (Ioc x₀ (x₀ + ↑n))
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑n)) volume
⊢ ∑ i ∈ Finset.range n, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑n, f x
Tactic:
cases' n with n <;> simp [Nat.succ_eq_add_one] at hf ⊢
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)))
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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)))
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1) := by
  ext i ; by_cases hi : i = 0 <;> simp [hi] ; omega
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)
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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)
⊢ ∑ x ∈ Finset.range (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
simp [this, Finset.sum_union]
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)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l4 : IntervalIntegrable f volume x₀ (x₀ + 1) := by
  apply IntegrableOn.intervalIntegrable
  simp only [ge_iff_le, le_add_iff_nonneg_right, zero_le_one, uIcc_of_le]
  apply hfi.mono_set
  apply Icc_subset_Icc ; linarith ; simp
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)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l5 x (hx : x ∈ Ioc x₀ (x₀ + 1)) : (fun x ↦ f (x₀ + 1)) x ≤ f x := by
  rcases hx with ⟨hx1, hx2⟩
  refine hf ⟨hx1, by linarith⟩ ⟨by linarith, by linarith⟩ hx2
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
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l6 : ∫ x in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1) := by simp
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)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l1 : f (x₀ + 1) ≤ ∫ x in x₀..x₀ + 1, f x := by
  rw [← l6] ; apply intervalIntegral.integral_mono_ae_restrict (by linarith) (by simp) l4
  apply eventually_of_mem _ l5
  have : (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀} := by simp [← diff_eq_compl_inter]
  simp [ae, this]
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
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
Tactic:
have l2 : AntitoneOn (fun x ↦ f (x₀ + x)) (Icc 1 ↑(n + 1)) := by
  intro u ⟨hu1, _⟩ v ⟨_, hv2⟩ huv ; push_cast at hv2
  refine hf ⟨?_, ?_⟩ ⟨?_, ?_⟩ ?_ <;> linarith
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))
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x

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)
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

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
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

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
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)

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₀
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)

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
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)

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]
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

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]
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))

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
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)

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]
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

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
State after:
no goals

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
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

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]
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

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
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))

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
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)

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
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)

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
State after:
no goals

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⟩
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
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

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
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

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
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)))

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]
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)))

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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]
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

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
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))

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
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)

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
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)

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
State after:
no goals

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
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

State before:
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
Tactic:
simp only [ge_iff_le, add_le_add_iff_left, le_add_iff_nonneg_left, Nat.cast_nonneg, uIcc_of_le]
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) (Icc (x₀ + 1) (x₀ + (↑n + 1))) volume

State before:
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) (Icc (x₀ + 1) (x₀ + (↑n + 1))) volume
Tactic:
apply hfi.mono_set
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
⊢ Icc (x₀ + 1) (x₀ + (↑n + 1)) ⊆ Icc x₀ (x₀ + ↑(n + 1))

State before:
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
⊢ Icc (x₀ + 1) (x₀ + (↑n + 1)) ⊆ Icc x₀ (x₀ + ↑(n + 1))
Tactic:
apply Icc_subset_Icc
State after:
case h.e'_4.hbc.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₀ + 1

case h.e'_4.hbc.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₀ + (↑n + 1) ≤ x₀ + ↑(n + 1)

State before:
case h.e'_4.hbc.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₀ + 1

case h.e'_4.hbc.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₀ + (↑n + 1) ≤ x₀ + ↑(n + 1)
Tactic:
linarith
State after:
case h.e'_4.hbc.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₀ + (↑n + 1) ≤ x₀ + ↑(n + 1)

State before:
case h.e'_4.hbc.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₀ + (↑n + 1) ≤ x₀ + ↑(n + 1)
Tactic:
simp
State after:
no goals