internlm/Lean-Github huggingface dataset:
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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 : ℝ) ∂volume.restrict {x | 1 < x},
    ∀ z ∈ Metric.ball s ε,
      HasDerivAt (fun w => ↑x ^ (-w - 1) * (↑⌊x⌋ + 1 / 2 - ↑x)) (↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) z
Tactic:
filter_upwards [h_bound1, self_mem_ae_restrict measSetIoi1] with x _ one_lt_x
Proof state after:
case 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 ∈ Metric.ball s ε,
    HasDerivAt (fun w => ↑x ^ (-w - 1) * (↑⌊x⌋ + 1 / 2 - ↑x)) (↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) z
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case 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 ∈ Metric.ball s ε,
    HasDerivAt (fun w => ↑x ^ (-w - 1) * (↑⌊x⌋ + 1 / 2 - ↑x)) (↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) z
Tactic:
intro z hz
Proof state after:
case 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 ε
⊢ HasDerivAt (fun w => ↑x ^ (-w - 1) * (↑⌊x⌋ + 1 / 2 - ↑x)) (↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) z
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case 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 ε
⊢ HasDerivAt (fun w => ↑x ^ (-w - 1) * (↑⌊x⌋ + 1 / 2 - ↑x)) (↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) z
Tactic:
convert HasDerivAt.mul_const (c := fun (w : ℂ) ↦ (x : ℂ) ^ (-w-1))
  (c' := (x : ℂ) ^ (-z-1) * -Real.log x) (d := (⌊x⌋ : ℝ) + 1 / 2 - x) ?_ using 1
Proof state after:
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
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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
Tactic:
simp only [mul_neg, mul_one]
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)) z
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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)) z
Tactic:
congr! 2
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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)
Tactic:
simp only
Proof state after:
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) (-z - 1)
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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) (-z - 1)
Tactic:
convert HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w ↦ w) (f' := 1) (x := -z-1)
  (hasDerivAt_id _) ?_ using 1
Proof state after:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑x ^ (-z - 1) * ↑x.log = ↑x ^ (-z - 1) * (↑x).log * 1

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 ε
⊢ ↑x ≠ 0 ∨ (fun w => w) (-z - 1) ≠ 0
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑x ^ (-z - 1) * ↑x.log = ↑x ^ (-z - 1) * (↑x).log * 1
Tactic:
simp only [mul_one, mul_eq_mul_left_iff, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq]
Proof state after:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑x.log = (↑x).log ∨ x = 0 ∧ ¬-z - 1 = 0
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑x.log = (↑x).log ∨ x = 0 ∧ ¬-z - 1 = 0
Tactic:
left
Proof state after:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑x.log = (↑x).log
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑x.log = (↑x).log
Tactic:
rw [Complex.ofReal_log]
Proof state after:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ 0 ≤ x
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case 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 μ
x : ℝ
a✝ : ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
one_lt_x : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ 0 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
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 ε
⊢ ↑x ≠ 0 ∨ (fun w => w) (-z - 1) ≠ 0
Tactic:
right
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 : ℂ
hz : z ∈ Metric.ball s ε
⊢ (fun w => w) (-z - 1) ≠ 0
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 ε
⊢ (fun w => w) (-z - 1) ≠ 0
Tactic:
intro h
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 : ℂ
hz : z ∈ Metric.ball s ε
h : (fun w => w) (-z - 1) = 0
⊢ False