-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma continuousOn_term (n : ℕ) :
    ContinuousOn (fun x ↦ term (n + 1) x) (Ici 1)

Proof state:
case h_cont.h.refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ x ^ (s + 1) ≠ 0

Tactic:
exact (rpow_pos_of_pos ((Nat.cast_pos.mpr (by simp)).trans hx.1) _).ne'

Result:
no goals

Proof state:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 2 ≤ s + 1

Tactic:
linarith

Result:
no goals

Proof state:
case h_cont
n : ℕ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)),
    ContinuousOn (fun x => (a - ↑(n + 1)) / a ^ (x + 1)) (Ici 1)

Tactic:
rw [ae_restrict_iff' measurableSet_Ioc]

Result:
case h_cont
n : ℕ
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ContinuousOn (fun x_1 => (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)

Proof state:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (s + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

Tactic:
rw [ae_restrict_iff' measurableSet_Ioc]

Result:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Proof state:
n : ℕ
⊢ 0 < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
⊢ ContinuousOn (fun x => ∫ (x_1 : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x_1 - ↑(n + 1)) / x_1 ^ (x + 1) ∂volume) (Ici 1)

Tactic:
apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))

Result:
case hF_meas
n : ℕ
⊢ ∀ x ∈ Ici 1,
    AEStronglyMeasurable (fun a => (a - ↑(n + 1)) / a ^ (x + 1)) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))

case h_bound
n : ℕ
⊢ ∀ x ∈ Ici 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (x + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

case bound_integrable
n : ℕ
⊢ Integrable (fun x => (x - ↑(n + 1)) / x ^ 2) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))

case h_cont
n : ℕ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)),
    ContinuousOn (fun x => (a - ↑(n + 1)) / a ^ (x + 1)) (Ici 1)

Proof state:
n : ℕ
⊢ ↑(n + 1) ≤ ↑(n + 1) + 1

Tactic:
linarith

Result:
no goals

Proof state:
n : ℕ
⊢ ContinuousOn (fun x => term (n + 1) x) (Ici 1)

Tactic:
simp only [term, intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]

Result:
n : ℕ
⊢ ContinuousOn (fun x => ∫ (x_1 : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x_1 - ↑(n + 1)) / x_1 ^ (x + 1) ∂volume) (Ici 1)

Proof state:
case hF_meas
n : ℕ
⊢ ∀ x ∈ Ici 1,
    AEStronglyMeasurable (fun a => (a - ↑(n + 1)) / a ^ (x + 1)) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))

Tactic:
exact fun s hs ↦ (term_welldef (by simp) (zero_lt_one.trans_le hs)).1.1

Result:
no goals

Proof state:
case h_bound.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Tactic:
have : 0 < x := lt_trans (by positivity) hx.1

Result:
case h_bound.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Proof state:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 0 < ↑(n + 1)

Tactic:
positivity

Result:
no goals

Proof state:
case h_cont.h
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ ContinuousOn (fun x_1 => (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
refine continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)

Result:
case h_cont.h.refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ ContinuousAt (fun x_1 => x ^ (x_1 + 1)) s

case h_cont.h.refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ x ^ (s + 1) ≠ 0

Proof state:
case h_bound.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ (x - (↑n + 1)) / x ^ (s + 1) ≤ (x - (↑n + 1)) / x ^ 2

Tactic:
apply div_le_div_of_nonneg_left

Result:
case h_bound.h.ha
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 0 ≤ x - (↑n + 1)

case h_bound.h.hc
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 0 < x ^ 2

case h_bound.h.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ x ^ 2 ≤ x ^ (s + 1)

Proof state:
case bound_integrable
n : ℕ
⊢ IntervalIntegrable (fun x => (x - ↑(n + 1)) / x ^ 2) volume (↑(n + 1)) (↑(n + 1) + 1)

Tactic:
exact_mod_cast term_welldef (by omega : 0 < (n + 1)) zero_lt_one

Result:
no goals

Proof state:
case h_bound.h.ha
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 0 ≤ x - (↑n + 1)

Tactic:
exact_mod_cast sub_nonneg.mpr hx.1.le

Result:
no goals

Proof state:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < s + 1

Tactic:
linarith

Result:
no goals

Proof state:
case h_cont
n : ℕ
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ContinuousOn (fun x_1 => (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
filter_upwards with x hx

Result:
case h_cont.h
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ ContinuousOn (fun x_1 => (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)

Proof state:
case bound_integrable
n : ℕ
⊢ Integrable (fun x => (x - ↑(n + 1)) / x ^ 2) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))

Tactic:
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith)]

Result:
case bound_integrable
n : ℕ
⊢ IntervalIntegrable (fun x => (x - ↑(n + 1)) / x ^ 2) volume (↑(n + 1)) (↑(n + 1) + 1)

Proof state:
case h_bound.h.hc
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 0 < x ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case h_cont.h.refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ ContinuousAt (fun x_1 => x ^ (x_1 + 1)) s

Tactic:
exact continuousAt_const.rpow (continuousAt_id.add continuousAt_const) (Or.inr (by linarith))

Result:
no goals

Proof state:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < n + 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ 0 ≤ x ^ (s + 1)

Tactic:
positivity

Result:
no goals

Proof state:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Tactic:
filter_upwards with x hx

Result:
case h_bound.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Proof state:
case h_bound
n : ℕ
⊢ ∀ x ∈ Ici 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (x + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

Tactic:
intro s (hs : 1 ≤ s)

Result:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (s + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

Proof state:
case h_bound.h.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ x ^ 2 ≤ x ^ (s + 1)

Tactic:
exact rpow_le_rpow_of_exponent_le (le_trans (by simp) hx.1.le) (by linarith)

Result:
no goals

Proof state:
case h_bound.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Tactic:
rw [norm_of_nonneg (div_nonneg (sub_nonneg.mpr hx.1.le) (by positivity)), Nat.cast_add_one]

Result:
case h_bound.h
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 0 < x
⊢ (x - (↑n + 1)) / x ^ (s + 1) ≤ (x - (↑n + 1)) / x ^ 2

Proof state:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 < n + 1

Tactic:
simp

Result:
no goals