Theorem: DeltaSpikeSupport_aux (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
unfold DeltaSpike
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else Ψ (x ^ (1 / ε)) / ε) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else Ψ (x ^ (1 / ε)) / ε) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
simp only [one_div, Function.support_subset_iff, ne_eq, ite_eq_left_iff, not_lt, div_eq_zero_iff,
  not_forall, exists_prop, mem_Icc, and_imp]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 0 ≤ x → ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0) → 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 0 ≤ x → ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0) → 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
intro x hx h
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0)
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0)
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
push_neg at h
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
have := suppΨ <| Function.mem_support.mpr h.1
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : x ^ ε⁻¹ ∈ Icc (1 / 2) 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : x ^ ε⁻¹ ∈ Icc (1 / 2) 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
simp only [one_div, mem_Icc] at this
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
have hl := (le_rpow_inv_iff_of_pos (by norm_num) hx εpos).mp this.1
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2⁻¹ ^ ε ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2⁻¹ ^ ε ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
rw [inv_rpow (by norm_num) ε, ← rpow_neg (by norm_num)] at hl
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
refine ⟨hl, (rpow_inv_le_iff_of_pos ?_ (by norm_num) εpos).mp this.2⟩
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ x
Tactic:
linarith [(by apply rpow_nonneg (by norm_num) : 0 ≤ (2 : ℝ) ^ (-ε))]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 0 ≤ 2⁻¹
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2⁻¹ ^ ε ≤ x
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : (2 ^ ε)⁻¹ ≤ x
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ 2 ^ (-ε)
Tactic:
apply rpow_nonneg (by norm_num)
State after:
no goals