Theorem: decay_bounds_cor_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
have l1 : HasCompactSupport (fun u : ℝ => ((1 + u ^ 2) : ℝ) * ψ u) := by exact ψ.h2.mul_left
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
have := ψ.h1.continuous
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
obtain ⟨C, hC⟩ := l1.exists_bound_of_continuous (by continuity)
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
⊢ ∃ C, ∀ (u : ℝ), ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
refine ⟨C, fun u => ?_⟩
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
u : ℝ
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C : ℝ
hC : ∀ (x : ℝ), ‖↑(1 + x ^ 2) * ψ.toFun x‖ ≤ C
u : ℝ
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
specialize hC u
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : ‖↑(1 + u ^ 2) * ψ.toFun u‖ ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : ‖↑(1 + u ^ 2) * ψ.toFun u‖ ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
simp only [norm_mul, Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self.mpr (one_add_sq_pos u).le] at hC
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : (1 + u ^ 2) * Complex.abs (ψ.toFun u) ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
C u : ℝ
hC : (1 + u ^ 2) * Complex.abs (ψ.toFun u) ≤ C
⊢ ‖ψ.toFun u‖ ≤ C / (1 + u ^ 2)
Tactic:
rwa [le_div_iff' (one_add_sq_pos _)]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
⊢ HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
Tactic:
exact ψ.h2.mul_left
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
l1 : HasCompactSupport fun u => ↑(1 + u ^ 2) * ψ.toFun u
this : Continuous ψ.toFun
⊢ Continuous fun u => ↑(1 + u ^ 2) * ψ.toFun u
Tactic:
continuity
State after:
no goals