internlm/Lean-Github huggingface dataset:
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_5.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) μ
x : ℝ
⊢ ↑x ^ (-s - 1) * (↑⌊x⌋ + 1 / 2 - ↑x) = (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
ring_nf
Proof state after:
no goals
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) μ
⊢ AEStronglyMeasurable (F' s) μ
Tactic:
convert integrableOn_of_Zeta0_fun_log Npos hs |>.aestronglyMeasurable using 1
Proof state after:
case h.e'_5
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) μ
⊢ F' s = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_5
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) μ
⊢ F' s = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log
Tactic:
simp only [F', f]
Proof state after:
case h.e'_5
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) μ
⊢ (fun x => ↑x ^ (-s - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_5
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) μ
⊢ (fun x => ↑x ^ (-s - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)) = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log
Tactic:
ext x
Proof state after:
case h.e'_5.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) μ
x : ℝ
⊢ ↑x ^ (-s - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x) = (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.e'_5.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) μ
x : ℝ
⊢ ↑x ^ (-s - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x) = (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log
Tactic:
ring_nf
Proof state after:
no goals
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) μ
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 1 ≤ ↑N
Tactic:
simp only [Nat.one_le_cast]
Proof state after:
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) μ
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 1 ≤ N
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) μ
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 1 ≤ N
Tactic:
omega
Proof state after:
no goals
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}
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict {x | 1 < x}, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
Tactic:
filter_upwards [self_mem_ae_restrict measSetIoi1] with x hx
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}
x : ℝ
hx : 1 < x
⊢ ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
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}
x : ℝ
hx : 1 < x
⊢ ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖F' z x‖ ≤ bound x
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖F' z x‖ ≤ bound x
Tactic:
simp only [F', f, bound]
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)‖ ≤ |x ^ (-s.re / 2 - 1)| * |x.log|
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)‖ ≤ |x ^ (-s.re / 2 - 1)| * |x.log|
Tactic:
calc _ = ‖(x : ℂ) ^ (-z - 1)‖ * ‖-(Real.log x)‖ * ‖(⌊x⌋ + 1 / 2 - x)‖ := by
        simp only [mul_neg, one_div, neg_mul, norm_neg, norm_mul, norm_eq_abs, abs_ofReal,
          Real.norm_eq_abs, mul_eq_mul_left_iff, mul_eq_zero, map_eq_zero, cpow_eq_zero_iff,
          ofReal_eq_zero, ne_eq, abs_eq_zero, Real.log_eq_zero,
          ← (by simp : (((⌊x⌋ + 2⁻¹ - x) : ℝ) : ℂ) = (⌊x⌋ : ℂ) + 2⁻¹ - ↑x),
          Complex.abs_ofReal]
     _ = ‖x ^ (-z.re - 1)‖ * ‖-(Real.log x)‖ * ‖(⌊x⌋ + 1 / 2 - x)‖ := ?_
     _ = |x ^ (-z.re - 1)| * |(Real.log x)| * |(⌊x⌋ + 1 / 2 - x)| := by simp
     _ ≤ _ := ?_
Proof state after:
case h.calc_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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1)‖ * ‖-x.log‖ * ‖↑⌊x⌋ + 1 / 2 - x‖ = ‖x ^ (-z.re - 1)‖ * ‖-x.log‖ * ‖↑⌊x⌋ + 1 / 2 - x‖

case h.calc_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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ |x ^ (-z.re - 1)| * |x.log| * |↑⌊x⌋ + 1 / 2 - x| ≤ |x ^ (-s.re / 2 - 1)| * |x.log|
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1) * -↑x.log * (↑⌊x⌋ + 1 / 2 - ↑x)‖ = ‖↑x ^ (-z - 1)‖ * ‖-x.log‖ * ‖↑⌊x⌋ + 1 / 2 - x‖
Tactic:
simp only [mul_neg, one_div, neg_mul, norm_neg, norm_mul, norm_eq_abs, abs_ofReal,
  Real.norm_eq_abs, mul_eq_mul_left_iff, mul_eq_zero, map_eq_zero, cpow_eq_zero_iff,
  ofReal_eq_zero, ne_eq, abs_eq_zero, Real.log_eq_zero,
  ← (by simp : (((⌊x⌋ + 2⁻¹ - x) : ℝ) : ℂ) = (⌊x⌋ : ℂ) + 2⁻¹ - ↑x),
  Complex.abs_ofReal]
Proof state after:
no goals
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ↑(↑⌊x⌋ + 2⁻¹ - x) = ↑⌊x⌋ + 2⁻¹ - ↑x
Tactic:
simp
Proof state after:
no goals
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖x ^ (-z.re - 1)‖ * ‖-x.log‖ * ‖↑⌊x⌋ + 1 / 2 - x‖ = |x ^ (-z.re - 1)| * |x.log| * |↑⌊x⌋ + 1 / 2 - x|
Tactic:
simp
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.calc_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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1)‖ * ‖-x.log‖ * ‖↑⌊x⌋ + 1 / 2 - x‖ = ‖x ^ (-z.re - 1)‖ * ‖-x.log‖ * ‖↑⌊x⌋ + 1 / 2 - x‖
Tactic:
congr! 2
Proof state after:
case h.calc_1.h.e'_5.h.e'_5
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1)‖ = ‖x ^ (-z.re - 1)‖
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.calc_1.h.e'_5.h.e'_5
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ ‖↑x ^ (-z - 1)‖ = ‖x ^ (-z.re - 1)‖
Tactic:
simp only [norm_eq_abs, Real.norm_eq_abs, abs_cpow_eq_rpow_re_of_pos (by linarith),
  sub_re, neg_re, one_re]
Proof state after:
case h.calc_1.h.e'_5.h.e'_5
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ x ^ (-z.re - 1) = |x ^ (-z.re - 1)|
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.calc_1.h.e'_5.h.e'_5
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ x ^ (-z.re - 1) = |x ^ (-z.re - 1)|
Tactic:
apply abs_eq_self.mpr ?_ |>.symm
Proof state after:
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ 0 ≤ x ^ (-z.re - 1)
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ 0 ≤ x ^ (-z.re - 1)
Tactic:
positivity
Proof state after:
no goals
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ 0 < ?m.451134
Tactic:
linarith
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.calc_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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ |x ^ (-z.re - 1)| * |x.log| * |↑⌊x⌋ + 1 / 2 - x| ≤ |x ^ (-s.re / 2 - 1)| * |x.log|
Tactic:
rw [mul_comm, ← mul_assoc]
Proof state after:
case h.calc_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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (-z.re - 1)| * |x.log| ≤ |x ^ (-s.re / 2 - 1)| * |x.log|
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
case h.calc_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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (-z.re - 1)| * |x.log| ≤ |x ^ (-s.re / 2 - 1)| * |x.log|
Tactic:
apply mul_le_mul_of_nonneg_right ?_ <| abs_nonneg _
Proof state after:
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}
x : ℝ
hx : 1 < x
z : ℂ
hz : z ∈ Metric.ball s ε
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (-z.re - 1)| ≤ |x ^ (-s.re / 2 - 1)|