Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.convert_2
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
F : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * f x
F' : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * -↑x.log * f x
ε : ℝ := s.re / 2
ε_pos : 0 < ε
bound : ℝ → ℝ := fun x => |x ^ (-s.re / 2 - 1)| * |x.log|
μ : Measure ℝ := volume.restrict (Ioi ↑N)
hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ
hF_int : Integrable (F s) μ
hF'_meas : AEStronglyMeasurable (F' s) μ
IoiSubIoi1 : Ioi ↑N ⊆ {x | 1 < x}
measSetIoi1 : MeasurableSet {x | 1 < x}
h_bound1 : ∀ᵐ (x : ℝ) ∂volume.restrict {x | 1 < x}, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
h_bound : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
bound_integrable : Integrable bound μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ HasDerivAt (fun w => ↑x ^ (-w - 1)) (↑x ^ (-z - 1) * -↑x.log) z
Tactic:
convert HasDerivAt.comp (h := fun w ↦ -w-1) (h' := -1) (h₂ := fun w ↦ x ^ w)
  (h₂' := x ^ (-z-1) * Real.log x) (x := z) ?_ ?_ using 0
Proof state after:
case a
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
F : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * f x
F' : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * -↑x.log * f x
ε : ℝ := s.re / 2
ε_pos : 0 < ε
bound : ℝ → ℝ := fun x => |x ^ (-s.re / 2 - 1)| * |x.log|
μ : Measure ℝ := volume.restrict (Ioi ↑N)
hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ
hF_int : Integrable (F s) μ
hF'_meas : AEStronglyMeasurable (F' s) μ
IoiSubIoi1 : Ioi ↑N ⊆ {x | 1 < x}
measSetIoi1 : MeasurableSet {x | 1 < x}
h_bound1 : ∀ᵐ (x : ℝ) ∂volume.restrict {x | 1 < x}, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
h_bound : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
bound_integrable : Integrable bound μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ HasDerivAt (fun w => ↑x ^ (-w - 1)) (↑x ^ (-z - 1) * -↑x.log) z ↔
    HasDerivAt ((fun w => ↑x ^ w) ∘ fun w => -w - 1) (↑x ^ (-z - 1) * ↑x.log * -1) z

case h.convert_2.convert_1
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
F : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * f x
F' : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * -↑x.log * f x
ε : ℝ := s.re / 2
ε_pos : 0 < ε
bound : ℝ → ℝ := fun x => |x ^ (-s.re / 2 - 1)| * |x.log|
μ : Measure ℝ := volume.restrict (Ioi ↑N)
hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ
hF_int : Integrable (F s) μ
hF'_meas : AEStronglyMeasurable (F' s) μ
IoiSubIoi1 : Ioi ↑N ⊆ {x | 1 < x}
measSetIoi1 : MeasurableSet {x | 1 < x}
h_bound1 : ∀ᵐ (x : ℝ) ∂volume.restrict {x | 1 < x}, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
h_bound : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
bound_integrable : Integrable bound μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ HasDerivAt (fun w => ↑x ^ w) (↑x ^ (-z - 1) * ↑x.log) ((fun w => -w - 1) z)

case h.convert_2.convert_2
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
F : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * f x
F' : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * -↑x.log * f x
ε : ℝ := s.re / 2
ε_pos : 0 < ε
bound : ℝ → ℝ := fun x => |x ^ (-s.re / 2 - 1)| * |x.log|
μ : Measure ℝ := volume.restrict (Ioi ↑N)
hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ
hF_int : Integrable (F s) μ
hF'_meas : AEStronglyMeasurable (F' s) μ
IoiSubIoi1 : Ioi ↑N ⊆ {x | 1 < x}
measSetIoi1 : MeasurableSet {x | 1 < x}
h_bound1 : ∀ᵐ (x : ℝ) ∂volume.restrict {x | 1 < x}, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
h_bound : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
bound_integrable : Integrable bound μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ HasDerivAt (fun w => -w - 1) (-1) z