case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v → ∃ φ _hφ, u =ᶠ[l] φ * v

case mpr
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ (∃ φ _hφ, u =ᶠ[l] φ * v) → IsBigOWith c l u v
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v ↔ ∃ φ _hφ, u =ᶠ[l] φ * v
constructor
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v → ∃ φ _hφ, u =ᶠ[l] φ * v
intro h
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ _hφ, u =ᶠ[l] (fun x => u x / v x) * v
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ φ _hφ, u =ᶠ[l] φ * v
use fun x => u x / v x
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
⊢ ‖(fun x => u x / v x) y‖ ≤ c
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
⊢ ∃ _hφ, u =ᶠ[l] (fun x => u x / v x) * v
refine' ⟨Eventually.mono h.bound fun y hy => _, h.eventually_mul_div_cancel.symm⟩
no goals
case mp
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
⊢ ‖(fun x => u x / v x) y‖ ≤ c
simpa using div_le_of_nonneg_of_le_mul (norm_nonneg _) hc hy
case mpr.intro.intro
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v
case mpr
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ (∃ φ _hφ, u =ᶠ[l] φ * v) → IsBigOWith c l u v
rintro ⟨φ, hφ, h⟩
no goals
case mpr.intro.intro
α : Type u_1
β : Type ?u.630634
E : Type ?u.630637
F : Type ?u.630640
G : Type ?u.630643
E' : Type ?u.630646
F' : Type ?u.630649
G' : Type ?u.630652
E'' : Type ?u.630655
F'' : Type ?u.630658
G'' : Type ?u.630661
R : Type ?u.630664
R' : Type ?u.630667
𝕜 : Type u_2
𝕜' : Type ?u.630673
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
u v : α → 𝕜
hc : 0 ≤ c
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v
exact isBigOWith_of_eq_mul φ hφ h