Theorem: integrable_log_over_pow (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ioi ↑N) volume
Tactic:
apply IntegrableOn.mono_set (hst := Set.Ioi_subset_Ici <| le_refl (N : ℝ))
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume
Tactic:
apply LocallyIntegrableOn.integrableOn_of_isBigO_atTop (g := fun x ↦ x ^ (r / 2 - 1))
State after:
case hf
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ LocallyIntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume

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)

case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume

State before:
case hf
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ LocallyIntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume
Tactic:
apply ContinuousOn.abs ?_ |>.mul ?_ |>.locallyIntegrableOn (by simp)
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => x ^ (r - 1)) (Ici ↑N)

r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => |x.log|) (Ici ↑N)

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ MeasurableSet (Ici ↑N)
Tactic:
simp
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => x ^ (r - 1)) (Ici ↑N)
Tactic:
apply ContinuousOn.rpow (by fun_prop) (by fun_prop)
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, x ≠ 0 ∨ 0 < r - 1

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, x ≠ 0 ∨ 0 < r - 1
Tactic:
intro x hx
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0 ∨ 0 < r - 1

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0 ∨ 0 < r - 1
Tactic:
left
State after:
case h
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0

State before:
case h
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0
Tactic:
contrapose! Npos with h
State after:
case h
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0

State before:
case h
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0
Tactic:
exact_mod_cast h ▸ mem_Ici.mp hx
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun t => t) (Ici ↑N)
Tactic:
fun_prop
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun t => r - 1) (Ici ↑N)
Tactic:
fun_prop
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => |x.log|) (Ici ↑N)
Tactic:
apply continuous_id.continuousOn.log ?_ |>.abs
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, id x ≠ 0

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, id x ≠ 0
Tactic:
intro x hx
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ id x ≠ 0

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ id x ≠ 0
Tactic:
simp only [id_eq]
State after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0
Tactic:
contrapose! Npos with h
State after:
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0

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
State after:
no goals

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
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)

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
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)

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
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)

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)
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)

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
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)

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
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)

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
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ 0 < -r / 2
Tactic:
linarith
State after:
no goals

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
State after:
no goals

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])
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

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
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ 0 < ↑N
Tactic:
simp [Npos]
State after:
no goals

State before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ r / 2 - 1 < -1
Tactic:
linarith [rneg]
State after:
no goals