internlm/Lean-Github huggingface dataset:
Theorem: second_fourier
Proof state before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝¹ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this✝ : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
this : Tendsto (fun x => Complex.abs (cexp (c * ↑x)) / Complex.abs c) atTop (𝓝 (0 / Complex.abs c))
⊢ Tendsto (fun x => ‖f x‖) atTop (𝓝 0)
Tactic:
simpa [f, f'] using this
Proof state after:
no goals
Theorem: second_fourier
Proof state before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝¹ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this✝ : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
this : Tendsto (fun x => x * (1 - σ')) atTop atBot
⊢ Tendsto (fun a => Complex.abs (cexp (c * ↑a))) atTop (𝓝 0)
Tactic:
simpa [Complex.abs_exp, mul_comm (1 - σ'), c]
Proof state after:
no goals
Theorem: second_fourier
Proof state before:
n : ℕ
A a b c✝ d u x✝ y t✝ σ'✝ : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
x σ' : ℝ
hx : 0 < x
hσ : 1 < σ'
t : ℝ
this✝ : ∀ (u : ℝ), -↑u * (↑σ' - 1) + 2 * ↑π * -(↑t * (↑u / (2 * ↑π))) * I = (1 - ↑σ' - ↑t * I) * ↑u
c : ℂ := 1 - ↑σ' - ↑t * I
this : c ≠ 0
f' : ℝ → ℂ := fun u => cexp (c * ↑u)
f : ℝ → ℂ := fun u => f' u / c
hderiv : ∀ u ∈ Ici (-x.log), HasDerivAt f (f' u) u
⊢ 1 - σ' < 0
Tactic:
linarith
Proof state after:
no goals
Theorem: one_add_sq_pos
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℝ
⊢ 1 ≤ 1 + u ^ 2
Tactic:
simpa using sq_nonneg u
Proof state after:
no goals
Theorem: decay_bounds_key
Proof 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 _
Proof 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)⁻¹
Theorem: decay_bounds_key
Proof 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]
Proof 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)⁻¹
Theorem: decay_bounds_key
Proof 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
Proof 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)⁻¹
Theorem: decay_bounds_key
Proof 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
Proof 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)⁻¹
Theorem: decay_bounds_key
Proof 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
Proof 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)⁻¹
Theorem: decay_bounds_key
Proof 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
Proof 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)⁻¹
Theorem: decay_bounds_key
Proof 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]
Proof 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‖
Theorem: decay_bounds_key
Proof 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
Proof 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‖
Theorem: decay_bounds_key
Proof 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 _
Proof 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
Theorem: decay_bounds_key
Proof 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]
Proof 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‖
Theorem: decay_bounds_key
Proof 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
Proof state after:
no goals
Theorem: decay_bounds_key
Proof 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
Proof 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)‖
Theorem: decay_bounds_key
Proof 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]
Proof state after:
no goals
Theorem: decay_bounds_key
Proof 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
Proof state after:
no goals
Theorem: decay_bounds_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
hf : AEStronglyMeasurable f volume
h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹
⊢ ∫ (t : ℝ), ‖f t‖ ≤ π * A
Tactic:
have l1 : Integrable (fun x ↦ A * (1 + x ^ 2)⁻¹) := integrable_inv_one_add_sq.const_mul A
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
hf : AEStronglyMeasurable f volume
h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹
l1 : Integrable (fun x => A * (1 + x ^ 2)⁻¹) volume
⊢ ∫ (t : ℝ), ‖f t‖ ≤ π * A
Theorem: decay_bounds_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
hf : AEStronglyMeasurable f volume
h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹
l1 : Integrable (fun x => A * (1 + x ^ 2)⁻¹) volume
⊢ ∫ (t : ℝ), ‖f t‖ ≤ π * A
Tactic:
simp_rw [← integral_univ_inv_one_add_sq, mul_comm, ← integral_mul_left]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
hf : AEStronglyMeasurable f volume
h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹
l1 : Integrable (fun x => A * (1 + x ^ 2)⁻¹) volume
⊢ ∫ (t : ℝ), ‖f t‖ ≤ ∫ (a : ℝ), A * (1 + a ^ 2)⁻¹
Theorem: decay_bounds_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
hf : AEStronglyMeasurable f volume
h : ∀ (t : ℝ), ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹
l1 : Integrable (fun x => A * (1 + x ^ 2)⁻¹) volume
⊢ ∫ (t : ℝ), ‖f t‖ ≤ ∫ (a : ℝ), A * (1 + a ^ 2)⁻¹
Tactic:
exact integral_mono (l1.mono' hf (eventually_of_forall h)).norm l1 h
Proof state after:
no goals
Theorem: decay_bounds_W21
Proof 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
Proof 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)
Theorem: decay_bounds_W21
Proof 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
Proof 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)
Theorem: decay_bounds_W21
Proof 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'
Proof 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)
Theorem: decay_bounds_W21
Proof 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
Proof 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)
Theorem: decay_bounds_W21
Proof 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 _ * _ ≤ _
Proof 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)
Theorem: decay_bounds_W21
Proof 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]
Proof 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)⁻¹
Theorem: decay_bounds_W21
Proof 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
Proof state after:
no goals
Theorem: decay_bounds_W21
Proof 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
Proof 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 * π)
Theorem: decay_bounds_W21
Proof 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
Proof state after:
no goals
Theorem: decay_bounds_W21
Proof 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
Proof 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)⁻¹
Theorem: decay_bounds_W21
Proof 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]
Proof 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)
Theorem: decay_bounds_W21
Proof 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
Proof state after:
no goals
Theorem: decay_bounds_W21
Proof 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
Proof 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)⁻¹
Theorem: decay_bounds_W21
Proof 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]
Proof 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)