Theorem: DeltaSpikeSupport' (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ DeltaSpike Ψ ε x ≠ 0 → x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
intro h
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
have : (fun x ↦ if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x := by simp [xnonneg]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
rw [← this] at h
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
exact (Function.support_subset_iff.mp <| DeltaSpikeSupport_aux εpos suppΨ) _ h
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
⊢ (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
Tactic:
simp [xnonneg]
State after:
no goals