Theorem: MellinOfDeltaSpikeAt1_asymp (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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Tactic:
have := ofReal_zero ▸ diff.isBigO_sub
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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 1 - (𝓜 (fun x => ↑(Ψ x)) 0 - 1)) =O[𝓝[>] 0] fun x => x - 0
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 1 - (𝓜 (fun x => ↑(Ψ x)) 0 - 1)) =O[𝓝[>] 0] fun x => x - 0
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Tactic:
simp only [sub_sub_sub_cancel_right, sub_zero] at this
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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
⊢ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
Tactic:
convert this
State after:
case h.e'_7.h.h.e'_6
𝕂 : 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = 𝓜 (fun x => ↑(Ψ x)) 0

State before:
case h.e'_7.h.h.e'_6
𝕂 : 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = 𝓜 (fun x => ↑(Ψ x)) 0
Tactic:
simp only [MellinTransform, zero_sub, sub_right_inj, cpow_neg_one, ← div_eq_mul_inv, ← ofReal_div]
State after:
case h.e'_7.h.h.e'_6
𝕂 : 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)

State before:
case h.e'_7.h.h.e'_6
𝕂 : 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
Tactic:
rw [← ofReal_one, ← mass_one]
State after:
case h.e'_7.h.h.e'_6
𝕂 : 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ ↑(∫ (x : ℝ) in Ioi 0, Ψ x / x) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)

State before:
case h.e'_7.h.h.e'_6
𝕂 : 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
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ ↑(∫ (x : ℝ) in Ioi 0, Ψ x / x) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
Tactic:
convert integral_ofReal.symm
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
⊢ DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
Tactic:
apply DifferentiableAt.differentiableWithinAt
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
⊢ DifferentiableAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) 0

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
⊢ DifferentiableAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) 0
Tactic:
simp only [differentiableAt_sub_const_iff, MellinTransform_eq]
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
⊢ DifferentiableAt ℝ (fun y => mellin (fun x => ↑(Ψ x)) ↑y) 0

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
⊢ DifferentiableAt ℝ (fun y => mellin (fun x => ↑(Ψ x)) ↑y) 0
Tactic:
refine DifferentiableAt.comp_ofReal ?_
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
⊢ DifferentiableAt ℂ (mellin fun x => ↑(Ψ x)) ↑0

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
⊢ DifferentiableAt ℂ (mellin fun x => ↑(Ψ x)) ↑0
Tactic:
refine mellin_differentiableAt_of_isBigO_rpow (a := 1) (b := -1) ?_ ?_ (by simp) ?_ (by simp)
State after:
case h.refine_1
𝕂 : 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
⊢ LocallyIntegrableOn (fun x => ↑(Ψ x)) (Ioi 0) volume

case h.refine_2
𝕂 : 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 x => ↑(Ψ x)) =O[atTop] fun x => x ^ (-1)

case h.refine_3
𝕂 : 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 x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => x ^ (- -1)

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
⊢ (↑0).re < 1
Tactic:
simp
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
⊢ -1 < (↑0).re
Tactic:
simp
State after:
no goals

State before:
case h.refine_1
𝕂 : 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
⊢ LocallyIntegrableOn (fun x => ↑(Ψ x)) (Ioi 0) volume
Tactic:
apply (Continuous.continuousOn ?_).locallyIntegrableOn (by simp)
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
⊢ Continuous fun x => ↑(Ψ 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
⊢ Continuous fun x => ↑(Ψ x)
Tactic:
have := diffΨ.continuous
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
this : Continuous Ψ
⊢ Continuous fun x => ↑(Ψ 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
this : Continuous Ψ
⊢ Continuous fun x => ↑(Ψ x)
Tactic:
continuity
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
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals

State before:
case h.refine_2
𝕂 : 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 x => ↑(Ψ x)) =O[atTop] fun x => x ^ (-1)
Tactic:
apply Asymptotics.IsBigO.trans_le (g' := fun _ ↦ (0 : ℝ)) ?_ (by simp)
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
⊢ (fun x => ↑(Ψ x)) =O[atTop] fun x => 0

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 x => ↑(Ψ x)) =O[atTop] fun x => 0
Tactic:
apply BigO_zero_atTop_of_support_in_Icc (a := 1 / 2) (b := 2)
State after:
case fSupp
𝕂 : 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
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2

State before:
case fSupp
𝕂 : 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
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2
Tactic:
rwa [Ψ.support_ofReal]
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
⊢ ∀ (x : ℝ), ‖(fun x => 0) x‖ ≤ ‖x ^ (-1)‖
Tactic:
simp
State after:
no goals

State before:
case h.refine_3
𝕂 : 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 x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => x ^ (- -1)
Tactic:
apply Asymptotics.IsBigO.trans_le (g' := fun _ ↦ (0 : ℝ)) ?_ (by simp)
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
⊢ (fun x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => 0

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 x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => 0
Tactic:
apply BigO_zero_atZero_of_support_in_Icc (a := 1 / 2) (b := 2) (ha := (by norm_num))
State after:
case fSupp
𝕂 : 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
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2

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
⊢ ∀ (x : ℝ), ‖(fun x => 0) x‖ ≤ ‖x ^ (- -1)‖
Tactic:
simp
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
f : ℝ → ℂ
⊢ 0 < 1 / 2
Tactic:
norm_num
State after:
no goals