internlm/Lean-Github huggingface dataset:
Theorem: ZetaSum_aux1_2
Proof state before:
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
⊢ EqOn (fun x => 1 / x ^ (c + 1)) (fun x => x ^ (-c - 1)) [[a, b]]
Tactic:
intro x hx
Proof state after:
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
x : ℝ
hx : x ∈ [[a, b]]
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
Theorem: ZetaSum_aux1_2
Proof state before:
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
x : ℝ
hx : x ∈ [[a, b]]
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
Tactic:
have : 0 ≤ x := (ZetaSum_aux1_1 apos a_lt_b hx).le
Proof state after:
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this✝ : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
x : ℝ
hx : x ∈ [[a, b]]
this : 0 ≤ x
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
Theorem: ZetaSum_aux1_2
Proof state before:
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this✝ : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
x : ℝ
hx : x ∈ [[a, b]]
this : 0 ≤ x
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
Tactic:
simp [div_rpow_eq_rpow_neg _ _ _ this, sub_eq_add_neg, add_comm]
Proof state after:
no goals
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ (a ^ (-c) - b ^ (-c)) / c = (b ^ (-c) - a ^ (-c)) / -c
Tactic:
ring
Proof state after:
no goals
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ -c - 1 ≠ -1
Tactic:
simp [h.1]
Proof state after:
no goals
Theorem: ZetaSum_aux1_3a
Proof state before:
x : ℝ
⊢ -(1 / 2) < ↑⌊x⌋ + 1 / 2 - x
Tactic:
norm_num [← add_assoc]
Proof state after:
x : ℝ
⊢ x < 1 / 2 + ↑⌊x⌋ + 1 / 2
Theorem: ZetaSum_aux1_3a
Proof state before:
x : ℝ
⊢ x < 1 / 2 + ↑⌊x⌋ + 1 / 2
Tactic:
linarith [sub_pos_of_lt (Int.lt_floor_add_one x)]
Proof state after:
no goals
Theorem: ZetaSum_aux1_3b
Proof state before:
x : ℝ
⊢ ↑⌊x⌋ + 1 / 2 - x ≤ 1 / 2
Tactic:
ring_nf
Proof state after:
x : ℝ
⊢ 1 / 2 + (↑⌊x⌋ - x) ≤ 1 / 2
Theorem: ZetaSum_aux1_3b
Proof state before:
x : ℝ
⊢ 1 / 2 + (↑⌊x⌋ - x) ≤ 1 / 2
Tactic:
exact add_le_of_nonpos_right <| sub_nonpos.mpr (Int.floor_le x)
Proof state after:
no goals
Theorem: ZetaSum_aux1_4'
Proof state before:
x : ℝ
hx : 0 < x
s : ℂ
⊢ ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re
Tactic:
simp [map_div₀, abs_ofReal, Complex.abs_cpow_eq_rpow_re_of_pos hx, ← abs_ofReal]
Proof state after:
no goals
Theorem: ZetaSum_aux1_4
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
⊢ ∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖ = ∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re
Tactic:
apply intervalIntegral.integral_congr
Proof state after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
⊢ EqOn (fun x => ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖) (fun x => |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re) [[a, b]]
Theorem: ZetaSum_aux1_4
Proof state before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
⊢ EqOn (fun x => ‖(↑⌊x⌋ + ↑1 / 2 - ↑x) / ↑x ^ (s + 1)‖) (fun x => |↑⌊x⌋ + 1 / 2 - x| / x ^ (s + 1).re) [[a, b]]
Tactic:
exact fun x hx ↦ ZetaSum_aux1_4' x (ZetaSum_aux1_1 apos a_lt_b hx) s
Proof state after:
no goals
Theorem: ZetaSum_aux1_5a
Proof state before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)
Tactic:
apply div_le_div_of_nonneg_right _ _
Proof state after:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1

a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ 0 ≤ x ^ (s.re + 1)
Theorem: ZetaSum_aux1_5a
Proof state before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1
Tactic:
exact le_trans (ZetaSum_aux1_3 x) (by norm_num)
Proof state after:
no goals
Theorem: ZetaSum_aux1_5a
Proof state before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ 1 / 2 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaSum_aux1_5a
Proof state before:
a b : ℝ
apos : 0 < a
s : ℂ
x : ℝ
h : x ∈ Icc a b
⊢ 0 ≤ x ^ (s.re + 1)
Tactic:
apply Real.rpow_nonneg <| le_of_lt (ZetaSum_aux1_1' apos h)
Proof state after:
no goals
Theorem: ZetaSum_aux1_5b
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
refine continuousOn_const.div ?_ ?_ |>.intervalIntegrable_of_Icc (le_of_lt a_lt_b)
Proof state after:
case refine_1
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ContinuousOn (fun u => u ^ (s.re + 1)) (Icc a b)

case refine_2
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, x ^ (s.re + 1) ≠ 0
Theorem: ZetaSum_aux1_5b
Proof state before:
case refine_1
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ContinuousOn (fun u => u ^ (s.re + 1)) (Icc a b)
Tactic:
exact continuousOn_id.rpow_const fun x hx ↦ Or.inl (ne_of_gt <| ZetaSum_aux1_1' apos hx)
Proof state after:
no goals
Theorem: ZetaSum_aux1_5b
Proof state before:
case refine_2
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, x ^ (s.re + 1) ≠ 0
Tactic:
exact fun x hx h ↦ by rw [Real.rpow_eq_zero] at h <;> linarith [ZetaSum_aux1_1' apos hx]
Proof state after:
no goals
Theorem: ZetaSum_aux1_5b
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
x : ℝ
hx : x ∈ Icc a b
h : x ^ (s.re + 1) = 0
⊢ False
Tactic:
rw [Real.rpow_eq_zero] at h <;> linarith [ZetaSum_aux1_1' apos hx]
Proof state after:
no goals
Theorem: ZetaSum_aux1_5c
Proof state before:
a b : ℝ
s : ℂ
⊢ let g := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1);
  AEStronglyMeasurable g (volume.restrict (Ι a b))
Tactic:
intro
Proof state after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ AEStronglyMeasurable g✝ (volume.restrict (Ι a b))
Theorem: ZetaSum_aux1_5c
Proof state before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ AEStronglyMeasurable g✝ (volume.restrict (Ι a b))
Tactic:
refine (Measurable.div ?_ <| measurable_id.pow_const _).aestronglyMeasurable
Proof state after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => |↑⌊u⌋ + 1 / 2 - u|
Theorem: ZetaSum_aux1_5c
Proof state before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => |↑⌊u⌋ + 1 / 2 - u|
Tactic:
refine _root_.continuous_abs.measurable.comp ?_
Proof state after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋ + 1 / 2 - u
Theorem: ZetaSum_aux1_5c
Proof state before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋ + 1 / 2 - u
Tactic:
refine Measurable.add ?_ measurable_const |>.sub measurable_id
Proof state after:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋
Theorem: ZetaSum_aux1_5c
Proof state before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable fun u => ↑⌊u⌋
Tactic:
exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor
Proof state after:
no goals
Theorem: ZetaSum_aux1_5c
Proof state before:
a b : ℝ
s : ℂ
g✝ : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ Measurable IntCast.intCast
Tactic:
exact fun _ _ ↦ trivial
Proof state after:
no goals
Theorem: ZetaSum_aux1_5d
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
set g : ℝ → ℝ := (fun u ↦ |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1))
Proof state after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ IntervalIntegrable g MeasureTheory.volume a b
Theorem: ZetaSum_aux1_5d
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ IntervalIntegrable g MeasureTheory.volume a b
Tactic:
apply ZetaSum_aux1_5b apos a_lt_b σpos |>.mono_fun ZetaSum_aux1_5c ?_
Proof state after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ (fun x => ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖) ≤ᵐ[MeasureTheory.volume.restrict (Ι a b)] fun x =>
    ‖1 / x ^ (s.re + 1)‖
Theorem: ZetaSum_aux1_5d
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ (fun x => ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖) ≤ᵐ[MeasureTheory.volume.restrict (Ι a b)] fun x =>
    ‖1 / x ^ (s.re + 1)‖
Tactic:
filter_upwards with x
Proof state after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖ ≤ ‖1 / x ^ (s.re + 1)‖
Theorem: ZetaSum_aux1_5d
Proof state before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖ ≤ ‖1 / x ^ (s.re + 1)‖
Tactic:
simp only [g, Real.norm_eq_abs, one_div, norm_inv, abs_div, _root_.abs_abs]
Proof state after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 2⁻¹ - x| / |x ^ (s.re + 1)| ≤ |x ^ (s.re + 1)|⁻¹
Theorem: ZetaSum_aux1_5d
Proof state before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 2⁻¹ - x| / |x ^ (s.re + 1)| ≤ |x ^ (s.re + 1)|⁻¹
Tactic:
conv => rw [div_eq_mul_inv, ← one_div]; rhs; rw [← one_mul |x ^ (s.re + 1)|⁻¹]
Proof state after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (s.re + 1)|⁻¹ ≤ 1 * |x ^ (s.re + 1)|⁻¹
Theorem: ZetaSum_aux1_5d
Proof state before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (s.re + 1)|⁻¹ ≤ 1 * |x ^ (s.re + 1)|⁻¹
Tactic:
refine mul_le_mul ?_ (le_refl _) (by simp) <| by norm_num
Proof state after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1
Theorem: ZetaSum_aux1_5d
Proof state before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1
Tactic:
exact le_trans (ZetaSum_aux1_3 x) <| by norm_num
Proof state after:
no goals
Theorem: ZetaSum_aux1_5d
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ 0 ≤ |x ^ (s.re + 1)|⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaSum_aux1_5d
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaSum_aux1_5d
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ 1 / 2 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaSum_aux1_5
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1)
Tactic:
apply intervalIntegral.integral_mono_on (le_of_lt a_lt_b) ?_ ?_
Proof state after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)

a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b

a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b
Theorem: ZetaSum_aux1_5
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)
Tactic:
exact ZetaSum_aux1_5a apos
Proof state after:
no goals
Theorem: ZetaSum_aux1_5
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
exact ZetaSum_aux1_5d apos a_lt_b σpos
Proof state after:
no goals
Theorem: ZetaSum_aux1_5
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
exact ZetaSum_aux1_5b apos a_lt_b σpos
Proof state after:
no goals
Theorem: ZetaBnd_aux1a
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ (a ^ (-s.re) - b ^ (-s.re)) / s.re
Tactic:
calc
  _ = ∫ x in a..b, |(⌊x⌋ + 1 / 2 - x)| / x ^ (s+1).re := ZetaSum_aux1_4 apos a_lt_b
  _ ≤ ∫ x in a..b, 1 / x ^ (s.re + 1) := ZetaSum_aux1_5 apos a_lt_b σpos
  _ = (a ^ (-s.re) - b ^ (-s.re)) / s.re := ?_
Proof state after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1) = (a ^ (-s.re) - b ^ (-s.re)) / s.re
Theorem: ZetaBnd_aux1a
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1) = (a ^ (-s.re) - b ^ (-s.re)) / s.re
Tactic:
refine ZetaSum_aux1_2 (c := s.re) apos a_lt_b ⟨ne_of_gt σpos, ?_⟩
Proof state after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ 0 ∉ [[a, b]]
Theorem: ZetaBnd_aux1a
Proof state before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ 0 ∉ [[a, b]]
Tactic:
exact fun h ↦ (lt_self_iff_false 0).mp <| ZetaSum_aux1_1 apos a_lt_b h
Proof state after:
no goals
Theorem: tsum_eq_partial_add_tail
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
⊢ ∑' (n : ℕ), f n = ∑ n ∈ Finset.range N, f n + ∑' (n : ℕ), f (n + N)
Tactic:
rw [← sum_add_tsum_nat_add (f := f) (h := hf) (k := N)]
Proof state after:
no goals
Theorem: Finset.Ioc_eq_Ico
Proof state before:
M N : ℕ
⊢ Ioc N M = Ico (N + 1) (M + 1)
Tactic:
ext a
Proof state after:
case a
M N a : ℕ
⊢ a ∈ Ioc N M ↔ a ∈ Ico (N + 1) (M + 1)
Theorem: Finset.Ioc_eq_Ico
Proof state before:
case a
M N a : ℕ
⊢ a ∈ Ioc N M ↔ a ∈ Ico (N + 1) (M + 1)
Tactic:
simp only [Finset.mem_Ioc, Finset.mem_Ico]
Proof state after:
case a
M N a : ℕ
⊢ N < a ∧ a ≤ M ↔ N + 1 ≤ a ∧ a < M + 1
Theorem: Finset.Ioc_eq_Ico
Proof state before:
case a
M N a : ℕ
⊢ N < a ∧ a ≤ M ↔ N + 1 ≤ a ∧ a < M + 1
Tactic:
constructor <;> intro ⟨h₁, h₂⟩ <;> omega
Proof state after:
no goals
Theorem: Finset.Ioc_eq_Icc
Proof state before:
M N : ℕ
⊢ Ioc N M = Icc (N + 1) M
Tactic:
ext a
Proof state after:
case a
M N a : ℕ
⊢ a ∈ Ioc N M ↔ a ∈ Icc (N + 1) M
Theorem: Finset.Ioc_eq_Icc
Proof state before:
case a
M N a : ℕ
⊢ a ∈ Ioc N M ↔ a ∈ Icc (N + 1) M
Tactic:
simp only [Finset.mem_Ioc, Finset.mem_Icc]
Proof state after:
case a
M N a : ℕ
⊢ N < a ∧ a ≤ M ↔ N + 1 ≤ a ∧ a ≤ M
Theorem: Finset.Ioc_eq_Icc
Proof state before:
case a
M N a : ℕ
⊢ N < a ∧ a ≤ M ↔ N + 1 ≤ a ∧ a ≤ M
Tactic:
constructor <;> intro ⟨h₁, h₂⟩ <;> omega
Proof state after:
no goals
Theorem: Finset.Icc_eq_Ico
Proof state before:
M N : ℕ
⊢ Icc N M = Ico N (M + 1)
Tactic:
ext a
Proof state after:
case a
M N a : ℕ
⊢ a ∈ Icc N M ↔ a ∈ Ico N (M + 1)
Theorem: Finset.Icc_eq_Ico
Proof state before:
case a
M N a : ℕ
⊢ a ∈ Icc N M ↔ a ∈ Ico N (M + 1)
Tactic:
simp only [Finset.mem_Icc, Finset.mem_Ico]
Proof state after:
case a
M N a : ℕ
⊢ N ≤ a ∧ a ≤ M ↔ N ≤ a ∧ a < M + 1
Theorem: Finset.Icc_eq_Ico
Proof state before:
case a
M N a : ℕ
⊢ N ≤ a ∧ a ≤ M ↔ N ≤ a ∧ a < M + 1
Tactic:
constructor <;> intro ⟨h₁, h₂⟩ <;> omega
Proof state after:
no goals
Theorem: finsetSum_tendsto_tsum
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
have := Summable.hasSum_iff_tendsto_nat hf (m := ∑' (n : ℕ), f n) |>.mp hf.hasSum
Proof state after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Theorem: finsetSum_tendsto_tsum
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
have const := @tendsto_const_nhds (x := ∑ i in Finset.range N, f i) ℕ _ atTop
Proof state after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Theorem: finsetSum_tendsto_tsum
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
have := Filter.Tendsto.sub this const
Proof state after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this :
  Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop
    (𝓝 (∑' (n : ℕ), f n - ∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Theorem: finsetSum_tendsto_tsum
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this :
  Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop
    (𝓝 (∑' (n : ℕ), f n - ∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
rw [tsum_eq_partial_add_tail f hf (N := N), add_comm, add_sub_cancel_right] at this
Proof state after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Theorem: finsetSum_tendsto_tsum
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
Tactic:
apply this.congr'
Proof state after:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) =ᶠ[atTop] fun k => ∑ n ∈ Finset.Ico N k, f n
Theorem: finsetSum_tendsto_tsum
Proof state before:
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) =ᶠ[atTop] fun k => ∑ n ∈ Finset.Ico N k, f n
Tactic:
filter_upwards [Filter.mem_atTop (N + 1)]
Proof state after:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ ∀ (a : ℕ), N + 1 ≤ a → ∑ i ∈ Finset.range a, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N a, f n
Theorem: finsetSum_tendsto_tsum
Proof state before:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ ∀ (a : ℕ), N + 1 ≤ a → ∑ i ∈ Finset.range a, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N a, f n
Tactic:
intro M hM
Proof state after:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ ∑ i ∈ Finset.range M, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N M, f n
Theorem: finsetSum_tendsto_tsum
Proof state before:
case h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ ∑ i ∈ Finset.range M, f i - ∑ i ∈ Finset.range N, f i = ∑ n ∈ Finset.Ico N M, f n
Tactic:
rw [Finset.sum_Ico_eq_sub]
Proof state after:
case h.h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ N ≤ M
Theorem: finsetSum_tendsto_tsum
Proof state before:
case h.h
N : ℕ
f : ℕ → ℂ
hf : Summable f
this✝ : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
M : ℕ
hM : N + 1 ≤ M
⊢ N ≤ M
Tactic:
linarith
Proof state after:
no goals
Theorem: tendsto_coe_atTop
Proof state before:
⊢ Tendsto (fun n => ↑n) atTop atTop
Tactic:
rw [Filter.tendsto_atTop_atTop]
Proof state after:
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑a
Theorem: tendsto_coe_atTop
Proof state before:
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑a
Tactic:
intro b
Proof state after:
b : ℝ
⊢ ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑a
Theorem: tendsto_coe_atTop
Proof state before:
b : ℝ
⊢ ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑a
Tactic:
use ⌊b⌋.toNat + 1
Proof state after:
case h
b : ℝ
⊢ ∀ (a : ℕ), ⌊b⌋.toNat + 1 ≤ a → b ≤ ↑a
Theorem: tendsto_coe_atTop
Proof state before:
case h
b : ℝ
⊢ ∀ (a : ℕ), ⌊b⌋.toNat + 1 ≤ a → b ≤ ↑a
Tactic:
intro a ha
Proof state after:
case h
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
⊢ b ≤ ↑a
Theorem: tendsto_coe_atTop
Proof state before:
case h
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
⊢ b ≤ ↑a
Tactic:
by_cases a_zero : a = 0
Proof state after:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : a = 0
⊢ b ≤ ↑a

case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
⊢ b ≤ ↑a