internlm/Lean-Github huggingface dataset:
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
convert intervalIntegral.integral_mul_deriv_eq_deriv_mul hu φDiff hu' hv' using 1
Proof state after:
case h.e'_3
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b
⊢ (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x = u b * φ b - u a * φ a - ∫ (x : ℝ) in a..b, u' x * φ x
Theorem: sum_eq_int_deriv_aux2
Proof state before:
case h.e'_3
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b
⊢ (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x = u b * φ b - u a * φ a - ∫ (x : ℝ) in a..b, u' x * φ x
Tactic:
simp [u]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
⊢ ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
Tactic:
exact fun x _ ↦ by convert LinearDerivative_ofReal x (-1 : ℂ) c; ring
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt u (u' x) x
Tactic:
convert LinearDerivative_ofReal x (-1 : ℂ) c
Proof state after:
case h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
x : ℝ
x✝¹ : x ∈ [[a, b]]
x✝ : ℝ
⊢ u x✝ = -1 * ↑x✝ + c
Theorem: sum_eq_int_deriv_aux2
Proof state before:
case h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
x : ℝ
x✝¹ : x ∈ [[a, b]]
x✝ : ℝ
⊢ u x✝ = -1 * ↑x✝ + c
Tactic:
ring
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux2
Proof state before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
⊢ IntervalIntegrable u' MeasureTheory.volume a b
Tactic:
apply Continuous.intervalIntegrable
Proof state after:
case hu
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
⊢ Continuous u'
Theorem: sum_eq_int_deriv_aux2
Proof state before:
case hu
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
⊢ Continuous u'
Tactic:
continuity
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
have flb_eq_k : ⌊b⌋ = k + 1 := Int.floor_eq_iff.mpr ⟨by exact_mod_cast b_eq_kpOne.symm.le,
  by rw [b_eq_kpOne]; simp⟩
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
simp only [flb_eq_k, Finset.Icc_self, Finset.sum_singleton, Int.cast_add, Int.cast_one]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
rw [sum_eq_int_deriv_aux2 (k + 1 / 2) φDiff derivφCont, b_eq_kpOne]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..↑k + 1, φ x) + (↑k + 1 + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..↑k + 1, φ x)
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..↑k + 1, φ x) + (↑k + 1 + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..↑k + 1, φ x)
Tactic:
ring_nf
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (1 + k), φ ↑x = φ (1 + ↑k)
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
this : Finset.Ioc k (1 + k) = {k + 1}
⊢ ∑ x ∈ Finset.Ioc k (1 + k), φ ↑x = φ (1 + ↑k)
Tactic:
simp_rw [this, Finset.sum_singleton, Int.cast_add, Int.cast_one, add_comm]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑(k + 1) ≤ b
Tactic:
exact_mod_cast b_eq_kpOne.symm.le
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ b < ↑(k + 1) + 1
Tactic:
rw [b_eq_kpOne]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑k + 1 < ↑(k + 1) + 1
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑k + 1 < ↑(k + 1) + 1
Tactic:
simp
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ Finset.Ioc k (1 + k) = {k + 1}
Tactic:
ext m
Proof state after:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m ∈ Finset.Ioc k (1 + k) ↔ m ∈ {k + 1}
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m ∈ Finset.Ioc k (1 + k) ↔ m ∈ {k + 1}
Tactic:
simp only [Finset.mem_Ioc, Finset.mem_singleton]
Proof state after:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k ↔ m = k + 1
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k ↔ m = k + 1
Tactic:
constructor
Proof state after:
case a.mp
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k → m = k + 1

case a.mpr
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m = k + 1 → k < m ∧ m ≤ 1 + k
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
case a.mp
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k → m = k + 1
Tactic:
exact fun ⟨h₁, h₂⟩ ↦ by rw [add_comm] at h₂; exact Int.le_antisymm h₂ h₁
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
x✝ : k < m ∧ m ≤ 1 + k
h₁ : k < m
h₂ : m ≤ 1 + k
⊢ m = k + 1
Tactic:
rw [add_comm] at h₂
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
x✝ : k < m ∧ m ≤ 1 + k
h₁ : k < m
h₂ : m ≤ k + 1
⊢ m = k + 1
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
x✝ : k < m ∧ m ≤ 1 + k
h₁ : k < m
h₂ : m ≤ k + 1
⊢ m = k + 1
Tactic:
exact Int.le_antisymm h₂ h₁
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
case a.mpr
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m = k + 1 → k < m ∧ m ≤ 1 + k
Tactic:
exact fun h ↦ ⟨by simp [h], by simp [h, add_comm]⟩
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
h : m = k + 1
⊢ k < m
Tactic:
simp [h]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_eq
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
h : m = k + 1
⊢ m ≤ 1 + k
Tactic:
simp [h, add_comm]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
have flb_eq_k : ⌊b⌋ = k := Int.floor_eq_iff.mpr ⟨by linarith [ha.1, ha.2], by linarith⟩
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
simp only [flb_eq_k, gt_iff_lt, lt_add_iff_pos_right, zero_lt_one, Finset.Icc_eq_empty_of_lt,
  Finset.sum_empty]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
rw [sum_eq_int_deriv_aux2 (k + 1 / 2) φDiff derivφCont]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Tactic:
have : Finset.Ioc k k = {} := by simp only [ge_iff_le, le_refl, Finset.Ioc_eq_empty_of_le]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Tactic:
simp only [this, Finset.sum_empty, one_div]
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ 0 =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a -
      ((↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ 0 =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a -
      ((↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑k ≤ b
Tactic:
linarith [ha.1, ha.2]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ b < ↑k + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux_lt
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ Finset.Ioc k k = ∅
Tactic:
simp only [ge_iff_le, le_refl, Finset.Ioc_eq_empty_of_le]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux1
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
by_cases h : b = k + 1
Proof state after:
case pos
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

case neg
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : ¬b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux1
Proof state before:
case pos
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
exact sum_eq_int_deriv_aux_eq h φDiff derivφCont
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux1
Proof state before:
case neg
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : ¬b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
exact sum_eq_int_deriv_aux_lt ha (Ne.lt_of_le h b_le_kpOne) φDiff derivφCont
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
have fl_a_eq_k : ⌊a⌋ = k := Int.floor_eq_iff.mpr ⟨ha.1, by linarith [ha.2]⟩
Proof state after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
convert sum_eq_int_deriv_aux1 ha b_le_kpOne φDiff derivφCont using 2
Proof state after:
case h.e'_2.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ Finset.Ioc ⌊a⌋ ⌊b⌋ = Finset.Ioc k ⌊b⌋

case h.e'_3.h.e'_5
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a

case h.e'_3.h.e'_6
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Theorem: sum_eq_int_deriv_aux
Proof state before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ a < ↑k + 1
Tactic:
linarith [ha.2]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h.e'_2.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ Finset.Ioc ⌊a⌋ ⌊b⌋ = Finset.Ioc k ⌊b⌋
Tactic:
rw [fl_a_eq_k]
Proof state after:
no goals
Theorem: sum_eq_int_deriv_aux
Proof state before:
case h.e'_3.h.e'_5
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a
Tactic:
congr
Proof state after:
no goals