Theorem: decay_bounds_W21 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
Tactic:
have l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A) := by field_simp ; ring
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
Tactic:
have l1 : ∫ (v : ℝ), ‖f v‖ ≤ π * A := by
  apply decay_bounds_aux f.continuous.aestronglyMeasurable
  simp_rw [← div_eq_mul_inv] ; exact hA
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
Tactic:
have l2 : ∫ (v : ℝ), ‖deriv (deriv f) v‖ ≤ π * A := by
  apply decay_bounds_aux f.deriv.deriv.continuous.aestronglyMeasurable
  simp_rw [← div_eq_mul_inv] ; exact hA'
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ ‖𝓕 f.toFun u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
Tactic:
apply decay_bounds_key f u |>.trans
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ ‖f‖ * (1 + u ^ 2)⁻¹ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ ‖f‖ * (1 + u ^ 2)⁻¹ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
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
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ (W21.norm fun v => f.toFun v) * (1 + u ^ 2)⁻¹ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ (W21.norm fun v => f.toFun v) * (1 + u ^ 2)⁻¹ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)
Tactic:
simp_rw [W21.norm, div_eq_mul_inv, add_mul, l0]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ (∫ (v : ℝ), ‖f.toFun v‖) * (1 + u ^ 2)⁻¹ +
      ((4 * π ^ 2)⁻¹ * ∫ (v : ℝ), ‖deriv (deriv fun v => f.toFun v) v‖) * (1 + u ^ 2)⁻¹ ≤
    π * A * (1 + u ^ 2)⁻¹ + (4 * π ^ 2)⁻¹ * (π * A) * (1 + u ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
l2 : ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
⊢ (∫ (v : ℝ), ‖f.toFun v‖) * (1 + u ^ 2)⁻¹ +
      ((4 * π ^ 2)⁻¹ * ∫ (v : ℝ), ‖deriv (deriv fun v => f.toFun v) v‖) * (1 + u ^ 2)⁻¹ ≤
    π * A * (1 + u ^ 2)⁻¹ + (4 * π ^ 2)⁻¹ * (π * A) * (1 + u ^ 2)⁻¹
Tactic:
gcongr
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
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
⊢ 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
Tactic:
field_simp
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
⊢ A * (4 * π ^ 2) = π * A * (4 * π)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
⊢ A * (4 * π ^ 2) = π * A * (4 * π)
Tactic:
ring
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
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
Tactic:
apply decay_bounds_aux f.continuous.aestronglyMeasurable
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ∀ (t : ℝ), ‖f.toFun t‖ ≤ A * (1 + t ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ∀ (t : ℝ), ‖f.toFun t‖ ≤ A * (1 + t ^ 2)⁻¹
Tactic:
simp_rw [← div_eq_mul_inv]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
⊢ ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
Tactic:
exact hA
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
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ∫ (v : ℝ), ‖deriv (deriv f.toFun) v‖ ≤ π * A
Tactic:
apply decay_bounds_aux f.deriv.deriv.continuous.aestronglyMeasurable
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ∀ (t : ℝ), ‖(W1.deriv f).deriv.toFun t‖ ≤ A * (1 + t ^ 2)⁻¹

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ∀ (t : ℝ), ‖(W1.deriv f).deriv.toFun t‖ ≤ A * (1 + t ^ 2)⁻¹
Tactic:
simp_rw [← div_eq_mul_inv]
State after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ∀ (t : ℝ), ‖(W1.deriv f).deriv.toFun t‖ ≤ A / (1 + t ^ 2)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : W21
hA : ∀ (t : ℝ), ‖f.toFun t‖ ≤ A / (1 + t ^ 2)
hA' : ∀ (t : ℝ), ‖deriv (deriv f.toFun) t‖ ≤ A / (1 + t ^ 2)
u : ℝ
l0 : 1 * (4 * π)⁻¹ * A = (4 * π ^ 2)⁻¹ * (π * A)
l1 : ∫ (v : ℝ), ‖f.toFun v‖ ≤ π * A
⊢ ∀ (t : ℝ), ‖(W1.deriv f).deriv.toFun t‖ ≤ A / (1 + t ^ 2)
Tactic:
exact hA'
State after:
no goals