Theorem: sum_eq_int_deriv_aux2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
set u := fun (x : ℝ) ↦ c - x
State after:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x

State before:
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
set u' := fun (x : ℝ) ↦ (-1 : ℂ)
State after:
φ : ℝ → ℂ
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 : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x

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 : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
have hu : ∀ x ∈ uIcc a b, HasDerivAt u (u' x) x := by
  exact fun x _ ↦ by convert LinearDerivative_ofReal x (-1 : ℂ) c; ring
State after:
φ : ℝ → ℂ
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
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x

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
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
have hu' : IntervalIntegrable u' MeasureTheory.volume a b := by
  apply Continuous.intervalIntegrable; continuity
State after:
φ : ℝ → ℂ
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
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x

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
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
Tactic:
have hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b :=
  derivφCont.intervalIntegrable
State after:
φ : ℝ → ℂ
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

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

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

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

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

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

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

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