Theorem: MellinOfSmooth1c (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id
Tactic:
have h := MellinOfDeltaSpikeAt1_asymp diffΨ suppΨ mass_one
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id
Tactic:
rw [Asymptotics.isBigO_iff] at h ⊢
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Tactic:
obtain ⟨c, hc⟩ := h
State after:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖

State before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Tactic:
use c
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Tactic:
filter_upwards [hc, Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < 1)] with ε hε hε'
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1‖ ≤ c * ‖id ε‖

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1‖ ≤ c * ‖id ε‖
Tactic:
simp_rw [MellinOfSmooth1a Ψ diffΨ suppΨ hε'.1 (s := 1) (by norm_num), mul_one]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖1 / 1 * 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖1 / 1 * 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
Tactic:
simpa using hε
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ 0 < 1
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ 0 < re 1
Tactic:
norm_num
State after:
no goals