Theorem: decay_bounds_key (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
have l1 : 0 < 1 + u ^ 2 := one_add_sq_pos _
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
have l2 : 1 + u ^ 2 = ‖(1 : ℂ) + u ^ 2‖ := by
  norm_cast ; simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self.2 l1.le]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
have l3 : ‖1 / ((4 : ℂ) * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹ := by simp
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
have key := fourierIntegral_self_add_deriv_deriv f u
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
simp only [Function.iterate_succ _ 1, Function.iterate_one, Function.comp_apply] at key
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) u) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) u) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
rw [F_sub f.hf (f.hf''.const_mul (1 / (4 * ↑π ^ 2)))] at key
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ ≤ ‖f‖ * (1 + u ^ 2)⁻¹
Tactic:
rw [← div_eq_mul_inv, le_div_iff l1, mul_comm, l2, ← norm_mul, key, sub_eq_add_neg]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u + -𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ ‖f‖

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u + -𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ ‖f‖
Tactic:
apply norm_add_le _ _ |>.trans
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖-𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ ‖f‖

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖-𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ ‖f‖
Tactic:
change _ ≤ W21.norm _
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖-𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ W21.norm fun v => f.toFun v

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖-𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u‖ ≤ W21.norm fun v => f.toFun v
Tactic:
rw [norm_neg, F_mul, norm_mul, W21.norm]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖1 / (4 * ↑π ^ 2)‖ * ‖𝓕 (fun x => deriv (deriv f.toFun) x) u‖ ≤
    (∫ (v : ℝ), ‖f.toFun v‖) + (4 * π ^ 2)⁻¹ * ∫ (v : ℝ), ‖deriv (deriv fun v => f.toFun v) v‖

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
l3 : ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
key : (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 f.toFun u - 𝓕 (fun x => 1 / (4 * ↑π ^ 2) * deriv (deriv f.toFun) x) u
⊢ ‖𝓕 f.toFun u‖ + ‖1 / (4 * ↑π ^ 2)‖ * ‖𝓕 (fun x => deriv (deriv f.toFun) x) u‖ ≤
    (∫ (v : ℝ), ‖f.toFun v‖) + (4 * π ^ 2)⁻¹ * ∫ (v : ℝ), ‖deriv (deriv fun v => f.toFun v) v‖
Tactic:
gcongr <;> apply VectorFourier.norm_fourierIntegral_le_integral_norm
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
⊢ 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
Tactic:
norm_cast
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
⊢ 1 + u ^ 2 = ‖↑(1 + u ^ 2)‖

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
⊢ 1 + u ^ 2 = ‖↑(1 + u ^ 2)‖
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs_ofReal, abs_eq_self.2 l1.le]
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
u : ℝ
l1 : 0 < 1 + u ^ 2
l2 : 1 + u ^ 2 = ‖1 + ↑u ^ 2‖
⊢ ‖1 / (4 * ↑π ^ 2)‖ ≤ (4 * π ^ 2)⁻¹
Tactic:
simp
State after:
no goals