case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => Abs.abs (g x).im) l, (fun x x_1 => x ≤ x_1) x b
⊢ (fun x => Real.exp (arg (f x) * (g x).im)) =Θ[l] fun x => 1
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => Abs.abs (g x).im
⊢ (fun x => Real.exp (arg (f x) * (g x).im)) =Θ[l] fun x => 1
rcases hl with ⟨b, hb⟩
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => Abs.abs (g x).im) l, (fun x x_1 => x ≤ x_1) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x => Abs.abs (arg (f x) * (g x).im)) l, (fun x x_1 => x ≤ x_1) x (π * b)
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => Abs.abs (g x).im) l, (fun x x_1 => x ≤ x_1) x b
⊢ (fun x => Real.exp (arg (f x) * (g x).im)) =Θ[l] fun x => 1
refine' Real.isTheta_exp_comp_one.2 ⟨π * b, _⟩
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (g a).im) b
⊢ ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (arg (f a) * (g a).im)) (π * b)
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => Abs.abs (g x).im) l, (fun x x_1 => x ≤ x_1) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x => Abs.abs (arg (f x) * (g x).im)) l, (fun x x_1 => x ≤ x_1) x (π * b)
rw [eventually_map] at hb⊢
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (g a).im) b
x : α
hx : (fun x x_1 => x ≤ x_1) (Abs.abs (g x).im) b
⊢ (fun x x_1 => x ≤ x_1) (Abs.abs (arg (f x) * (g x).im)) (π * b)
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (g a).im) b
⊢ ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (arg (f a) * (g a).im)) (π * b)
refine' hb.mono fun x hx => _
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (g a).im) b
x : α
hx : (fun x x_1 => x ≤ x_1) (Abs.abs (g x).im) b
⊢ (fun x x_1 => x ≤ x_1) (Abs.abs (arg (f x)) * Abs.abs (g x).im) (π * b)
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (g a).im) b
x : α
hx : (fun x x_1 => x ≤ x_1) (Abs.abs (g x).im) b
⊢ (fun x x_1 => x ≤ x_1) (Abs.abs (arg (f x) * (g x).im)) (π * b)
erw [abs_mul]
no goals
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (Abs.abs (g a).im) b
x : α
hx : (fun x x_1 => x ≤ x_1) (Abs.abs (g x).im) b
⊢ (fun x x_1 => x ≤ x_1) (Abs.abs (arg (f x)) * Abs.abs (g x).im) (π * b)
exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le