internlm/Lean-Github huggingface dataset:
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun t => t) (Ici ↑N)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun t => r - 1) (Ici ↑N)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => |x.log|) (Ici ↑N)
Tactic:
apply continuous_id.continuousOn.log ?_ |>.abs
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, id x ≠ 0
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, id x ≠ 0
Tactic:
intro x hx
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ id x ≠ 0
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ id x ≠ 0
Tactic:
simp only [id_eq]
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0
Tactic:
contrapose! Npos with h
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0
Tactic:
exact_mod_cast h ▸ mem_Ici.mp hx
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
have := isLittleO_log_rpow_atTop (r := -r / 2) (by linarith) |>.isBigO
Proof state after:
case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : Real.log =O[atTop] fun x => x ^ (-r / 2)
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Theorem: integrable_log_over_pow
Proof state before:
case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : Real.log =O[atTop] fun x => x ^ (-r / 2)
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
rw [Asymptotics.isBigO_iff_eventually, Filter.eventually_atTop] at this
Proof state after:
case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : ∃ a, ∀ b ≥ a, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Theorem: integrable_log_over_pow
Proof state before:
case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : ∃ a, ∀ b ≥ a, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
obtain ⟨C, hC⟩ := this
Proof state after:
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Theorem: integrable_log_over_pow
Proof state before:
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
have := hC C (by simp)
Proof state after:
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
this : ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ C * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Theorem: integrable_log_over_pow
Proof state before:
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
this : ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ C * ‖x ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
rw [Filter.eventually_atTop] at this
Proof state after:
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
this : ∃ a, ∀ b ≥ a, ‖b.log‖ ≤ C * ‖b ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Theorem: integrable_log_over_pow
Proof state before:
case ho.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
this : ∃ a, ∀ b ≥ a, ‖b.log‖ ≤ C * ‖b ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
obtain ⟨x₀, hx₀⟩ := this
Proof state after:
case ho.intro.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, ‖b.log‖ ≤ C * ‖b ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Theorem: integrable_log_over_pow
Proof state before:
case ho.intro.intro
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, ‖b.log‖ ≤ C * ‖b ^ (-r / 2)‖
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ 0 < -r / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
C : ℝ
hC : ∀ b ≥ C, ∀ᶠ (x : ℝ) in atTop, ‖x.log‖ ≤ b * ‖x ^ (-r / 2)‖
⊢ C ≥ C
Tactic:
simp
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume
Tactic:
have := integrableOn_Ioi_rpow_iff (s := r / 2 - 1) (t := N) (by simp [Npos]) |>.mpr
  (by linarith [rneg])
Proof state after:
case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : IntegrableOn (fun x => x ^ (r / 2 - 1)) (Ioi ↑N) volume
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume
Theorem: integrable_log_over_pow
Proof state before:
case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : IntegrableOn (fun x => x ^ (r / 2 - 1)) (Ioi ↑N) volume
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume
Tactic:
exact integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin.mp this |>.1
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ 0 < ↑N
Tactic:
simp [Npos]
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ r / 2 - 1 < -1
Tactic:
linarith [rneg]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log) (Ioi ↑N) volume
Tactic:
simp_rw [mul_assoc]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * (↑x ^ (-(s + 1)) * -↑x.log)) (Ioi ↑N) volume
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * (↑x ^ (-(s + 1)) * -↑x.log)) (Ioi ↑N) volume
Tactic:
apply Integrable.bdd_mul ?_ ?_ ?_
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => ↑x ^ (-(s + 1)) * -↑x.log) (volume.restrict (Ioi ↑N))

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (volume.restrict (Ioi ↑N))

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => ↑x ^ (-(s + 1)) * -↑x.log) (volume.restrict (Ioi ↑N))
Tactic:
simp only [neg_add_rev, mul_neg, add_comm, ← sub_eq_add_neg]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => -(↑x ^ (-s - 1) * ↑x.log)) (volume.restrict (Ioi ↑N))
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => -(↑x ^ (-s - 1) * ↑x.log)) (volume.restrict (Ioi ↑N))
Tactic:
apply integrable_norm_iff ?_ |>.mp ?_ |>.neg
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑x ^ (-s - 1) * ↑x.log) (volume.restrict (Ioi ↑N))

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => ‖↑a ^ (-s - 1) * ↑a.log‖) (volume.restrict (Ioi ↑N))
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑x ^ (-s - 1) * ↑x.log) (volume.restrict (Ioi ↑N))
Tactic:
apply ContinuousOn.mul ?_ ?_ |>.aestronglyMeasurable (by simp)
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x ^ (-s - 1)) (Ioi ↑N)

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x.log) (Ioi ↑N)
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasurableSet (Ioi ↑N)
Tactic:
simp
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x ^ (-s - 1)) (Ioi ↑N)
Tactic:
intro x hx
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x ^ (-s - 1)) (Ioi ↑N) x
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x ^ (-s - 1)) (Ioi ↑N) x
Tactic:
apply ContinuousWithinAt.cpow ?_ continuous_const.continuousWithinAt ?_
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x) (Ioi ↑N) x

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ↑x ∈ slitPlane
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x) (Ioi ↑N) x
Tactic:
exact RCLike.continuous_ofReal.continuousWithinAt
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ↑x ∈ slitPlane
Tactic:
simp only [ofReal_mem_slitPlane]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 0 < x
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 0 < x
Tactic:
linarith [mem_Ioi.mp hx]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x.log) (Ioi ↑N)
Tactic:
apply RCLike.continuous_ofReal.continuousOn.comp ?_ (mapsTo_image _ _)
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn
    (fun x =>
      Decidable.rec (fun h => (fun hx => Real.expOrderIso.symm ⟨|x|, ⋯⟩) h) (fun h => (fun hx => 0) h)
        (x.decidableEq 0))
    (Ioi ↑N)
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn
    (fun x =>
      Decidable.rec (fun h => (fun hx => Real.expOrderIso.symm ⟨|x|, ⋯⟩) h) (fun h => (fun hx => 0) h)
        (x.decidableEq 0))
    (Ioi ↑N)
Tactic:
refine continuous_id.continuousOn.log ?_
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∀ x ∈ Ioi ↑N, id x ≠ 0
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∀ x ∈ Ioi ↑N, id x ≠ 0
Tactic:
intro x hx
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ id x ≠ 0
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ id x ≠ 0
Tactic:
simp only [id_eq]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ x ≠ 0
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ x ≠ 0
Tactic:
linarith [mem_Ioi.mp hx]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => ‖↑a ^ (-s - 1) * ↑a.log‖) (volume.restrict (Ioi ↑N))
Tactic:
simp only [norm_mul, norm_eq_abs, abs_ofReal]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
Tactic:
have := integrable_log_over_pow (r := -s.re) (by linarith) Npos
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
Tactic:
apply IntegrableOn.congr_fun this ?_ (by simp)
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ EqOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (Ioi ↑N)
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ EqOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (Ioi ↑N)
Tactic:
intro x hx
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ (fun x => |x ^ (-s.re - 1)| * |x.log|) x = (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) x
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ (fun x => |x ^ (-s.re - 1)| * |x.log|) x = (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) x
Tactic:
simp only [mul_eq_mul_right_iff, abs_eq_zero, Real.log_eq_zero]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1)) ∨ x = 0 ∨ x = 1 ∨ x = -1
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1)) ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
left
Proof state after:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
Tactic:
have xpos : 0 < x := by linarith [mem_Ioi.mp hx]
Proof state after:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
xpos : 0 < x
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
xpos : 0 < x
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
Tactic:
simp [abs_cpow_eq_rpow_re_of_pos xpos, Real.abs_rpow_of_nonneg xpos.le,
  abs_eq_self.mpr xpos.le]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ -s.re < 0
Tactic:
linarith
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ MeasurableSet (Ioi ↑N)
Tactic:
simp
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 0 < x
Tactic:
linarith [mem_Ioi.mp hx]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (volume.restrict (Ioi ↑N))
Tactic:
apply Measurable.add ?_ measurable_const |>.sub (by fun_prop) |>.aestronglyMeasurable
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun a => ↑⌊a⌋
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun a => ↑⌊a⌋
Tactic:
exact Measurable.comp (fun _ _ ↦ trivial) Int.measurable_floor
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun a => ↑a
Tactic:
fun_prop
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C
Tactic:
convert ZetaSum_aux2a with _ x
Proof state after:
case h.e'_2.h.h.h.e'_3
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x✝ x : ℝ
⊢ ‖↑⌊x⌋ + 1 / 2 - ↑x‖ = |↑⌊x⌋ + 1 / 2 - x|
Theorem: integrableOn_of_Zeta0_fun_log
Proof state before:
case h.e'_2.h.h.h.e'_3
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x✝ x : ℝ
⊢ ‖↑⌊x⌋ + 1 / 2 - ↑x‖ = |↑⌊x⌋ + 1 / 2 - x|
Tactic:
simp [← Complex.abs_ofReal]
Proof state after:
no goals
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
hs : s ∈ {s | 0 < s.re}
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
simp only [mem_setOf_eq] at hs
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
set f : ℝ → ℂ := fun x ↦ (⌊x⌋ : ℂ) + 1 / 2 - x
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Theorem: hasDerivAt_Zeta0Integral
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
set F : ℂ → ℝ → ℂ := fun s x ↦ (x : ℂ) ^ (- s - 1) * f x
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
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
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
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
set F' : ℂ → ℝ → ℂ := fun s x ↦ (x : ℂ) ^ (- s - 1) * (- Real.log x) * f x
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
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
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
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
set ε := s.re / 2
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
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
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
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
have ε_pos : 0 < ε := by aesop
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 < ε
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
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 < ε
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
set bound : ℝ → ℝ := fun x ↦ |x ^ (- s.re / 2 - 1)| * |Real.log x|
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|
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
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|
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s
Tactic:
let μ : Measure ℝ := volume.restrict (Ioi (N : ℝ))
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)
⊢ HasDerivAt (fun z => ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-z - 1))
    (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log) s