Theorem: Zeta_eq_int_derivZeta (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
Tactic:
have diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (σ + t * I) := by
  intro σ
  refine differentiableAt_riemannZeta ?_
  contrapose! t_ne_zero; apply And.right; simpa [Complex.ext_iff] using t_ne_zero
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
Tactic:
apply intervalIntegral.integral_deriv_eq_sub'
State after:
case hderiv
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => ζ (↑σ₂ + ↑t * I)) = fun y => deriv ζ (↑y + ↑t * I)

case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ [[σ₁, σ₂]], DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) x

case hcont
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => deriv ζ (↑y + ↑t * I)) [[σ₁, σ₂]]

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
⊢ ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
Tactic:
intro σ
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ DifferentiableAt ℂ ζ (↑σ + ↑t * I)

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ DifferentiableAt ℂ ζ (↑σ + ↑t * I)
Tactic:
refine differentiableAt_riemannZeta ?_
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ ↑σ + ↑t * I ≠ 1

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ ↑σ + ↑t * I ≠ 1
Tactic:
contrapose! t_ne_zero
State after:
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ t = 0

State before:
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ t = 0
Tactic:
apply And.right
State after:
case self
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ ?a ∧ t = 0

case a
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ Prop

State before:
case self
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ ?a ∧ t = 0

case a
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ Prop
Tactic:
simpa [Complex.ext_iff] using t_ne_zero
State after:
no goals

State before:
case hderiv
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => ζ (↑σ₂ + ↑t * I)) = fun y => deriv ζ (↑y + ↑t * I)
Tactic:
exact deriv_fun_re diff
State after:
no goals

State before:
case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ [[σ₁, σ₂]], DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) x
Tactic:
intro s _
State after:
case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) s

State before:
case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) s
Tactic:
apply DifferentiableAt.comp
State after:
case hdiff.hg
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ ζ (↑s + ↑t * I)

case hdiff.hf
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun σ₂ => ↑σ₂ + ↑t * I) s

State before:
case hdiff.hg
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ ζ (↑s + ↑t * I)
Tactic:
exact (diff s).restrictScalars ℝ
State after:
no goals

State before:
case hdiff.hf
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun σ₂ => ↑σ₂ + ↑t * I) s
Tactic:
exact DifferentiableAt.add_const (c := t * I) <| differentiableAt_ofReal _
State after:
no goals

State before:
case hcont
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => deriv ζ (↑y + ↑t * I)) [[σ₁, σ₂]]
Tactic:
apply ContinuousOn.comp (g := deriv ζ) ?_ ?_ (mapsTo_image _ _)
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (deriv ζ) ((fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]])

σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => ↑y + ↑t * I) [[σ₁, σ₂]]

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (deriv ζ) ((fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]])
Tactic:
apply HasDerivAt.continuousOn (f' := deriv <| deriv ζ)
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]], HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]], HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x
Tactic:
intro x hx
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x
Tactic:
apply hasDerivAt_deriv_iff.mpr
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ DifferentiableAt ℂ (deriv ζ) x

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
replace hx : x ≠ 1 := by
  contrapose! hx
  simp only [hx, mem_image, Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
    I_im, mul_one, sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im, not_exists,
    not_and]
  exact fun _ _ _ ↦ t_ne_zero
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ DifferentiableAt ℂ (deriv ζ) x

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
have := (Complex.analyticAt_iff_eventually_differentiableAt (c := x) (f := ζ)).mpr ?_
State after:
case refine_2
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
⊢ DifferentiableAt ℂ (deriv ζ) x

case refine_1
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ ∀ᶠ (z : ℂ) in 𝓝 x, DifferentiableAt ℂ ζ z

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ x ≠ 1
Tactic:
contrapose! hx
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ x ∉ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ x ∉ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
Tactic:
simp only [hx, mem_image, Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
  I_im, mul_one, sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im, not_exists,
  not_and]
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ ∀ x ∈ [[σ₁, σ₂]], x = 1 → ¬t = 0

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ ∀ x ∈ [[σ₁, σ₂]], x = 1 → ¬t = 0
Tactic:
exact fun _ _ _ ↦ t_ne_zero
State after:
no goals

State before:
case refine_2
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
obtain ⟨r, hr, h⟩ := this.exists_ball_analyticOn
State after:
case refine_2.intro.intro
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ DifferentiableAt ℂ (deriv ζ) x

State before:
case refine_2.intro.intro
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
apply (h.deriv x ?_).differentiableAt
State after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ x ∈ Metric.ball x r

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ x ∈ Metric.ball x r
Tactic:
simp [hr]
State after:
no goals

State before:
case refine_1
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ ∀ᶠ (z : ℂ) in 𝓝 x, DifferentiableAt ℂ ζ z
Tactic:
filter_upwards [compl_singleton_mem_nhds hx] with z hz
State after:
case h
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ DifferentiableAt ℂ ζ z

State before:
case h
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ DifferentiableAt ℂ ζ z
Tactic:
apply differentiableAt_riemannZeta
State after:
case h.hs'
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ z ≠ 1

State before:
case h.hs'
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ z ≠ 1
Tactic:
simpa [mem_compl_iff, mem_singleton_iff] using hz
State after:
no goals

State before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => ↑y + ↑t * I) [[σ₁, σ₂]]
Tactic:
exact continuous_ofReal.continuousOn.add continuousOn_const
State after:
no goals