Theorem: decay_bounds_aux (PrimeNumberTheoremAnd/Wiener.lean)

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
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

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]
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)⁻¹

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
State after:
no goals