Further basic lemmas about asymptotics

@[simp]

theorem Asymptotics.isBigOWith_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ} {f : α → E} {g : α → F} {s : Set α} : IsBigOWith c (Filter.principal s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

theorem Asymptotics.isBigO_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {s : Set α} : f =O[Filter.principal s] g ↔ ∃ (c : ℝ), ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

@[simp]

theorem Asymptotics.isLittleO_principal {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : α → F'} {f'' : α → E''} {s : Set α} : f'' =o[Filter.principal s] g' ↔ ∀ x ∈ s, f'' x = 0

@[simp]

theorem Asymptotics.isBigOWith_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ} {f : α → E} {g : α → F} : IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖

@[simp]

theorem Asymptotics.isBigO_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} : f =O[⊤] g ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

@[simp]

theorem Asymptotics.isLittleO_top {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : α → F'} {f'' : α → E''} : f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0

theorem Asymptotics.isBigOWith_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] [One F] [NormOneClass F] (c : E) (l : Filter α) : IsBigOWith ‖c‖ l (fun (_x : α) => c) fun (_x : α) => 1

theorem Asymptotics.isBigO_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] [One F] [NormOneClass F] (c : E) (l : Filter α) : (fun (_x : α) => c) =O[l] fun (_x : α) => 1

theorem Asymptotics.isLittleO_const_iff_isLittleO_one {α : Type u_1} {E : Type u_3} (F : Type u_4) {F'' : Type u_10} [Norm E] [Norm F] [NormedAddCommGroup F''] {f : α → E} {l : Filter α} [One F] [NormOneClass F] {c : F''} (hc : c ≠ 0) : (f =o[l] fun (_x : α) => c) ↔ f =o[l] fun (_x : α) => 1

@[simp]

theorem Asymptotics.isLittleO_one_iff {α : Type u_1} (F : Type u_4) {E''' : Type u_12} [Norm F] [SeminormedAddGroup E'''] {l : Filter α} [One F] [NormOneClass F] {f : α → E'''} : (f =o[l] fun (_x : α) => 1) ↔ Filter.Tendsto f l (nhds 0)

@[simp]

theorem Asymptotics.isBigO_one_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : α → E} {l : Filter α} [One F] [NormOneClass F] : (f =O[l] fun (_x : α) => 1) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x‖

theorem Filter.IsBoundedUnder.isBigO_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : α → E} {l : Filter α} [One F] [NormOneClass F] : (IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x‖) → f =O[l] fun (_x : α) => 1

Alias of the reverse direction of Asymptotics.isBigO_one_iff.

@[simp]

theorem Asymptotics.isLittleO_one_left_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : α → E} {l : Filter α} [One F] [NormOneClass F] : (fun (_x : α) => 1) =o[l] f ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) l Filter.atTop

theorem Filter.Tendsto.isBigO_one {α : Type u_1} (F : Type u_4) {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} [One F] [NormOneClass F] {c : E'} (h : Tendsto f' l (nhds c)) : f' =O[l] fun (_x : α) => 1

theorem Asymptotics.IsBigO.trans_tendsto_nhds {α : Type u_1} {E : Type u_3} (F : Type u_4) {F' : Type u_7} [Norm E] [Norm F] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} [One F] [NormOneClass F] (hfg : f =O[l] g') {y : F'} (hg : Filter.Tendsto g' l (nhds y)) : f =O[l] fun (_x : α) => 1

theorem Asymptotics.isBigO_one_nhds_ne_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : α → E} [One F] [NormOneClass F] [TopologicalSpace α] {a : α} : (f =O[nhdsWithin a {a}ᶜ] fun (x : α) => 1) ↔ f =O[nhds a] fun (x : α) => 1

The condition f = O[𝓝[≠] a] 1 is equivalent to f = O[𝓝 a] 1.

theorem Asymptotics.isLittleO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {c : F''} (hc : c ≠ 0) : (f'' =o[l] fun (_x : α) => c) ↔ Filter.Tendsto f'' l (nhds 0)

theorem Asymptotics.isLittleO_id_const {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {c : F''} (hc : c ≠ 0) : (fun (x : E'') => x) =o[nhds 0] fun (_x : E'') => c

theorem Filter.IsBoundedUnder.isBigO_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : α → E} {l : Filter α} (h : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) {c : F''} (hc : c ≠ 0) : f =O[l] fun (_x : α) => c

theorem Asymptotics.isBigO_const_of_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {y : E''} (h : Filter.Tendsto f'' l (nhds y)) {c : F''} (hc : c ≠ 0) : f'' =O[l] fun (_x : α) => c

theorem Asymptotics.IsBigO.isBoundedUnder_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {l : Filter α} {c : F} (h : f =O[l] fun (_x : α) => c) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)

theorem Asymptotics.isBigO_const_of_ne {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : α → E} {l : Filter α} {c : F''} (hc : c ≠ 0) : (f =O[l] fun (_x : α) => c) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)

theorem Asymptotics.isBigO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {c : F''} : (f'' =O[l] fun (_x : α) => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f'' x‖

theorem Asymptotics.isBigO_iff_isBoundedUnder_le_div {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : α → E} {g'' : α → F''} {l : Filter α} (h : ∀ᶠ (x : α) in l, g'' x ≠ 0) : f =O[l] g'' ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x‖ / ‖g'' x‖

theorem Asymptotics.isBigO_const_left_iff_pos_le_norm {α : Type u_1} {E' : Type u_6} {E'' : Type u_9} [SeminormedAddCommGroup E'] [NormedAddCommGroup E''] {f' : α → E'} {l : Filter α} {c : E''} (hc : c ≠ 0) : (fun (_x : α) => c) =O[l] f' ↔ ∃ (b : ℝ), 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

(fun x ↦ c) =O[l] f if and only if f is bounded away from zero.

theorem Asymptotics.IsBigO.trans_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α} (hfg : f'' =O[l] g'') (hg : Filter.Tendsto g'' l (nhds 0)) : Filter.Tendsto f'' l (nhds 0)

theorem Asymptotics.IsLittleO.trans_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α} (hfg : f'' =o[l] g'') (hg : Filter.Tendsto g'' l (nhds 0)) : Filter.Tendsto f'' l (nhds 0)

theorem Asymptotics.isLittleO_id_one {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [One F''] [NeZero 1] : (fun (x : E'') => x) =o[nhds 0] 1

theorem Asymptotics.continuousAt_iff_isLittleO {α : Type u_17} {E : Type u_18} [NormedRing E] [NormOneClass E] [TopologicalSpace α] {f : α → E} {x : α} : ContinuousAt f x ↔ (fun (y : α) => f y - f x) =o[nhds x] fun (x : α) => 1

Multiplication

theorem Asymptotics.IsBigO.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → R} {n : ℕ} (hn : n ≠ 0) (h : (f ^ n) =O[l] (g ^ n)) : f =O[l] g

Scalar multiplication

theorem Asymptotics.IsBigOWith.const_smul_self {α : Type u_1} {E' : Type u_6} {R : Type u_13} [SeminormedAddCommGroup E'] [SeminormedRing R] {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (c' : R) : IsBigOWith ‖c'‖ l (fun (x : α) => c' • f' x) f'

theorem Asymptotics.IsBigO.const_smul_self {α : Type u_1} {E' : Type u_6} {R : Type u_13} [SeminormedAddCommGroup E'] [SeminormedRing R] {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (c' : R) : (fun (x : α) => c' • f' x) =O[l] f'

theorem Asymptotics.IsBigOWith.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : IsBigOWith c l f' g) (c' : R) : IsBigOWith (‖c'‖ * c) l (fun (x : α) => c' • f' x) g

theorem Asymptotics.IsBigO.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {g : α → F} {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : f' =O[l] g) (c : R) : (c • f') =O[l] g

theorem Asymptotics.IsLittleO.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {g : α → F} {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : f' =o[l] g) (c : R) : (c • f') =o[l] g

theorem Asymptotics.isBigO_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [Norm F] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c • f' x) =O[l] g ↔ f' =O[l] g

theorem Asymptotics.isLittleO_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [Norm F] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c • f' x) =o[l] g ↔ f' =o[l] g

theorem Asymptotics.isBigO_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [Norm E] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {f : α → E} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (f =O[l] fun (x : α) => c • f' x) ↔ f =O[l] f'

theorem Asymptotics.isLittleO_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [Norm E] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {f : α → E} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (f =o[l] fun (x : α) => c • f' x) ↔ f =o[l] f'

theorem Asymptotics.IsBigOWith.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {c c' : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : IsBigOWith c l k₁ k₂) (h₂ : IsBigOWith c' l f' g') : IsBigOWith (c * c') l (fun (x : α) => k₁ x • f' x) fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsBigO.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =O[l] k₂) (h₂ : f' =O[l] g') : (fun (x : α) => k₁ x • f' x) =O[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsBigO.smul_isLittleO {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =O[l] k₂) (h₂ : f' =o[l] g') : (fun (x : α) => k₁ x • f' x) =o[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsLittleO.smul_isBigO {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') : (fun (x : α) => k₁ x • f' x) =o[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsLittleO.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =o[l] k₂) (h₂ : f' =o[l] g') : (fun (x : α) => k₁ x • f' x) =o[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsBigO.listProd {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {ι : Type u_17} {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ L, f i =O[l] g i) : (fun (x : α) => (List.map (fun (x_1 : ι) => f x_1 x) L).prod) =O[l] fun (x : α) => (List.map (fun (x_1 : ι) => g x_1 x) L).prod

theorem Asymptotics.IsBigO.multisetProd {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [SeminormedCommRing R] [NormedField 𝕜] {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ s, f i =O[l] g i) : (fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) =O[l] fun (x : α) => (Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod

theorem Asymptotics.IsBigO.finsetProd {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [SeminormedCommRing R] [NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ s, f i =O[l] g i) : (fun (x : α) => ∏ i ∈ s, f i x) =O[l] fun (x : α) => ∏ i ∈ s, g i x

theorem Asymptotics.IsLittleO.listProd {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {ι : Type u_17} {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i) : (fun (x : α) => (List.map (fun (x_1 : ι) => f x_1 x) L).prod) =o[l] fun (x : α) => (List.map (fun (x_1 : ι) => g x_1 x) L).prod

theorem Asymptotics.IsLittleO.multisetProd {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [SeminormedCommRing R] [NormedField 𝕜] {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i) (h₂ : ∃ i ∈ s, f i =o[l] g i) : (fun (x : α) => (Multiset.map (fun (x_1 : ι) => f x_1 x) s).prod) =o[l] fun (x : α) => (Multiset.map (fun (x_1 : ι) => g x_1 x) s).prod

theorem Asymptotics.IsLittleO.finsetProd {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [SeminormedCommRing R] [NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i) (h₂ : ∃ i ∈ s, f i =o[l] g i) : (fun (x : α) => ∏ i ∈ s, f i x) =o[l] fun (x : α) => ∏ i ∈ s, g i x

Relation between f = o(g) and f / g → 0

theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜} (h : f =o[l] g) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero {α : Type u_1} {E' : Type u_6} {𝕜 : Type u_15} [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {f : α → E'} {g : α → 𝕜} {l : Filter α} (h : f =o[l] g) : Filter.Tendsto (fun (x : α) => (g x)⁻¹ • f x) l (nhds 0)

theorem Asymptotics.isLittleO_iff_tendsto' {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : f =o[l] g ↔ Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Asymptotics.isLittleO_iff_tendsto {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜} (hgf : ∀ (x : α), g x = 0 → f x = 0) : f =o[l] g ↔ Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Asymptotics.isLittleO_of_tendsto' {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0) → f =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto'.

theorem Asymptotics.isLittleO_of_tendsto {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜} (hgf : ∀ (x : α), g x = 0 → f x = 0) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0) → f =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto.

theorem Asymptotics.isLittleO_const_left_of_ne {α : Type u_1} {F : Type u_4} {E'' : Type u_9} [Norm F] [NormedAddCommGroup E''] {g : α → F} {l : Filter α} {c : E''} (hc : c ≠ 0) : (fun (_x : α) => c) =o[l] g ↔ Filter.Tendsto (fun (x : α) => ‖g x‖) l Filter.atTop

@[simp]

theorem Asymptotics.isLittleO_const_left {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {g'' : α → F''} {l : Filter α} {c : E''} : (fun (_x : α) => c) =o[l] g'' ↔ c = 0 ∨ Filter.Tendsto (norm ∘ g'') l Filter.atTop

@[simp]

theorem Asymptotics.isLittleO_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} [l.NeBot] {d : E''} {c : F''} : ((fun (_x : α) => d) =o[l] fun (_x : α) => c) ↔ d = 0

@[simp]

theorem Asymptotics.isLittleO_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {x : α} : f'' =o[pure x] g'' ↔ f'' x = 0

theorem Asymptotics.isLittleO_const_id_cobounded {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] (c : F'') : (fun (x : E'') => c) =o[Bornology.cobounded E''] id

theorem Asymptotics.isLittleO_const_id_atTop {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') : (fun (_x : ℝ) => c) =o[Filter.atTop] id

theorem Asymptotics.isLittleO_const_id_atBot {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') : (fun (_x : ℝ) => c) =o[Filter.atBot] id

Equivalent definitions of the form ∃ φ, u =ᶠ[l] φ * v in a NormedField.

theorem Asymptotics.isBigOWith_of_eq_mul {α : Type u_1} {R : Type u_13} [SeminormedRing R] {c : ℝ} {l : Filter α} {u v : α → R} (φ : α → R) (hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) (h : u =ᶠ[l] φ * v) : IsBigOWith c l u v

If ‖φ‖ is eventually bounded by c, and u =ᶠ[l] φ * v, then we have IsBigOWith c u v l. This does not require any assumptions on c, which is why we keep this version along with IsBigOWith_iff_exists_eq_mul.

theorem Asymptotics.isBigOWith_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜} (hc : 0 ≤ c) : IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.IsBigOWith.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜} (h : IsBigOWith c l u v) (hc : 0 ≤ c) : ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.isBigO_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜} : u =O[l] v ↔ ∃ (φ : α → 𝕜), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.IsBigO.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜} : u =O[l] v → ∃ (φ : α → 𝕜), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Alias of the forward direction of Asymptotics.isBigO_iff_exists_eq_mul.

theorem Asymptotics.isLittleO_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜} : u =o[l] v ↔ ∃ (φ : α → 𝕜), Filter.Tendsto φ l (nhds 0) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.IsLittleO.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜} : u =o[l] v → ∃ (φ : α → 𝕜), Filter.Tendsto φ l (nhds 0) ∧ u =ᶠ[l] φ * v

Alias of the forward direction of Asymptotics.isLittleO_iff_exists_eq_mul.

Miscellaneous lemmas

theorem Asymptotics.div_isBoundedUnder_of_isBigO {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜} (h : f =O[l] g) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x / g x‖

theorem Asymptotics.isBigO_iff_div_isBoundedUnder {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : f =O[l] g ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x / g x‖

theorem Asymptotics.isBigO_of_div_tendsto_nhds {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) (c : 𝕜) (H : Filter.Tendsto (f / g) l (nhds c)) : f =O[l] g

theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto {α : Type u_17} {E : Type u_18} {𝕜 : Type u_19} [NormedAddCommGroup E] [NormedField 𝕜] {u : α → E} {v : α → 𝕜} {l : Filter α} {y : 𝕜} (huv : u =o[l] v) (hv : Filter.Tendsto v l (nhds y)) : Filter.Tendsto u l (nhds 0)

theorem Asymptotics.isLittleO_pow_pow {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {m n : ℕ} (h : m < n) : (fun (x : 𝕜) => x ^ n) =o[nhds 0] fun (x : 𝕜) => x ^ m

theorem Asymptotics.isLittleO_norm_pow_norm_pow {E' : Type u_6} [SeminormedAddCommGroup E'] {m n : ℕ} (h : m < n) : (fun (x : E') => ‖x‖ ^ n) =o[nhds 0] fun (x : E') => ‖x‖ ^ m

theorem Asymptotics.isLittleO_pow_id {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {n : ℕ} (h : 1 < n) : (fun (x : 𝕜) => x ^ n) =o[nhds 0] fun (x : 𝕜) => x

theorem Asymptotics.isLittleO_norm_pow_id {E' : Type u_6} [SeminormedAddCommGroup E'] {n : ℕ} (h : 1 < n) : (fun (x : E') => ‖x‖ ^ n) =o[nhds 0] fun (x : E') => x

theorem Asymptotics.IsBigO.eq_zero_of_norm_pow_within {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E'' → F''} {s : Set E''} {x₀ : E''} {n : ℕ} (h : f =O[nhdsWithin x₀ s] fun (x : E'') => ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s) (hn : n ≠ 0) : f x₀ = 0

theorem Asymptotics.IsBigO.eq_zero_of_norm_pow {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E'' → F''} {x₀ : E''} {n : ℕ} (h : f =O[nhds x₀] fun (x : E'') => ‖x - x₀‖ ^ n) (hn : n ≠ 0) : f x₀ = 0

theorem Asymptotics.isLittleO_pow_sub_pow_sub {E' : Type u_6} [SeminormedAddCommGroup E'] (x₀ : E') {n m : ℕ} (h : n < m) : (fun (x : E') => ‖x - x₀‖ ^ m) =o[nhds x₀] fun (x : E') => ‖x - x₀‖ ^ n

theorem Asymptotics.isLittleO_pow_sub_sub {E' : Type u_6} [SeminormedAddCommGroup E'] (x₀ : E') {m : ℕ} (h : 1 < m) : (fun (x : E') => ‖x - x₀‖ ^ m) =o[nhds x₀] fun (x : E') => x - x₀

theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₂ x - f₁ x

theorem Asymptotics.IsBigOWith.right_le_add_of_lt_one {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₁ x + f₂ x

theorem Asymptotics.IsLittleO.right_isBigO_sub {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun (x : α) => f₂ x - f₁ x

theorem Asymptotics.IsLittleO.right_isBigO_add {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun (x : α) => f₁ x + f₂ x

theorem Asymptotics.IsLittleO.right_isBigO_add' {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] (f₂ + f₁)

theorem Asymptotics.bound_of_isBigO_cofinite {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : α → E} {g'' : α → F''} (h : f =O[Filter.cofinite] g'') : ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

If f x = O(g x) along cofinite, then there exists a positive constant C such that ‖f x‖ ≤ C * ‖g x‖ whenever g x ≠ 0.

theorem Asymptotics.isBigO_cofinite_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} (h : ∀ (x : α), g'' x = 0 → f'' x = 0) : f'' =O[Filter.cofinite] g'' ↔ ∃ (C : ℝ), ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

theorem Asymptotics.bound_of_isBigO_nat_atTop {E : Type u_3} {E'' : Type u_9} [Norm E] [NormedAddCommGroup E''] {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[Filter.atTop] g'') : ∃ C > 0, ∀ ⦃x : ℕ⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

theorem Asymptotics.isBigO_nat_atTop_iff {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : ℕ → E''} {g : ℕ → F''} (h : ∀ (x : ℕ), g x = 0 → f x = 0) : f =O[Filter.atTop] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

theorem Asymptotics.isBigO_one_nat_atTop_iff {E'' : Type u_9} [NormedAddCommGroup E''] {f : ℕ → E''} : (f =O[Filter.atTop] fun (_n : ℕ) => 1) ↔ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

theorem Asymptotics.isBigOWith_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ι → Type u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i} {C : ℝ} (hC : 0 ≤ C) : IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith C l (fun (x : α) => f x i) g'

@[simp]

theorem Asymptotics.isBigO_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ι → Type u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i} : f =O[l] g' ↔ ∀ (i : ι), (fun (x : α) => f x i) =O[l] g'

@[simp]

theorem Asymptotics.isLittleO_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ι → Type u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i} : f =o[l] g' ↔ ∀ (i : ι), (fun (x : α) => f x i) =o[l] g'

theorem Asymptotics.IsBigO.natCast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =O[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =O[Filter.atTop] fun (n : ℕ) => g ↑n

@[deprecated Asymptotics.IsBigO.natCast_atTop (since := "2024-04-17")]

theorem Asymptotics.IsBigO.nat_cast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =O[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =O[Filter.atTop] fun (n : ℕ) => g ↑n

Alias of Asymptotics.IsBigO.natCast_atTop.

theorem Asymptotics.IsLittleO.natCast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =o[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =o[Filter.atTop] fun (n : ℕ) => g ↑n

@[deprecated Asymptotics.IsLittleO.natCast_atTop (since := "2024-04-17")]

theorem Asymptotics.IsLittleO.nat_cast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =o[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =o[Filter.atTop] fun (n : ℕ) => g ↑n

Alias of Asymptotics.IsLittleO.natCast_atTop.

theorem Asymptotics.isBigO_atTop_iff_eventually_exists {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {α : Type u_17} [SemilatticeSup α] [Nonempty α] {f : α → E} {g : α → F} : f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

theorem Asymptotics.isBigO_atTop_iff_eventually_exists_pos {G : Type u_5} {G' : Type u_8} [Norm G] [SeminormedAddCommGroup G'] {α : Type u_17} [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} : f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

theorem Asymptotics.isBigO_mul_iff_isBigO_div {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f g h : α → 𝕜} (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

theorem summable_of_isBigO {ι : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : f =O[Filter.cofinite] g) : Summable f

theorem summable_of_isBigO_nat {E : Type u_1} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ} (hg : Summable g) (h : f =O[Filter.atTop] g) : Summable f

theorem Asymptotics.IsBigO.comp_summable_norm {ι : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {g : ι → E} (hf : f =O[nhds 0] id) (hg : Summable fun (x : ι) => ‖g x‖) : Summable fun (x : ι) => ‖f (g x)‖

theorem PartialHomeomorph.isBigOWith_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} {C : ℝ} : Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Transfer IsBigOWith over a PartialHomeomorph.

theorem PartialHomeomorph.isBigO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} : f =O[nhds b] g ↔ (f ∘ ↑e) =O[nhds (↑e.symm b)] (g ∘ ↑e)

Transfer IsBigO over a PartialHomeomorph.

theorem PartialHomeomorph.isLittleO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} : f =o[nhds b] g ↔ (f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)

Transfer IsLittleO over a PartialHomeomorph.

theorem Homeomorph.isBigOWith_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ} : Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)

Transfer IsBigOWith over a Homeomorph.

theorem Homeomorph.isBigO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} : f =O[nhds b] g ↔ (f ∘ ⇑e) =O[nhds (e.symm b)] (g ∘ ⇑e)

Transfer IsBigO over a Homeomorph.

theorem Homeomorph.isLittleO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} : f =o[nhds b] g ↔ (f ∘ ⇑e) =o[nhds (e.symm b)] (g ∘ ⇑e)

Transfer IsLittleO over a Homeomorph.

theorem ContinuousOn.isBigOWith_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} {c : F} [SeminormedAddGroup E] [Norm F] (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) : Asymptotics.IsBigOWith (sSup (Norm.norm '' (f '' s)) / ‖c‖) (Filter.principal s) f fun (x : α) => c

theorem ContinuousOn.isBigO_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} {c : F} [SeminormedAddGroup E] [Norm F] (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) : f =O[Filter.principal s] fun (x : α) => c

theorem ContinuousOn.isBigOWith_rev_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) : Asymptotics.IsBigOWith (‖c‖ / sInf (Norm.norm '' (f '' s))) (Filter.principal s) (fun (x : α) => c) f

theorem ContinuousOn.isBigO_rev_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) : (fun (x : α) => c) =O[Filter.principal s] f

theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι : Type u_1} {𝕜 : Type u_2} {𝔸 : Type u_3} [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [BoundedSMul 𝕜 𝔸] {l : Filter ι} {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Filter.Tendsto ε l (nhds 0)) (hf : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) : Filter.Tendsto (ε • f) l (nhds 0)

The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.