Theorem: Asymptotics.isBigO_mul_iff_isBigO_div (EulerProducts/PNT.lean)

State before:
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x => f x * g x) =O[l] h ↔ g =O[l] fun x => h x / f x
Tactic:
rw [isBigO_iff', isBigO_iff']
State after:
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖

State before:
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Tactic:
refine ⟨fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩⟩ <;>
{ refine H.congr <| Eventually.mp hf <| eventually_of_forall fun x hx ↦ ?_
  rw [norm_mul, norm_div, ← mul_div_assoc, mul_comm]
  have hx' : ‖f x‖ > 0 := norm_pos_iff.mpr hx
  rw [le_div_iff hx', mul_comm] }
State after:
no goals

State before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖
Tactic:
refine H.congr <| Eventually.mp hf <| eventually_of_forall fun x hx ↦ ?_
State after:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h x‖

State before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h x‖
Tactic:
rw [norm_mul, norm_div, ← mul_div_assoc, mul_comm]
State after:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c

State before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c
Tactic:
have hx' : ‖f x‖ > 0 := norm_pos_iff.mpr hx
State after:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
hx' : ‖f x‖ > 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c

State before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
hx' : ‖f x‖ > 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c
Tactic:
rw [le_div_iff hx', mul_comm]
State after:
no goals