Theorem: bound_I2 (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have key a : ‖𝓕 ψ (a / (2 * π))‖ ≤ W21.norm ψ * (1 + (a / (2 * π)) ^ 2)⁻¹ := decay_bounds_key ψ _
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have twopi : 0 ≤ 2 * π := by simp [pi_nonneg]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have l3 : Integrable (fun a ↦ (1 + (a / (2 * π)) ^ 2)⁻¹) := integrable_inv_one_add_sq.comp_div (by norm_num [pi_ne_zero])
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have l2 : IntegrableOn (fun i ↦ W21.norm ψ * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-Real.log x)) := by
  exact (l3.const_mul _).integrableOn
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
have l5 : 0 ≤ᵐ[volume] fun a ↦ (1 + (a / (2 * π)) ^ 2)⁻¹ := by apply eventually_of_forall ; intro x ; positivity
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ‖∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))‖ ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
refine (norm_integral_le_integral_norm _).trans <| (setIntegral_mono l1 l2 key).trans ?_
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (x : ℝ) in Ici (-x.log), W21.norm ψ.toFun * (1 + (x / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (x : ℝ) in Ici (-x.log), W21.norm ψ.toFun * (1 + (x / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
rw [integral_mul_left]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ W21.norm ψ.toFun * ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ W21.norm ψ.toFun * ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ W21.norm ψ.toFun * (2 * π ^ 2)
Tactic:
gcongr
State after:
case a0
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 0 ≤ W21.norm ψ.toFun

case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2

State before:
case a0
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 0 ≤ W21.norm ψ.toFun

case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2
Tactic:
apply W21.norm_nonneg
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (a : ℝ) in Ici (-x.log), (1 + (a / (2 * π)) ^ 2)⁻¹ ∂volume ≤ 2 * π ^ 2
Tactic:
refine (setIntegral_le_integral l3 l5).trans ?_
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (x : ℝ), (1 + (x / (2 * π)) ^ 2)⁻¹ ≤ 2 * π ^ 2

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ ∫ (x : ℝ), (1 + (x / (2 * π)) ^ 2)⁻¹ ≤ 2 * π ^ 2
Tactic:
rw [Measure.integral_comp_div (fun x => (1 + x ^ 2)⁻¹) (2 * π)]
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ |2 * π| • ∫ (y : ℝ), (1 + y ^ 2)⁻¹ ≤ 2 * π ^ 2

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ |2 * π| • ∫ (y : ℝ), (1 + y ^ 2)⁻¹ ≤ 2 * π ^ 2
Tactic:
simp [abs_eq_self.mpr twopi]
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 2 * π * π ≤ 2 * π ^ 2

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 2 * π * π ≤ 2 * π ^ 2
Tactic:
ring_nf
State after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ π ^ 2 * 2 ≤ π ^ 2 * 2

State before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
l5 : 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ π ^ 2 * 2 ≤ π ^ 2 * 2
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
⊢ 0 ≤ 2 * π
Tactic:
simp [pi_nonneg]
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
⊢ 2 * π ≠ 0
Tactic:
norm_num [pi_ne_zero]
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
⊢ IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
Tactic:
exact (l3.const_mul _).integrableOn
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
Tactic:
refine ((l3.const_mul (W21.norm ψ)).mono' ?_ ?_).integrableOn
State after:
case refine_1
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ AEStronglyMeasurable (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) volume

case refine_2
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ∀ᵐ (a : ℝ), ‖‖𝓕 ψ.toFun (a / (2 * π))‖‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹

State before:
case refine_1
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ AEStronglyMeasurable (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) volume
Tactic:
apply Continuous.aestronglyMeasurable
State after:
case refine_1.hf
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ Continuous fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖

State before:
case refine_1.hf
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ Continuous fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖
Tactic:
continuity
State after:
no goals

State before:
case refine_2
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ∀ᵐ (a : ℝ), ‖‖𝓕 ψ.toFun (a / (2 * π))‖‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
Tactic:
simp only [norm_norm, key]
State after:
case refine_2
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ∀ᵐ (a : ℝ), True

State before:
case refine_2
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
⊢ ∀ᵐ (a : ℝ), True
Tactic:
simp
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
⊢ 0 ≤ᶠ[ae volume] fun a => (1 + (a / (2 * π)) ^ 2)⁻¹
Tactic:
apply eventually_of_forall
State after:
case hp
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
⊢ ∀ (x : ℝ), 0 x ≤ (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) x

State before:
case hp
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x.log)) volume
⊢ ∀ (x : ℝ), 0 x ≤ (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) x
Tactic:
intro x
State after:
case hp
n : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x✝ : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x✝.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x✝.log)) volume
x : ℝ
⊢ 0 x ≤ (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) x

State before:
case hp
n : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x✝ : ℝ
ψ : W21
key : ∀ (a : ℝ), ‖𝓕 ψ.toFun (a / (2 * π))‖ ≤ W21.norm ψ.toFun * (1 + (a / (2 * π)) ^ 2)⁻¹
twopi : 0 ≤ 2 * π
l3 : Integrable (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) volume
l2 : IntegrableOn (fun i => W21.norm ψ.toFun * (1 + (i / (2 * π)) ^ 2)⁻¹) (Ici (-x✝.log)) volume
l1 : IntegrableOn (fun i => ‖𝓕 ψ.toFun (i / (2 * π))‖) (Ici (-x✝.log)) volume
x : ℝ
⊢ 0 x ≤ (fun a => (1 + (a / (2 * π)) ^ 2)⁻¹) x
Tactic:
positivity
State after:
no goals