internlm/Lean-Github huggingface dataset:
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.convert_2.convert_1.h
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 ε
h : (fun w => w) (-z - 1) = 0
⊢ False
Tactic:
simp only [Metric.mem_ball, ε, Complex.dist_eq,
  neg_eq_iff_eq_neg.mp <| sub_eq_zero.mp h] at hz
Proof state after:
case h.convert_2.convert_1.h
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 : ℂ
h : (fun w => w) (-z - 1) = 0
hz : Complex.abs (-1 - s) < s.re / 2
⊢ False
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.convert_2.convert_1.h
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 : ℂ
h : (fun w => w) (-z - 1) = 0
hz : Complex.abs (-1 - s) < s.re / 2
⊢ False
Tactic:
have := (abs_le.mp <| le_trans (abs_re_le_abs (-1-s)) hz.le).1
Proof state after:
case h.convert_2.convert_1.h
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 : ℂ
h : (fun w => w) (-z - 1) = 0
hz : Complex.abs (-1 - s) < s.re / 2
this : -(s.re / 2) ≤ (-1 - s).re
⊢ False
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.convert_2.convert_1.h
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 : ℂ
h : (fun w => w) (-z - 1) = 0
hz : Complex.abs (-1 - s) < s.re / 2
this : -(s.re / 2) ≤ (-1 - s).re
⊢ False
Tactic:
simp only [sub_re, neg_re, one_re, neg_le_sub_iff_le_add, le_neg_add_iff_add_le] at this
Proof state after:
case h.convert_2.convert_1.h
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 : ℂ
h : (fun w => w) (-z - 1) = 0
hz : Complex.abs (-1 - s) < s.re / 2
this : 1 + s.re ≤ s.re / 2
⊢ False
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.convert_2.convert_1.h
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 : ℂ
h : (fun w => w) (-z - 1) = 0
hz : Complex.abs (-1 - s) < s.re / 2
this : 1 + s.re ≤ s.re / 2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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
Tactic:
apply hasDerivAt_id _ |>.neg |>.sub_const
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_6.h.h.e'_7
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℂ
⊢ (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-x✝ - 1)) = fun a => F x✝ a
Tactic:
ext a
Proof state after:
case h.e'_6.h.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℂ
a : ℝ
⊢ (↑⌊a⌋ + 1 / 2 - ↑a) * ↑a ^ (-x✝ - 1) = F x✝ a
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_6.h.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℂ
a : ℝ
⊢ (↑⌊a⌋ + 1 / 2 - ↑a) * ↑a ^ (-x✝ - 1) = F x✝ a
Tactic:
simp only [one_div, F, f, div_cpow_eq_cpow_neg]
Proof state after:
case h.e'_6.h.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℂ
a : ℝ
⊢ (↑⌊a⌋ + 2⁻¹ - ↑a) * ↑a ^ (-x✝ - 1) = ↑a ^ (-x✝ - 1) * (↑⌊a⌋ + 2⁻¹ - ↑a)
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_6.h.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℂ
a : ℝ
⊢ (↑⌊a⌋ + 2⁻¹ - ↑a) * ↑a ^ (-x✝ - 1) = ↑a ^ (-x✝ - 1) * (↑⌊a⌋ + 2⁻¹ - ↑a)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_7.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℝ
⊢ (↑⌊x✝⌋ + 1 / 2 - ↑x✝) * ↑x✝ ^ (-s - 1) * -↑x✝.log = F' s x✝
Tactic:
simp only [one_div, mul_neg, neg_mul, neg_inj, F', f, div_cpow_eq_cpow_neg]
Proof state after:
case h.e'_7.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℝ
⊢ (↑⌊x✝⌋ + 2⁻¹ - ↑x✝) * ↑x✝ ^ (-s - 1) * ↑x✝.log = ↑x✝ ^ (-s - 1) * ↑x✝.log * (↑⌊x✝⌋ + 2⁻¹ - ↑x✝)
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_7.h.e'_7.h
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 μ
h_diff : ∀ᵐ (x : ℝ) ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w => F w x) (F' z x) z
x✝ : ℝ
⊢ (↑⌊x✝⌋ + 2⁻¹ - ↑x✝) * ↑x✝ ^ (-s - 1) * ↑x✝.log = ↑x✝ ^ (-s - 1) * ↑x✝.log * (↑⌊x✝⌋ + 2⁻¹ - ↑x✝)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: HasDerivAt_neg_cpow_over2
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (-(-↑(↑N).log * ↑N ^ (-s)) / 2) s
Tactic:
convert hasDerivAt_neg' s |>.const_cpow (c := N) (by aesop) |>.neg |>.div_const _ using 1
Proof state after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
⊢ -(-↑(↑N).log * ↑N ^ (-s)) / 2 = -(↑N ^ (-s) * (↑N).log * -1) / 2
Theorem: HasDerivAt_neg_cpow_over2
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
⊢ -(-↑(↑N).log * ↑N ^ (-s)) / 2 = -(↑N ^ (-s) * (↑N).log * -1) / 2
Tactic:
simp [mul_comm]
Proof state after:
no goals
Theorem: HasDerivAt_neg_cpow_over2
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
⊢ ↑N ≠ 0 ∨ -s ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: HasDerivAt_cpow_over_var
Proof state before:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ z / z ^ 2 - ↑(↑N).log * ↑N ^ z / z) z
Tactic:
simp_rw [div_eq_mul_inv]
Proof state after:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z * z⁻¹) (↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹) z
Theorem: HasDerivAt_cpow_over_var
Proof state before:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z * z⁻¹) (↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹) z
Tactic:
convert HasDerivAt.mul (c := fun z ↦ - (N : ℂ) ^ z) (d := fun z ↦ z⁻¹) (c' := - (N : ℂ) ^ z * Real.log N)
  (d' := - (z ^ 2)⁻¹) ?_ ?_ using 1
Proof state after:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹ = -↑N ^ z * ↑(↑N).log * z⁻¹ + -↑N ^ z * -(z ^ 2)⁻¹

case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-↑N ^ z * ↑(↑N).log) z

case convert_3
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => z⁻¹) (-(z ^ 2)⁻¹) z
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹ = -↑N ^ z * ↑(↑N).log * z⁻¹ + -↑N ^ z * -(z ^ 2)⁻¹
Tactic:
simp only [natCast_log, neg_mul, cpow_ofNat, mul_neg, neg_neg]
Proof state after:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - (↑N).log * ↑N ^ z * z⁻¹ = -(↑N ^ z * (↑N).log * z⁻¹) + ↑N ^ z * (z ^ 2)⁻¹
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - (↑N).log * ↑N ^ z * z⁻¹ = -(↑N ^ z * (↑N).log * z⁻¹) + ↑N ^ z * (z ^ 2)⁻¹
Tactic:
ring_nf
Proof state after:
no goals
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-↑N ^ z * ↑(↑N).log) z
Tactic:
simp only [natCast_log, neg_mul]
Proof state after:
case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-(↑N ^ z * (↑N).log)) z
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-(↑N ^ z * (↑N).log)) z
Tactic:
apply HasDerivAt.neg
Proof state after:
case convert_2.h
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun x => ↑N ^ x) (↑N ^ z * (↑N).log) z
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case convert_2.h
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun x => ↑N ^ x) (↑N ^ z * (↑N).log) z
Tactic:
convert HasDerivAt.const_cpow (c := (N : ℂ)) (f := id) (f' := 1) (x := z) (hasDerivAt_id z)
  (by simp [z_ne_zero]) using 1
Proof state after:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (↑N).log = ↑N ^ id z * (↑N).log * 1
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (↑N).log = ↑N ^ id z * (↑N).log * 1
Tactic:
simp only [id_eq, mul_one]
Proof state after:
no goals
Theorem: HasDerivAt_cpow_over_var
Proof state before:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ≠ 0 ∨ id z ≠ 0
Tactic:
simp [z_ne_zero]
Proof state after:
no goals
Theorem: HasDerivAt_cpow_over_var
Proof state before:
case convert_3
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => z⁻¹) (-(z ^ 2)⁻¹) z
Tactic:
exact hasDerivAt_inv z_ne_zero
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (ζ₀ N) (ζ₀' N s) s
Tactic:
unfold riemannZeta0 ζ₀'
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt
    (fun s =>
      ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1))
    (∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(↑n).log +
          (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) +
        ↑(↑N).log * ↑N ^ (-s) / 2 +
      ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log))
    s
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt
    (fun s =>
      ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1))
    (∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(↑n).log +
          (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) +
        ↑(↑N).log * ↑N ^ (-s) / 2 +
      ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log))
    s
Tactic:
apply HasDerivAt.sum ?_ |>.add ?_ |>.add ?_ |>.add ?_
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ∀ i ∈ Finset.range (N + 1), HasDerivAt (fun x => 1 / ↑i ^ x) (-1 / ↑i ^ s * ↑(↑i).log) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (1 - x) / (1 - x)) (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (↑(↑N).log * ↑N ^ (-s) / 2) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) / ↑x_1 ^ (x + 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ∀ i ∈ Finset.range (N + 1), HasDerivAt (fun x => 1 / ↑i ^ x) (-1 / ↑i ^ s * ↑(↑i).log) s
Tactic:
intro n _
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ HasDerivAt (fun x => 1 / ↑n ^ x) (-1 / ↑n ^ s * ↑(↑n).log) s
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ HasDerivAt (fun x => 1 / ↑n ^ x) (-1 / ↑n ^ s * ↑(↑n).log) s
Tactic:
convert hasDerivAt_neg' s |>.const_cpow (c := n) (by aesop) using 1
Proof state after:
case h.e'_6
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ (fun x => 1 / ↑n ^ x) = fun x => ↑n ^ (-x)

case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_6
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ (fun x => 1 / ↑n ^ x) = fun x => ↑n ^ (-x)

case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Tactic:
all_goals (ring_nf; simp [cpow_neg])
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ ↑n ≠ 0 ∨ -s ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Tactic:
(ring_nf; simp [cpow_neg])
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1
Tactic:
ring_nf
Proof state after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -((↑n ^ s)⁻¹ * ↑(↑n).log) = -(↑n ^ (-s) * (↑n).log)