ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>One F<VAR>NormOneClass F<VAR>c : E<VAR>l : Filter α<GOAL>(fun _x => c) =O[l] fun _x => 1
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>F'' : Type u_10<VAR>Norm E<VAR>Norm F<VAR>NormedAddCommGroup F''<VAR>f : α → E<VAR>l : Filter α<VAR>One F<VAR>NormOneClass F<VAR>c : F''<VAR>hc : c ≠ 0<GOAL>(f =o[l] fun _x => c) ↔ f =o[l] fun _x => 1
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>f' : α → E'<VAR>l : Filter α<VAR>One F<VAR>NormOneClass F<GOAL>(f' =o[l] fun _x => 1) ↔ Filter.Tendsto f' l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>l : Filter α<VAR>One F<VAR>NormOneClass F<GOAL>(f =O[l] fun _x => 1) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>l : Filter α<VAR>One F<VAR>NormOneClass F<GOAL>(fun _x => 1) =o[l] f ↔ Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>f' : α → E'<VAR>l : Filter α<VAR>One F<VAR>NormOneClass F<VAR>c : E'<VAR>h : Filter.Tendsto f' l (𝓝 c)<GOAL>f' =O[l] fun _x => 1
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>F' : Type u_7<VAR>Norm E<VAR>Norm F<VAR>SeminormedAddCommGroup F'<VAR>f : α → E<VAR>g' : α → F'<VAR>l : Filter α<VAR>One F<VAR>NormOneClass F<VAR>hfg : f =O[l] g'<VAR>y : F'<VAR>hg : Filter.Tendsto g' l (𝓝 y)<GOAL>f =O[l] fun _x => 1
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>One F<VAR>NormOneClass F<VAR>TopologicalSpace α<VAR>a : α<GOAL>(f =O[𝓝[≠] a] fun x => 1) ↔ f =O[𝓝 a] fun x => 1
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>l : Filter α<VAR>c : F''<VAR>hc : c ≠ 0<GOAL>(f'' =o[l] fun _x => c) ↔ Filter.Tendsto f'' l (𝓝 0)
<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>c : F''<VAR>hc : c ≠ 0<GOAL>(fun x => x) =o[𝓝 0] fun _x => c
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F'' : Type u_10<VAR>Norm E<VAR>NormedAddCommGroup F''<VAR>f : α → E<VAR>l : Filter α<VAR>h : Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>c : F''<VAR>hc : c ≠ 0<GOAL>f =O[l] fun _x => c
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>l : Filter α<VAR>y : E''<VAR>h : Filter.Tendsto f'' l (𝓝 y)<VAR>c : F''<VAR>hc : c ≠ 0<GOAL>f'' =O[l] fun _x => c
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>f : α → E<VAR>l : Filter α<VAR>c : F<VAR>h : f =O[l] fun _x => c<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F'' : Type u_10<VAR>Norm E<VAR>NormedAddCommGroup F''<VAR>f : α → E<VAR>l : Filter α<VAR>c : F''<VAR>hc : c ≠ 0<GOAL>(f =O[l] fun _x => c) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>l : Filter α<VAR>c : F''<GOAL>(f'' =O[l] fun _x => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f'' x‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F'' : Type u_10<VAR>Norm E<VAR>NormedAddCommGroup F''<VAR>f : α → E<VAR>g'' : α → F''<VAR>l : Filter α<VAR>h : ∀ᶠ (x : α) in l, g'' x ≠ 0<GOAL>f =O[l] g'' ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x‖ / ‖g'' x‖
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>E'' : Type u_9<VAR>SeminormedAddCommGroup E'<VAR>NormedAddCommGroup E''<VAR>f' : α → E'<VAR>l : Filter α<VAR>c : E''<VAR>hc : c ≠ 0<GOAL>(fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l : Filter α<VAR>hfg : f'' =O[l] g''<VAR>hg : Filter.Tendsto g'' l (𝓝 0)<GOAL>Filter.Tendsto f'' l (𝓝 0)
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l : Filter α<VAR>hfg : f'' =o[l] g''<VAR>hg : Filter.Tendsto g'' l (𝓝 0)<GOAL>Filter.Tendsto f'' l (𝓝 0)
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>SeminormedRing R<VAR>c : R<VAR>f : α → R<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith ‖c‖ l (fun x => c * f x) f
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>SeminormedRing R<VAR>c : R<VAR>f : α → R<VAR>l : Filter α<GOAL>(fun x => c * f x) =O[l] f
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedRing R<VAR>c : ℝ<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → R<VAR>h : Asymptotics.IsBigOWith c l f g<VAR>c' : R<GOAL>Asymptotics.IsBigOWith (‖c'‖ * c) l (fun x => c' * f x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedRing R<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → R<VAR>h : f =O[l] g<VAR>c' : R<GOAL>(fun x => c' * f x) =O[l] g
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>SeminormedRing R<VAR>u : Rˣ<VAR>f : α → R<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith ‖↑u⁻¹‖ l f fun x => ↑u * f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>f : α → 𝕜<VAR>l : Filter α<GOAL>Asymptotics.IsBigOWith ‖c‖⁻¹ l f fun x => c * f x
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>SeminormedRing R<VAR>c : R<VAR>hc : IsUnit c<VAR>f : α → R<VAR>l : Filter α<GOAL>f =O[l] fun x => c * f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>f : α → 𝕜<VAR>l : Filter α<GOAL>f =O[l] fun x => c * f x
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedRing R<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → R<VAR>c : R<VAR>hc : IsUnit c<GOAL>(fun x => c * f x) =O[l] g ↔ f =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>𝕜 : Type u_15<VAR>Norm F<VAR>NormedDivisionRing 𝕜<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c * f x) =O[l] g ↔ f =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedRing R<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → R<VAR>h : f =o[l] g<VAR>c : R<GOAL>(fun x => c * f x) =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedRing R<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → R<VAR>c : R<VAR>hc : IsUnit c<GOAL>(fun x => c * f x) =o[l] g ↔ f =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>𝕜 : Type u_15<VAR>Norm F<VAR>NormedDivisionRing 𝕜<VAR>g : α → F<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c * f x) =o[l] g ↔ f =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>c' : ℝ<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>hc' : 0 ≤ c'<VAR>h : Asymptotics.IsBigOWith c' l f fun x => c * g x<GOAL>Asymptotics.IsBigOWith (c' * ‖c‖) l f g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>h : f =O[l] fun x => c * g x<GOAL>f =O[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>u : Rˣ<VAR>c' : ℝ<VAR>hc' : 0 ≤ c'<VAR>h : Asymptotics.IsBigOWith c' l f g<GOAL>Asymptotics.IsBigOWith (c' * ‖↑u⁻¹‖) l f fun x => ↑u * g x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>c' : ℝ<VAR>hc' : 0 ≤ c'<VAR>h : Asymptotics.IsBigOWith c' l f g<GOAL>Asymptotics.IsBigOWith (c' * ‖c‖⁻¹) l f fun x => c * g x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>hc : IsUnit c<VAR>h : f =O[l] g<GOAL>f =O[l] fun x => c * g x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>h : f =O[l] g<GOAL>f =O[l] fun x => c * g x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>hc : IsUnit c<GOAL>(f =O[l] fun x => c * g x) ↔ f =O[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =O[l] fun x => c * g x) ↔ f =O[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>h : f =o[l] fun x => c * g x<GOAL>f =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>hc : IsUnit c<VAR>h : f =o[l] g<GOAL>f =o[l] fun x => c * g x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>h : f =o[l] g<GOAL>f =o[l] fun x => c * g x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>R : Type u_13<VAR>Norm E<VAR>SeminormedRing R<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → R<VAR>c : R<VAR>hc : IsUnit c<GOAL>(f =o[l] fun x => c * g x) ↔ f =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>l : Filter α<VAR>g : α → 𝕜<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =o[l] fun x => c * g x) ↔ f =o[l] g
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>c₁ c₂ : ℝ<VAR>h₁ : Asymptotics.IsBigOWith c₁ l f₁ g₁<VAR>h₂ : Asymptotics.IsBigOWith c₂ l f₂ g₂<GOAL>Asymptotics.IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =O[l] g₁<VAR>h₂ : f₂ =O[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =O[l] g₁<VAR>h₂ : f₂ =o[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =o[l] g₁<VAR>h₂ : f₂ =O[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =o[l] g₁<VAR>h₂ : f₂ =o[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>c : ℝ<VAR>l : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : Asymptotics.IsBigOWith c l f g<VAR>n : ℕ<GOAL>Asymptotics.IsBigOWith (Nat.casesOn n ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ n) fun x => g x ^ n
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>c : ℝ<VAR>l : Filter α<VAR>NormOneClass R<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : Asymptotics.IsBigOWith c l f g<VAR>n : ℕ<GOAL>Asymptotics.IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>c c' : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>f : α → 𝕜<VAR>g : α → R<VAR>h : Asymptotics.IsBigOWith c l (f ^ n) (g ^ n)<VAR>hn : n ≠ 0<VAR>hc : c ≤ c' ^ n<VAR>hc' : 0 ≤ c'<GOAL>Asymptotics.IsBigOWith c' l f g
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : f =O[l] g<VAR>n : ℕ<GOAL>(fun x => f x ^ n) =O[l] fun x => g x ^ n
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : (f ^ n) =O[l] (g ^ n)<GOAL>f =O[l] g
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : f =o[l] g<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(fun x => f x ^ n) =o[l] fun x => g x ^ n
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>𝕜 : Type u_15<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → R<VAR>n : ℕ<VAR>h : (f ^ n) =o[l] (g ^ n)<VAR>hn : n ≠ 0<GOAL>f =o[l] g
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>NormedDivisionRing 𝕜<VAR>NormedDivisionRing 𝕜'<VAR>c : ℝ<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : Asymptotics.IsBigOWith c l f g<VAR>h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<GOAL>Asymptotics.IsBigOWith c l (fun x => (g x)⁻¹) fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>NormedDivisionRing 𝕜<VAR>NormedDivisionRing 𝕜'<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : f =O[l] g<VAR>h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<GOAL>(fun x => (g x)⁻¹) =O[l] fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>NormedDivisionRing 𝕜<VAR>NormedDivisionRing 𝕜'<VAR>l : Filter α<VAR>f : α → 𝕜<VAR>g : α → 𝕜'<VAR>h : f =o[l] g<VAR>h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0<GOAL>(fun x => (g x)⁻¹) =o[l] fun x => (f x)⁻¹
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>R : Type u_13<VAR>SeminormedAddCommGroup E'<VAR>SeminormedRing R<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>c' : R<GOAL>Asymptotics.IsBigOWith ‖c'‖ l (fun x => c' • f' x) f'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>R : Type u_13<VAR>SeminormedAddCommGroup E'<VAR>SeminormedRing R<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>c' : R<GOAL>(fun x => c' • f' x) =O[l] f'
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>SeminormedRing R<VAR>c : ℝ<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>h : Asymptotics.IsBigOWith c l f' g<VAR>c' : R<GOAL>Asymptotics.IsBigOWith (‖c'‖ * c) l (fun x => c' • f' x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>SeminormedRing R<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>h : f' =O[l] g<VAR>c : R<GOAL>(c • f') =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>R : Type u_13<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>SeminormedRing R<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>h : f' =o[l] g<VAR>c : R<GOAL>(c • f') =o[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>𝕜 : Type u_15<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>NormedDivisionRing 𝕜<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module 𝕜 E'<VAR>BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c • f' x) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>𝕜 : Type u_15<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>NormedDivisionRing 𝕜<VAR>g : α → F<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module 𝕜 E'<VAR>BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c • f' x) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_6<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>SeminormedAddCommGroup E'<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module 𝕜 E'<VAR>BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =O[l] fun x => c • f' x) ↔ f =O[l] f'
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_6<VAR>𝕜 : Type u_15<VAR>Norm E<VAR>SeminormedAddCommGroup E'<VAR>NormedDivisionRing 𝕜<VAR>f : α → E<VAR>f' : α → E'<VAR>l : Filter α<VAR>Module 𝕜 E'<VAR>BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =o[l] fun x => c • f' x) ↔ f =o[l] f'
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>R : Type u_13<VAR>𝕜' : Type u_16<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜'<VAR>c c' : ℝ<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>Module 𝕜' F'<VAR>BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : Asymptotics.IsBigOWith c l k₁ k₂<VAR>h₂ : Asymptotics.IsBigOWith c' l f' g'<GOAL>Asymptotics.IsBigOWith (c * c') l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>R : Type u_13<VAR>𝕜' : Type u_16<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>Module 𝕜' F'<VAR>BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : f' =O[l] g'<GOAL>(fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>R : Type u_13<VAR>𝕜' : Type u_16<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>Module 𝕜' F'<VAR>BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =O[l] k₂<VAR>h₂ : f' =o[l] g'<GOAL>(fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>R : Type u_13<VAR>𝕜' : Type u_16<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>Module 𝕜' F'<VAR>BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =o[l] k₂<VAR>h₂ : f' =O[l] g'<GOAL>(fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>R : Type u_13<VAR>𝕜' : Type u_16<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>SeminormedRing R<VAR>NormedDivisionRing 𝕜'<VAR>f' : α → E'<VAR>g' : α → F'<VAR>l : Filter α<VAR>Module R E'<VAR>BoundedSMul R E'<VAR>Module 𝕜' F'<VAR>BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =o[l] k₂<VAR>h₂ : f' =o[l] g'<GOAL>(fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>C : ι → ℝ<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, Asymptotics.IsBigOWith (C i) l (A i) g<GOAL>Asymptotics.IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E' : Type u_6<VAR>Norm F<VAR>SeminormedAddCommGroup E'<VAR>g : α → F<VAR>l : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, A i =O[l] g<GOAL>(fun x => ∑ i ∈ s, A i x) =O[l] g
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup E'<VAR>SeminormedAddCommGroup F'<VAR>g' : α → F'<VAR>l : Filter α<VAR>ι : Type u_17<VAR>A : ι → α → E'<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, A i =o[l] g'<GOAL>(fun x => ∑ i ∈ s, A i x) =o[l] g'
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>h : f =o[l] g<GOAL>Filter.Tendsto (fun x => f x / g x) l (𝓝 0)
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>𝕜 : Type u_15<VAR>SeminormedAddCommGroup E'<VAR>NormedDivisionRing 𝕜<VAR>Module 𝕜 E'<VAR>BoundedSMul 𝕜 E'<VAR>f : α → E'<VAR>g : α → 𝕜<VAR>l : Filter α<VAR>h : f =o[l] g<GOAL>Filter.Tendsto (fun x => (g x)⁻¹ • f x) l (𝓝 0)
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<GOAL>f =o[l] g ↔ Filter.Tendsto (fun x => f x / g x) l (𝓝 0)
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ (x : α), g x = 0 → f x = 0<GOAL>f =o[l] g ↔ Filter.Tendsto (fun x => f x / g x) l (𝓝 0)
<VAR>α : Type u_1<VAR>F : Type u_4<VAR>E'' : Type u_9<VAR>Norm F<VAR>NormedAddCommGroup E''<VAR>g : α → F<VAR>l : Filter α<VAR>c : E''<VAR>hc : c ≠ 0<GOAL>(fun _x => c) =o[l] g ↔ Filter.Tendsto (fun x => ‖g x‖) l Filter.atTop
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>g'' : α → F''<VAR>l : Filter α<VAR>c : E''<GOAL>(fun _x => c) =o[l] g'' ↔ c = 0 ∨ Filter.Tendsto (norm ∘ g'') l Filter.atTop
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>l : Filter α<VAR>l.NeBot<VAR>d : E''<VAR>c : F''<GOAL>((fun _x => d) =o[l] fun _x => c) ↔ d = 0
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>x : α<GOAL>f'' =o[pure x] g'' ↔ f'' x = 0
<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>c : F''<GOAL>(fun x => c) =o[Bornology.cobounded E''] id
<VAR>E'' : Type u_9<VAR>NormedAddCommGroup E''<VAR>c : E''<GOAL>(fun _x => c) =o[Filter.atTop] id
<VAR>E'' : Type u_9<VAR>NormedAddCommGroup E''<VAR>c : E''<GOAL>(fun _x => c) =o[Filter.atBot] id
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>c : ℝ<VAR>l : Filter α<VAR>u v : α → 𝕜<VAR>h : Asymptotics.IsBigOWith c l u v<GOAL>u / v * v =ᶠ[l] u
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>u v : α → 𝕜<VAR>h : u =O[l] v<GOAL>u / v * v =ᶠ[l] u
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>u v : α → 𝕜<VAR>h : u =o[l] v<GOAL>u / v * v =ᶠ[l] u
<VAR>α : Type u_1<VAR>R : Type u_13<VAR>SeminormedRing R<VAR>c : ℝ<VAR>l : Filter α<VAR>u v : α → R<VAR>φ : α → R<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c<VAR>h : u =ᶠ[l] φ * v<GOAL>Asymptotics.IsBigOWith c l u v
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>c : ℝ<VAR>l : Filter α<VAR>u v : α → 𝕜<VAR>hc : 0 ≤ c<GOAL>Asymptotics.IsBigOWith c l u v ↔ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>c : ℝ<VAR>l : Filter α<VAR>u v : α → 𝕜<VAR>h : Asymptotics.IsBigOWith c l u v<VAR>hc : 0 ≤ c<GOAL>∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>u v : α → 𝕜<GOAL>u =O[l] v ↔ ∃ φ, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v
<VAR>α : Type u_1<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>l : Filter α<VAR>u v : α → 𝕜<GOAL>u =o[l] v ↔ ∃ φ, Filter.Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v
<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>h : f =O[l] g<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x / g x‖
<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<GOAL>f =O[l] g ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x / g x‖
<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0<VAR>c : 𝕜<VAR>H : Filter.Tendsto (f / g) l (𝓝 c)<GOAL>f =O[l] g
<VAR>α : Type u_17<VAR>E : Type u_18<VAR>𝕜 : Type u_19<VAR>NormedAddCommGroup E<VAR>NormedField 𝕜<VAR>u : α → E<VAR>v : α → 𝕜<VAR>l : Filter α<VAR>y : 𝕜<VAR>huv : u =o[l] v<VAR>hv : Filter.Tendsto v l (𝓝 y)<GOAL>Filter.Tendsto u l (𝓝 0)
<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>m n : ℕ<VAR>h : m < n<GOAL>(fun x => x ^ n) =o[𝓝 0] fun x => x ^ m
<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>m n : ℕ<VAR>h : m < n<GOAL>(fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ m
<VAR>𝕜 : Type u_15<VAR>NormedDivisionRing 𝕜<VAR>n : ℕ<VAR>h : 1 < n<GOAL>(fun x => x ^ n) =o[𝓝 0] fun x => x
<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>n : ℕ<VAR>h : 1 < n<GOAL>(fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x
<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f : E'' → F''<VAR>s : Set E''<VAR>x₀ : E''<VAR>n : ℕ<VAR>h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n<VAR>hx₀ : x₀ ∈ s<VAR>hn : n ≠ 0<GOAL>f x₀ = 0