Asymptotics
We introduce these relations:
is_O_with c f g l: "f is big O of g along l with constant c";is_O f g l: "f is big O of g along l";is_o f g l: "f is little o of g along l".
Here l is any filter on the domain of f and g, which are assumed to be the same. The codomains
of f and g do not need to be the same; all that is needed that there is a norm associated with
these types, and it is the norm that is compared asymptotically.
The relation is_O_with c is introduced to factor out common algebraic arguments in the proofs of
similar properties of is_O and is_o. Usually proofs outside of this file should use is_O
instead.
Often the ranges of f and g will be the real numbers, in which case the norm is the absolute
value. In general, we have
is_O f g l ↔ is_O (λ x, ∥f x∥) (λ x, ∥g x∥) l,
and similarly for is_o. But our setup allows us to use the notions e.g. with functions
to the integers, rationals, complex numbers, or any normed vector space without mentioning the
norm explicitly.
If f and g are functions to a normed field like the reals or complex numbers and g is always
nonzero, we have
is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0).
In fact, the right-to-left direction holds without the hypothesis on g, and in the other direction
it suffices to assume that f is zero wherever g is. (This generalization is useful in defining
the Fréchet derivative.)
Definitions
This version of the Landau notation is_O_with C f g l where f and g are two functions on
a type α and l is a filter on α, means that eventually for l, ∥f∥ is bounded by C * ∥g∥.
In other words, ∥f∥ / ∥g∥ is eventually bounded by C, modulo division by zero issues that are
avoided by this definition. Probably you want to use is_O instead of this relation.
theorem
asymptotics.is_O_with_iff
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l : filter α} :
Definition of is_O_with. We record it in a lemma as we will set is_O_with to be irreducible
at the end of this file.
def
asymptotics.is_O
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F] :
(α → E) → (α → F) → filter α → Prop
The Landau notation is_O f g l where f and g are two functions on a type α and l is
a filter on α, means that eventually for l, ∥f∥ is bounded by a constant multiple of ∥g∥.
In other words, ∥f∥ / ∥g∥ is eventually bounded, modulo division by zero issues that are avoided
by this definition.
Equations
- asymptotics.is_O f g l = ∃ (c : ℝ), asymptotics.is_O_with c f g l
theorem
asymptotics.is_O_iff_is_O_with
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α} :
asymptotics.is_O f g l ↔ ∃ (c : ℝ), asymptotics.is_O_with c f g l
Definition of is_O in terms of is_O_with. We record it in a lemma as we will set
is_O to be irreducible at the end of this file.
theorem
asymptotics.is_O_iff
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α} :
Definition of is_O in terms of filters. We record it in a lemma as we will set
is_O to be irreducible at the end of this file.
def
asymptotics.is_o
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F] :
(α → E) → (α → F) → filter α → Prop
The Landau notation is_o f g l where f and g are two functions on a type α and l is
a filter on α, means that eventually for l, ∥f∥ is bounded by an arbitrarily small constant
multiple of ∥g∥. In other words, ∥f∥ / ∥g∥ tends to 0 along l, modulo division by zero
issues that are avoided by this definition.
Equations
- asymptotics.is_o f g l = ∀ ⦃c : ℝ⦄, 0 < c → asymptotics.is_O_with c f g l
theorem
asymptotics.is_o_iff_forall_is_O_with
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α} :
asymptotics.is_o f g l ↔ ∀ ⦃c : ℝ⦄, 0 < c → asymptotics.is_O_with c f g l
Definition of is_o in terms of is_O_with. We record it in a lemma as we will set
is_o to be irreducible at the end of this file.
theorem
asymptotics.is_o_iff
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α} :
Definition of is_o in terms of filters. We record it in a lemma as we will set
is_o to be irreducible at the end of this file.
theorem
asymptotics.is_o.def'
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α}
(h : asymptotics.is_o f g l)
{c : ℝ} :
0 < c → asymptotics.is_O_with c f g l
Conversions
theorem
asymptotics.is_O_with.is_O
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l : filter α} :
asymptotics.is_O_with c f g l → asymptotics.is_O f g l
theorem
asymptotics.is_o.is_O_with
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α} :
asymptotics.is_o f g l → asymptotics.is_O_with 1 f g l
theorem
asymptotics.is_o.is_O
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α} :
asymptotics.is_o f g l → asymptotics.is_O f g l
theorem
asymptotics.is_O_with.weaken
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{c c' : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c f g' l → c ≤ c' → asymptotics.is_O_with c' f g' l
theorem
asymptotics.is_O_with.exists_pos
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c f g' l → (∃ (c' : ℝ) (H : 0 < c'), asymptotics.is_O_with c' f g' l)
theorem
asymptotics.is_O.exists_pos
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f g' l → (∃ (c : ℝ) (H : 0 < c), asymptotics.is_O_with c f g' l)
theorem
asymptotics.is_O_with.exists_nonneg
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c f g' l → (∃ (c' : ℝ) (H : 0 ≤ c'), asymptotics.is_O_with c' f g' l)
theorem
asymptotics.is_O.exists_nonneg
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f g' l → (∃ (c : ℝ) (H : 0 ≤ c), asymptotics.is_O_with c f g' l)
Congruence
theorem
asymptotics.is_O_with_congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
c₁ = c₂ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (asymptotics.is_O_with c₁ f₁ g₁ l ↔ asymptotics.is_O_with c₂ f₂ g₂ l)
theorem
asymptotics.is_O_with.congr'
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
c₁ = c₂ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → asymptotics.is_O_with c₁ f₁ g₁ l → asymptotics.is_O_with c₂ f₂ g₂ l
theorem
asymptotics.is_O_with.congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
c₁ = c₂ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → asymptotics.is_O_with c₁ f₁ g₁ l → asymptotics.is_O_with c₂ f₂ g₂ l
theorem
asymptotics.is_O_with.congr_left
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{g : α → F}
{f₁ f₂ : α → E}
{l : filter α} :
(∀ (x : α), f₁ x = f₂ x) → asymptotics.is_O_with c f₁ g l → asymptotics.is_O_with c f₂ g l
theorem
asymptotics.is_O_with.congr_right
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{f : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
(∀ (x : α), g₁ x = g₂ x) → asymptotics.is_O_with c f g₁ l → asymptotics.is_O_with c f g₂ l
theorem
asymptotics.is_O_with.congr_const
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{c₁ c₂ : ℝ}
{l : filter α} :
c₁ = c₂ → asymptotics.is_O_with c₁ f g l → asymptotics.is_O_with c₂ f g l
theorem
asymptotics.is_O_congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (asymptotics.is_O f₁ g₁ l ↔ asymptotics.is_O f₂ g₂ l)
theorem
asymptotics.is_O.congr'
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → asymptotics.is_O f₁ g₁ l → asymptotics.is_O f₂ g₂ l
theorem
asymptotics.is_O.congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
(∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → asymptotics.is_O f₁ g₁ l → asymptotics.is_O f₂ g₂ l
theorem
asymptotics.is_O.congr_left
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{g : α → F}
{f₁ f₂ : α → E}
{l : filter α} :
(∀ (x : α), f₁ x = f₂ x) → asymptotics.is_O f₁ g l → asymptotics.is_O f₂ g l
theorem
asymptotics.is_O.congr_right
{α : Type u_1}
{E : Type u_3}
[has_norm E]
{f g₁ g₂ : α → E}
{l : filter α} :
(∀ (x : α), g₁ x = g₂ x) → asymptotics.is_O f g₁ l → asymptotics.is_O f g₂ l
theorem
asymptotics.is_o_congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (asymptotics.is_o f₁ g₁ l ↔ asymptotics.is_o f₂ g₂ l)
theorem
asymptotics.is_o.congr'
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → asymptotics.is_o f₁ g₁ l → asymptotics.is_o f₂ g₂ l
theorem
asymptotics.is_o.congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
{l : filter α} :
(∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → asymptotics.is_o f₁ g₁ l → asymptotics.is_o f₂ g₂ l
theorem
asymptotics.is_o.congr_left
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{g : α → F}
{f₁ f₂ : α → E}
{l : filter α} :
(∀ (x : α), f₁ x = f₂ x) → asymptotics.is_o f₁ g l → asymptotics.is_o f₂ g l
theorem
asymptotics.is_o.congr_right
{α : Type u_1}
{E : Type u_3}
[has_norm E]
{f g₁ g₂ : α → E}
{l : filter α} :
(∀ (x : α), g₁ x = g₂ x) → asymptotics.is_o f g₁ l → asymptotics.is_o f g₂ l
Filter operations and transitivity
theorem
asymptotics.is_O_with.comp_tendsto
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l : filter α}
(hcfg : asymptotics.is_O_with c f g l)
{k : β → α}
{l' : filter β} :
filter.tendsto k l' l → asymptotics.is_O_with c (f ∘ k) (g ∘ k) l'
theorem
asymptotics.is_O.comp_tendsto
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α}
(hfg : asymptotics.is_O f g l)
{k : β → α}
{l' : filter β} :
filter.tendsto k l' l → asymptotics.is_O (f ∘ k) (g ∘ k) l'
theorem
asymptotics.is_o.comp_tendsto
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l : filter α}
(hfg : asymptotics.is_o f g l)
{k : β → α}
{l' : filter β} :
filter.tendsto k l' l → asymptotics.is_o (f ∘ k) (g ∘ k) l'
theorem
asymptotics.is_O_with.mono
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l l' : filter α} :
asymptotics.is_O_with c f g l' → l ≤ l' → asymptotics.is_O_with c f g l
theorem
asymptotics.is_O.mono
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l l' : filter α} :
asymptotics.is_O f g l' → l ≤ l' → asymptotics.is_O f g l
theorem
asymptotics.is_o.mono
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l l' : filter α} :
asymptotics.is_o f g l' → l ≤ l' → asymptotics.is_o f g l
theorem
asymptotics.is_O_with.trans
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[has_norm E]
[has_norm F]
[has_norm G]
{c c' : ℝ}
{f : α → E}
{g : α → F}
{k : α → G}
{l : filter α} :
asymptotics.is_O_with c f g l → asymptotics.is_O_with c' g k l → 0 ≤ c → asymptotics.is_O_with (c * c') f k l
theorem
asymptotics.is_O.trans
{α : Type u_1}
{E : Type u_3}
{G : Type u_5}
{F' : Type u_7}
[has_norm E]
[has_norm G]
[normed_group F']
{f : α → E}
{k : α → G}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f g' l → asymptotics.is_O g' k l → asymptotics.is_O f k l
theorem
asymptotics.is_o.trans_is_O_with
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[has_norm E]
[has_norm F]
[has_norm G]
{c : ℝ}
{f : α → E}
{g : α → F}
{k : α → G}
{l : filter α} :
asymptotics.is_o f g l → asymptotics.is_O_with c g k l → 0 < c → asymptotics.is_o f k l
theorem
asymptotics.is_o.trans_is_O
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G' : Type u_8}
[has_norm E]
[has_norm F]
[normed_group G']
{f : α → E}
{g : α → F}
{k' : α → G'}
{l : filter α} :
asymptotics.is_o f g l → asymptotics.is_O g k' l → asymptotics.is_o f k' l
theorem
asymptotics.is_O_with.trans_is_o
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[has_norm E]
[has_norm F]
[has_norm G]
{c : ℝ}
{f : α → E}
{g : α → F}
{k : α → G}
{l : filter α} :
asymptotics.is_O_with c f g l → asymptotics.is_o g k l → 0 < c → asymptotics.is_o f k l
theorem
asymptotics.is_O.trans_is_o
{α : Type u_1}
{E : Type u_3}
{G : Type u_5}
{F' : Type u_7}
[has_norm E]
[has_norm G]
[normed_group F']
{f : α → E}
{k : α → G}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f g' l → asymptotics.is_o g' k l → asymptotics.is_o f k l
theorem
asymptotics.is_o.trans
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G' : Type u_8}
[has_norm E]
[has_norm F]
[normed_group G']
{f : α → E}
{g : α → F}
{k' : α → G'}
{l : filter α} :
asymptotics.is_o f g l → asymptotics.is_o g k' l → asymptotics.is_o f k' l
theorem
asymptotics.is_o.trans'
{α : Type u_1}
{E : Type u_3}
{G : Type u_5}
{F' : Type u_7}
[has_norm E]
[has_norm G]
[normed_group F']
{f : α → E}
{k : α → G}
{g' : α → F'}
{l : filter α} :
asymptotics.is_o f g' l → asymptotics.is_o g' k l → asymptotics.is_o f k l
theorem
asymptotics.is_O_with_refl
{α : Type u_1}
{E : Type u_3}
[has_norm E]
(f : α → E)
(l : filter α) :
asymptotics.is_O_with 1 f f l
theorem
asymptotics.is_O_refl
{α : Type u_1}
{E : Type u_3}
[has_norm E]
(f : α → E)
(l : filter α) :
asymptotics.is_O f f l
theorem
asymptotics.is_O_with.trans_le
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[has_norm E]
[has_norm F]
[has_norm G]
{c : ℝ}
{f : α → E}
{g : α → F}
{k : α → G}
{l : filter α} :
asymptotics.is_O_with c f g l → (∀ (x : α), ∥g x∥ ≤ ∥k x∥) → 0 ≤ c → asymptotics.is_O_with c f k l
theorem
asymptotics.is_O.trans_le
{α : Type u_1}
{E : Type u_3}
{G : Type u_5}
{F' : Type u_7}
[has_norm E]
[has_norm G]
[normed_group F']
{f : α → E}
{k : α → G}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f g' l → (∀ (x : α), ∥g' x∥ ≤ ∥k x∥) → asymptotics.is_O f k l
theorem
asymptotics.is_o.trans_le
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[has_norm E]
[has_norm F]
[has_norm G]
{f : α → E}
{g : α → F}
{k : α → G}
{l : filter α} :
asymptotics.is_o f g l → (∀ (x : α), ∥g x∥ ≤ ∥k x∥) → asymptotics.is_o f k l
theorem
asymptotics.is_O_with_bot
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
(c : ℝ)
(f : α → E)
(g : α → F) :
asymptotics.is_O_with c f g ⊥
theorem
asymptotics.is_O_bot
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
(c : ℝ)
(f : α → E)
(g : α → F) :
asymptotics.is_O f g ⊥
theorem
asymptotics.is_o_bot
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
(f : α → E)
(g : α → F) :
asymptotics.is_o f g ⊥
theorem
asymptotics.is_O_with.join
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l l' : filter α} :
asymptotics.is_O_with c f g l → asymptotics.is_O_with c f g l' → asymptotics.is_O_with c f g (l ⊔ l')
theorem
asymptotics.is_O_with.join'
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{c c' : ℝ}
{f : α → E}
{g' : α → F'}
{l l' : filter α} :
asymptotics.is_O_with c f g' l → asymptotics.is_O_with c' f g' l' → asymptotics.is_O_with (max c c') f g' (l ⊔ l')
theorem
asymptotics.is_O.join
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l l' : filter α} :
asymptotics.is_O f g' l → asymptotics.is_O f g' l' → asymptotics.is_O f g' (l ⊔ l')
theorem
asymptotics.is_o.join
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{f : α → E}
{g : α → F}
{l l' : filter α} :
asymptotics.is_o f g l → asymptotics.is_o f g l' → asymptotics.is_o f g (l ⊔ l')
Simplification : norm
@[simp]
theorem
asymptotics.is_O_with_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c f (λ (x : α), ∥g' x∥) l ↔ asymptotics.is_O_with c f g' l
@[simp]
theorem
asymptotics.is_O_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f (λ (x : α), ∥g' x∥) l ↔ asymptotics.is_O f g' l
@[simp]
theorem
asymptotics.is_o_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_o f (λ (x : α), ∥g' x∥) l ↔ asymptotics.is_o f g' l
@[simp]
theorem
asymptotics.is_O_with_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c (λ (x : α), ∥f' x∥) g l ↔ asymptotics.is_O_with c f' g l
@[simp]
theorem
asymptotics.is_O_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O (λ (x : α), ∥f' x∥) g l ↔ asymptotics.is_O f' g l
@[simp]
theorem
asymptotics.is_o_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_o (λ (x : α), ∥f' x∥) g l ↔ asymptotics.is_o f' g l
theorem
asymptotics.is_O_with_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c (λ (x : α), ∥f' x∥) (λ (x : α), ∥g' x∥) l ↔ asymptotics.is_O_with c f' g' l
theorem
asymptotics.is_O_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O (λ (x : α), ∥f' x∥) (λ (x : α), ∥g' x∥) l ↔ asymptotics.is_O f' g' l
theorem
asymptotics.is_o_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_o (λ (x : α), ∥f' x∥) (λ (x : α), ∥g' x∥) l ↔ asymptotics.is_o f' g' l
Simplification: negate
@[simp]
theorem
asymptotics.is_O_with_neg_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c f (λ (x : α), -g' x) l ↔ asymptotics.is_O_with c f g' l
@[simp]
theorem
asymptotics.is_O_neg_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f (λ (x : α), -g' x) l ↔ asymptotics.is_O f g' l
@[simp]
theorem
asymptotics.is_o_neg_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_o f (λ (x : α), -g' x) l ↔ asymptotics.is_o f g' l
@[simp]
theorem
asymptotics.is_O_with_neg_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c (λ (x : α), -f' x) g l ↔ asymptotics.is_O_with c f' g l
@[simp]
theorem
asymptotics.is_O_neg_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O (λ (x : α), -f' x) g l ↔ asymptotics.is_O f' g l
@[simp]
theorem
asymptotics.is_o_neg_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_o (λ (x : α), -f' x) g l ↔ asymptotics.is_o f' g l
Product of functions (right)
theorem
asymptotics.is_O_with_fst_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with 1 f' (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_O_with_snd_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with 1 g' (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_O_fst_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f' (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_O_snd_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O g' (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_O_fst_prod'
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{l : filter α}
{f' : α → E' × F'} :
asymptotics.is_O (λ (x : α), (f' x).fst) f' l
theorem
asymptotics.is_O_snd_prod'
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{l : filter α}
{f' : α → E' × F'} :
asymptotics.is_O (λ (x : α), (f' x).snd) f' l
theorem
asymptotics.is_O_with.prod_rightl
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
{G' : Type u_8}
[has_norm E]
[normed_group F']
[normed_group G']
{c : ℝ}
{f : α → E}
{g' : α → F'}
(k' : α → G')
{l : filter α} :
asymptotics.is_O_with c f g' l → 0 ≤ c → asymptotics.is_O_with c f (λ (x : α), (g' x, k' x)) l
theorem
asymptotics.is_O.prod_rightl
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
{G' : Type u_8}
[has_norm E]
[normed_group F']
[normed_group G']
{f : α → E}
{g' : α → F'}
(k' : α → G')
{l : filter α} :
asymptotics.is_O f g' l → asymptotics.is_O f (λ (x : α), (g' x, k' x)) l
theorem
asymptotics.is_o.prod_rightl
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
{G' : Type u_8}
[has_norm E]
[normed_group F']
[normed_group G']
{f : α → E}
{g' : α → F'}
(k' : α → G')
{l : filter α} :
asymptotics.is_o f g' l → asymptotics.is_o f (λ (x : α), (g' x, k' x)) l
theorem
asymptotics.is_O_with.prod_rightr
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{F' : Type u_7}
[has_norm E]
[normed_group E']
[normed_group F']
{c : ℝ}
{f : α → E}
(f' : α → E')
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c f g' l → 0 ≤ c → asymptotics.is_O_with c f (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_O.prod_rightr
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{F' : Type u_7}
[has_norm E]
[normed_group E']
[normed_group F']
{f : α → E}
(f' : α → E')
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f g' l → asymptotics.is_O f (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_o.prod_rightr
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{F' : Type u_7}
[has_norm E]
[normed_group E']
[normed_group F']
{f : α → E}
(f' : α → E')
{g' : α → F'}
{l : filter α} :
asymptotics.is_o f g' l → asymptotics.is_o f (λ (x : α), (f' x, g' x)) l
theorem
asymptotics.is_O_with.prod_left_same
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O_with c f' k' l → asymptotics.is_O_with c g' k' l → asymptotics.is_O_with c (λ (x : α), (f' x, g' x)) k' l
theorem
asymptotics.is_O_with.prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{c c' : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O_with c f' k' l → asymptotics.is_O_with c' g' k' l → asymptotics.is_O_with (max c c') (λ (x : α), (f' x, g' x)) k' l
theorem
asymptotics.is_O_with.prod_left_fst
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O_with c (λ (x : α), (f' x, g' x)) k' l → asymptotics.is_O_with c f' k' l
theorem
asymptotics.is_O_with.prod_left_snd
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O_with c (λ (x : α), (f' x, g' x)) k' l → asymptotics.is_O_with c g' k' l
theorem
asymptotics.is_O_with_prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O_with c (λ (x : α), (f' x, g' x)) k' l ↔ asymptotics.is_O_with c f' k' l ∧ asymptotics.is_O_with c g' k' l
theorem
asymptotics.is_O.prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O f' k' l → asymptotics.is_O g' k' l → asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l
theorem
asymptotics.is_O.prod_left_fst
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l → asymptotics.is_O f' k' l
theorem
asymptotics.is_O.prod_left_snd
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l → asymptotics.is_O g' k' l
@[simp]
theorem
asymptotics.is_O_prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l ↔ asymptotics.is_O f' k' l ∧ asymptotics.is_O g' k' l
theorem
asymptotics.is_o.prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_o f' k' l → asymptotics.is_o g' k' l → asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l
theorem
asymptotics.is_o.prod_left_fst
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l → asymptotics.is_o f' k' l
theorem
asymptotics.is_o.prod_left_snd
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l → asymptotics.is_o g' k' l
@[simp]
theorem
asymptotics.is_o_prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[normed_group E']
[normed_group F']
[normed_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l ↔ asymptotics.is_o f' k' l ∧ asymptotics.is_o g' k' l
Addition and subtraction
theorem
asymptotics.is_O_with.add
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c₁ f₁ g l → asymptotics.is_O_with c₂ f₂ g l → asymptotics.is_O_with (c₁ + c₂) (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_O.add
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O f₁ g l → asymptotics.is_O f₂ g l → asymptotics.is_O (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_o.add
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o f₁ g l → asymptotics.is_o f₂ g l → asymptotics.is_o (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_o.add_add
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{l : filter α}
{f₁ f₂ : α → E'}
{g₁ g₂ : α → F'} :
asymptotics.is_o f₁ g₁ l → asymptotics.is_o f₂ g₂ l → asymptotics.is_o (λ (x : α), f₁ x + f₂ x) (λ (x : α), ∥g₁ x∥ + ∥g₂ x∥) l
theorem
asymptotics.is_O.add_is_o
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O f₁ g l → asymptotics.is_o f₂ g l → asymptotics.is_O (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_o.add_is_O
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o f₁ g l → asymptotics.is_O f₂ g l → asymptotics.is_O (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_O_with.add_is_o
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c₁ f₁ g l → asymptotics.is_o f₂ g l → c₁ < c₂ → asymptotics.is_O_with c₂ (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_o.add_is_O_with
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E'} :
asymptotics.is_o f₁ g l → asymptotics.is_O_with c₁ f₂ g l → c₁ < c₂ → asymptotics.is_O_with c₂ (λ (x : α), f₁ x + f₂ x) g l
theorem
asymptotics.is_O_with.sub
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c₁ f₁ g l → asymptotics.is_O_with c₂ f₂ g l → asymptotics.is_O_with (c₁ + c₂) (λ (x : α), f₁ x - f₂ x) g l
theorem
asymptotics.is_O_with.sub_is_o
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{c₁ c₂ : ℝ}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c₁ f₁ g l → asymptotics.is_o f₂ g l → c₁ < c₂ → asymptotics.is_O_with c₂ (λ (x : α), f₁ x - f₂ x) g l
theorem
asymptotics.is_O.sub
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O f₁ g l → asymptotics.is_O f₂ g l → asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l
theorem
asymptotics.is_o.sub
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o f₁ g l → asymptotics.is_o f₂ g l → asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l
Lemmas about is_O (f₁ - f₂) g l / is_o (f₁ - f₂) g l treated as a binary relation
theorem
asymptotics.is_O_with.symm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{c : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c (λ (x : α), f₁ x - f₂ x) g l → asymptotics.is_O_with c (λ (x : α), f₂ x - f₁ x) g l
theorem
asymptotics.is_O_with_comm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{c : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c (λ (x : α), f₁ x - f₂ x) g l ↔ asymptotics.is_O_with c (λ (x : α), f₂ x - f₁ x) g l
theorem
asymptotics.is_O.symm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l → asymptotics.is_O (λ (x : α), f₂ x - f₁ x) g l
theorem
asymptotics.is_O_comm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l ↔ asymptotics.is_O (λ (x : α), f₂ x - f₁ x) g l
theorem
asymptotics.is_o.symm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l → asymptotics.is_o (λ (x : α), f₂ x - f₁ x) g l
theorem
asymptotics.is_o_comm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l ↔ asymptotics.is_o (λ (x : α), f₂ x - f₁ x) g l
theorem
asymptotics.is_O_with.triangle
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{c c' : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ f₃ : α → E'} :
asymptotics.is_O_with c (λ (x : α), f₁ x - f₂ x) g l → asymptotics.is_O_with c' (λ (x : α), f₂ x - f₃ x) g l → asymptotics.is_O_with (c + c') (λ (x : α), f₁ x - f₃ x) g l
theorem
asymptotics.is_O.triangle
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ f₃ : α → E'} :
asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l → asymptotics.is_O (λ (x : α), f₂ x - f₃ x) g l → asymptotics.is_O (λ (x : α), f₁ x - f₃ x) g l
theorem
asymptotics.is_o.triangle
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ f₃ : α → E'} :
asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l → asymptotics.is_o (λ (x : α), f₂ x - f₃ x) g l → asymptotics.is_o (λ (x : α), f₁ x - f₃ x) g l
theorem
asymptotics.is_O.congr_of_sub
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l → (asymptotics.is_O f₁ g l ↔ asymptotics.is_O f₂ g l)
theorem
asymptotics.is_o.congr_of_sub
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l → (asymptotics.is_o f₁ g l ↔ asymptotics.is_o f₂ g l)
Zero, one, and other constants
theorem
asymptotics.is_o_zero
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
(g' : α → F')
(l : filter α) :
asymptotics.is_o (λ (x : α), 0) g' l
theorem
asymptotics.is_O_with_zero
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{c : ℝ}
(g' : α → F')
(l : filter α) :
0 ≤ c → asymptotics.is_O_with c (λ (x : α), 0) g' l
theorem
asymptotics.is_O_with_zero'
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
(g : α → F)
(l : filter α) :
asymptotics.is_O_with 0 (λ (x : α), 0) g l
theorem
asymptotics.is_O_zero
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
(g : α → F)
(l : filter α) :
asymptotics.is_O (λ (x : α), 0) g l
theorem
asymptotics.is_O_refl_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
(g' : α → F')
(l : filter α) :
asymptotics.is_O (λ (x : α), f' x - f' x) g' l
theorem
asymptotics.is_o_refl_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
(g' : α → F')
(l : filter α) :
asymptotics.is_o (λ (x : α), f' x - f' x) g' l
theorem
asymptotics.is_O_with_zero_right_iff
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{c : ℝ}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c f' (λ (x : α), 0) l ↔ ∀ᶠ (x : α) in l, f' x = 0
theorem
asymptotics.is_O_zero_right_iff
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{l : filter α} :
asymptotics.is_O f' (λ (x : α), 0) l ↔ ∀ᶠ (x : α) in l, f' x = 0
theorem
asymptotics.is_o_zero_right_iff
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{l : filter α} :
asymptotics.is_o f' (λ (x : α), 0) l ↔ ∀ᶠ (x : α) in l, f' x = 0
theorem
asymptotics.is_O_with_const_const
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
(c : E)
{c' : F'}
(hc' : c' ≠ 0)
(l : filter α) :
theorem
asymptotics.is_O_const_const
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[normed_group F']
(c : E)
{c' : F'}
(hc' : c' ≠ 0)
(l : filter α) :
asymptotics.is_O (λ (x : α), c) (λ (x : α), c') l
theorem
asymptotics.is_O_with_const_one
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
(c : E)
(l : filter α) :
asymptotics.is_O_with ∥c∥ (λ (x : α), c) (λ (x : α), 1) l
theorem
asymptotics.is_O_const_one
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
(c : E)
(l : filter α) :
asymptotics.is_O (λ (x : α), c) (λ (x : α), 1) l
theorem
asymptotics.is_o_const_iff_is_o_one
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
(𝕜 : Type u_11)
[has_norm E]
[normed_group F']
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{c : F'} :
c ≠ 0 → (asymptotics.is_o f (λ (x : α), c) l ↔ asymptotics.is_o f (λ (x : α), 1) l)
theorem
asymptotics.is_o_const_iff
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{l : filter α}
{c : F'} :
c ≠ 0 → (asymptotics.is_o f' (λ (x : α), c) l ↔ filter.tendsto f' l (nhds 0))
theorem
asymptotics.is_o_id_const
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{c : F'} :
c ≠ 0 → asymptotics.is_o (λ (x : E'), x) (λ (x : E'), c) (nhds 0)
theorem
asymptotics.is_O_const_of_tendsto
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{l : filter α}
{y : E'}
(h : filter.tendsto f' l (nhds y))
{c : F'} :
c ≠ 0 → asymptotics.is_O f' (λ (x : α), c) l
theorem
asymptotics.is_o_one_iff
{α : Type u_1}
{E' : Type u_6}
(𝕜 : Type u_11)
[normed_group E']
[normed_field 𝕜]
{f' : α → E'}
{l : filter α} :
asymptotics.is_o f' (λ (x : α), 1) l ↔ filter.tendsto f' l (nhds 0)
theorem
asymptotics.is_O_one_of_tendsto
{α : Type u_1}
{E' : Type u_6}
(𝕜 : Type u_11)
[normed_group E']
[normed_field 𝕜]
{f' : α → E'}
{l : filter α}
{y : E'} :
filter.tendsto f' l (nhds y) → asymptotics.is_O f' (λ (x : α), 1) l
theorem
asymptotics.is_O.trans_tendsto_nhds
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
(𝕜 : Type u_11)
[has_norm E]
[normed_group F']
[normed_field 𝕜]
{f : α → E}
{g' : α → F'}
{l : filter α}
(hfg : asymptotics.is_O f g' l)
{y : F'} :
filter.tendsto g' l (nhds y) → asymptotics.is_O f (λ (x : α), 1) l
theorem
asymptotics.is_O.trans_tendsto
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O f' g' l → filter.tendsto g' l (nhds 0) → filter.tendsto f' l (nhds 0)
theorem
asymptotics.is_o.trans_tendsto
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_o f' g' l → filter.tendsto g' l (nhds 0) → filter.tendsto f' l (nhds 0)
Multiplication by a constant
theorem
asymptotics.is_O_with_const_mul_self
{α : Type u_1}
{R : Type u_9}
[normed_ring R]
(c : R)
(f : α → R)
(l : filter α) :
asymptotics.is_O_with ∥c∥ (λ (x : α), c * f x) f l
theorem
asymptotics.is_O_const_mul_self
{α : Type u_1}
{R : Type u_9}
[normed_ring R]
(c : R)
(f : α → R)
(l : filter α) :
asymptotics.is_O (λ (x : α), c * f x) f l
theorem
asymptotics.is_O_with.const_mul_left
{α : Type u_1}
{F : Type u_4}
{R : Type u_9}
[has_norm F]
[normed_ring R]
{c : ℝ}
{g : α → F}
{l : filter α}
{f : α → R}
(h : asymptotics.is_O_with c f g l)
(c' : R) :
asymptotics.is_O_with (∥c'∥ * c) (λ (x : α), c' * f x) g l
theorem
asymptotics.is_O.const_mul_left
{α : Type u_1}
{F : Type u_4}
{R : Type u_9}
[has_norm F]
[normed_ring R]
{g : α → F}
{l : filter α}
{f : α → R}
(h : asymptotics.is_O f g l)
(c' : R) :
asymptotics.is_O (λ (x : α), c' * f x) g l
theorem
asymptotics.is_O_with_self_const_mul'
{α : Type u_1}
{R : Type u_9}
[normed_ring R]
(u : units R)
(f : α → R)
(l : filter α) :
theorem
asymptotics.is_O_with_self_const_mul
{α : Type u_1}
{𝕜 : Type u_11}
[normed_field 𝕜]
(c : 𝕜)
(hc : c ≠ 0)
(f : α → 𝕜)
(l : filter α) :
asymptotics.is_O_with ∥c∥⁻¹ f (λ (x : α), c * f x) l
theorem
asymptotics.is_O_self_const_mul'
{α : Type u_1}
{R : Type u_9}
[normed_ring R]
{c : R}
(hc : is_unit c)
(f : α → R)
(l : filter α) :
asymptotics.is_O f (λ (x : α), c * f x) l
theorem
asymptotics.is_O_self_const_mul
{α : Type u_1}
{𝕜 : Type u_11}
[normed_field 𝕜]
(c : 𝕜)
(hc : c ≠ 0)
(f : α → 𝕜)
(l : filter α) :
asymptotics.is_O f (λ (x : α), c * f x) l
theorem
asymptotics.is_O_const_mul_left_iff'
{α : Type u_1}
{F : Type u_4}
{R : Type u_9}
[has_norm F]
[normed_ring R]
{g : α → F}
{l : filter α}
{f : α → R}
{c : R} :
is_unit c → (asymptotics.is_O (λ (x : α), c * f x) g l ↔ asymptotics.is_O f g l)
theorem
asymptotics.is_O_const_mul_left_iff
{α : Type u_1}
{F : Type u_4}
{𝕜 : Type u_11}
[has_norm F]
[normed_field 𝕜]
{g : α → F}
{l : filter α}
{f : α → 𝕜}
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_O (λ (x : α), c * f x) g l ↔ asymptotics.is_O f g l)
theorem
asymptotics.is_o.const_mul_left
{α : Type u_1}
{F : Type u_4}
{R : Type u_9}
[has_norm F]
[normed_ring R]
{g : α → F}
{l : filter α}
{f : α → R}
(h : asymptotics.is_o f g l)
(c : R) :
asymptotics.is_o (λ (x : α), c * f x) g l
theorem
asymptotics.is_o_const_mul_left_iff'
{α : Type u_1}
{F : Type u_4}
{R : Type u_9}
[has_norm F]
[normed_ring R]
{g : α → F}
{l : filter α}
{f : α → R}
{c : R} :
is_unit c → (asymptotics.is_o (λ (x : α), c * f x) g l ↔ asymptotics.is_o f g l)
theorem
asymptotics.is_o_const_mul_left_iff
{α : Type u_1}
{F : Type u_4}
{𝕜 : Type u_11}
[has_norm F]
[normed_field 𝕜]
{g : α → F}
{l : filter α}
{f : α → 𝕜}
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_o (λ (x : α), c * f x) g l ↔ asymptotics.is_o f g l)
theorem
asymptotics.is_O_with.of_const_mul_right
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{c' : ℝ}
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
0 ≤ c' → asymptotics.is_O_with c' f (λ (x : α), c * g x) l → asymptotics.is_O_with (c' * ∥c∥) f g l
theorem
asymptotics.is_O.of_const_mul_right
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
asymptotics.is_O f (λ (x : α), c * g x) l → asymptotics.is_O f g l
theorem
asymptotics.is_O_with.const_mul_right'
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{u : units R}
{c' : ℝ} :
0 ≤ c' → asymptotics.is_O_with c' f g l → asymptotics.is_O_with (c' * ∥↑u⁻¹∥) f (λ (x : α), ↑u * g x) l
theorem
asymptotics.is_O_with.const_mul_right
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{g : α → 𝕜}
{c : 𝕜}
(hc : c ≠ 0)
{c' : ℝ} :
0 ≤ c' → asymptotics.is_O_with c' f g l → asymptotics.is_O_with (c' * ∥c∥⁻¹) f (λ (x : α), c * g x) l
theorem
asymptotics.is_O.const_mul_right'
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
is_unit c → asymptotics.is_O f g l → asymptotics.is_O f (λ (x : α), c * g x) l
theorem
asymptotics.is_O.const_mul_right
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{g : α → 𝕜}
{c : 𝕜} :
c ≠ 0 → asymptotics.is_O f g l → asymptotics.is_O f (λ (x : α), c * g x) l
theorem
asymptotics.is_O_const_mul_right_iff'
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
is_unit c → (asymptotics.is_O f (λ (x : α), c * g x) l ↔ asymptotics.is_O f g l)
theorem
asymptotics.is_O_const_mul_right_iff
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{g : α → 𝕜}
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_O f (λ (x : α), c * g x) l ↔ asymptotics.is_O f g l)
theorem
asymptotics.is_o.of_const_mul_right
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
asymptotics.is_o f (λ (x : α), c * g x) l → asymptotics.is_o f g l
theorem
asymptotics.is_o.const_mul_right'
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
is_unit c → asymptotics.is_o f g l → asymptotics.is_o f (λ (x : α), c * g x) l
theorem
asymptotics.is_o.const_mul_right
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{g : α → 𝕜}
{c : 𝕜} :
c ≠ 0 → asymptotics.is_o f g l → asymptotics.is_o f (λ (x : α), c * g x) l
theorem
asymptotics.is_o_const_mul_right_iff'
{α : Type u_1}
{E : Type u_3}
{R : Type u_9}
[has_norm E]
[normed_ring R]
{f : α → E}
{l : filter α}
{g : α → R}
{c : R} :
is_unit c → (asymptotics.is_o f (λ (x : α), c * g x) l ↔ asymptotics.is_o f g l)
theorem
asymptotics.is_o_const_mul_right_iff
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_11}
[has_norm E]
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{g : α → 𝕜}
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_o f (λ (x : α), c * g x) l ↔ asymptotics.is_o f g l)
Multiplication
theorem
asymptotics.is_O_with.mul
{α : Type u_1}
{R : Type u_9}
{𝕜 : Type u_11}
[normed_ring R]
[normed_field 𝕜]
{l : filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → 𝕜}
{c₁ c₂ : ℝ} :
asymptotics.is_O_with c₁ f₁ g₁ l → asymptotics.is_O_with c₂ f₂ g₂ l → asymptotics.is_O_with (c₁ * c₂) (λ (x : α), f₁ x * f₂ x) (λ (x : α), g₁ x * g₂ x) l
theorem
asymptotics.is_O.mul
{α : Type u_1}
{R : Type u_9}
{𝕜 : Type u_11}
[normed_ring R]
[normed_field 𝕜]
{l : filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → 𝕜} :
asymptotics.is_O f₁ g₁ l → asymptotics.is_O f₂ g₂ l → asymptotics.is_O (λ (x : α), f₁ x * f₂ x) (λ (x : α), g₁ x * g₂ x) l
theorem
asymptotics.is_O.mul_is_o
{α : Type u_1}
{R : Type u_9}
{𝕜 : Type u_11}
[normed_ring R]
[normed_field 𝕜]
{l : filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → 𝕜} :
asymptotics.is_O f₁ g₁ l → asymptotics.is_o f₂ g₂ l → asymptotics.is_o (λ (x : α), f₁ x * f₂ x) (λ (x : α), g₁ x * g₂ x) l
theorem
asymptotics.is_o.mul_is_O
{α : Type u_1}
{R : Type u_9}
{𝕜 : Type u_11}
[normed_ring R]
[normed_field 𝕜]
{l : filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → 𝕜} :
asymptotics.is_o f₁ g₁ l → asymptotics.is_O f₂ g₂ l → asymptotics.is_o (λ (x : α), f₁ x * f₂ x) (λ (x : α), g₁ x * g₂ x) l
theorem
asymptotics.is_o.mul
{α : Type u_1}
{R : Type u_9}
{𝕜 : Type u_11}
[normed_ring R]
[normed_field 𝕜]
{l : filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → 𝕜} :
asymptotics.is_o f₁ g₁ l → asymptotics.is_o f₂ g₂ l → asymptotics.is_o (λ (x : α), f₁ x * f₂ x) (λ (x : α), g₁ x * g₂ x) l
Scalar multiplication
theorem
asymptotics.is_O_with.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_11}
[has_norm F]
[normed_group E']
[normed_field 𝕜]
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
(h : asymptotics.is_O_with c f' g l)
(c' : 𝕜) :
asymptotics.is_O_with (∥c'∥ * c) (λ (x : α), c' • f' x) g l
theorem
asymptotics.is_O_const_smul_left_iff
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_11}
[has_norm F]
[normed_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_O (λ (x : α), c • f' x) g l ↔ asymptotics.is_O f' g l)
theorem
asymptotics.is_o_const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_11}
[has_norm F]
[normed_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
(h : asymptotics.is_o f' g l)
(c : 𝕜) :
asymptotics.is_o (λ (x : α), c • f' x) g l
theorem
asymptotics.is_o_const_smul_left_iff
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_11}
[has_norm F]
[normed_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_o (λ (x : α), c • f' x) g l ↔ asymptotics.is_o f' g l)
theorem
asymptotics.is_O_const_smul_right
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{𝕜 : Type u_11}
[has_norm E]
[normed_group E']
[normed_field 𝕜]
{f : α → E}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_O f (λ (x : α), c • f' x) l ↔ asymptotics.is_O f f' l)
theorem
asymptotics.is_o_const_smul_right
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{𝕜 : Type u_11}
[has_norm E]
[normed_group E']
[normed_field 𝕜]
{f : α → E}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜} :
c ≠ 0 → (asymptotics.is_o f (λ (x : α), c • f' x) l ↔ asymptotics.is_o f f' l)
theorem
asymptotics.is_O_with.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_11}
[normed_group E']
[normed_group F']
[normed_field 𝕜]
{c c' : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜 F']
{k₁ k₂ : α → 𝕜} :
asymptotics.is_O_with c k₁ k₂ l → asymptotics.is_O_with c' f' g' l → asymptotics.is_O_with (c * c') (λ (x : α), k₁ x • f' x) (λ (x : α), k₂ x • g' x) l
theorem
asymptotics.is_O.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_11}
[normed_group E']
[normed_group F']
[normed_field 𝕜]
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜 F']
{k₁ k₂ : α → 𝕜} :
asymptotics.is_O k₁ k₂ l → asymptotics.is_O f' g' l → asymptotics.is_O (λ (x : α), k₁ x • f' x) (λ (x : α), k₂ x • g' x) l
theorem
asymptotics.is_O.smul_is_o
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_11}
[normed_group E']
[normed_group F']
[normed_field 𝕜]
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜 F']
{k₁ k₂ : α → 𝕜} :
asymptotics.is_O k₁ k₂ l → asymptotics.is_o f' g' l → asymptotics.is_o (λ (x : α), k₁ x • f' x) (λ (x : α), k₂ x • g' x) l
theorem
asymptotics.is_o.smul_is_O
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_11}
[normed_group E']
[normed_group F']
[normed_field 𝕜]
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜 F']
{k₁ k₂ : α → 𝕜} :
asymptotics.is_o k₁ k₂ l → asymptotics.is_O f' g' l → asymptotics.is_o (λ (x : α), k₁ x • f' x) (λ (x : α), k₂ x • g' x) l
theorem
asymptotics.is_o.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_11}
[normed_group E']
[normed_group F']
[normed_field 𝕜]
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜 F']
{k₁ k₂ : α → 𝕜} :
asymptotics.is_o k₁ k₂ l → asymptotics.is_o f' g' l → asymptotics.is_o (λ (x : α), k₁ x • f' x) (λ (x : α), k₂ x • g' x) l
Sum
theorem
asymptotics.is_O_with.sum
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{ι : Type u_13}
{A : ι → α → E'}
{C : ι → ℝ}
{s : finset ι} :
(∀ (i : ι), i ∈ s → asymptotics.is_O_with (C i) (A i) g l) → asymptotics.is_O_with (s.sum (λ (i : ι), C i)) (λ (x : α), s.sum (λ (i : ι), A i x)) g l
theorem
asymptotics.is_O.sum
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[normed_group E']
{g : α → F}
{l : filter α}
{ι : Type u_13}
{A : ι → α → E'}
{s : finset ι} :
(∀ (i : ι), i ∈ s → asymptotics.is_O (A i) g l) → asymptotics.is_O (λ (x : α), s.sum (λ (i : ι), A i x)) g l
theorem
asymptotics.is_o.sum
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[normed_group E']
[normed_group F']
{g' : α → F'}
{l : filter α}
{ι : Type u_13}
{A : ι → α → E'}
{s : finset ι} :
(∀ (i : ι), i ∈ s → asymptotics.is_o (A i) g' l) → asymptotics.is_o (λ (x : α), s.sum (λ (i : ι), A i x)) g' l
Relation between f = o(g) and f / g → 0
theorem
asymptotics.is_o.tendsto_0
{α : Type u_1}
{𝕜 : Type u_11}
[normed_field 𝕜]
{f g : α → 𝕜}
{l : filter α} :
asymptotics.is_o f g l → filter.tendsto (λ (x : α), f x / g x) l (nhds 0)
theorem
asymptotics.is_o_iff_tendsto
{α : Type u_1}
{𝕜 : Type u_11}
[normed_field 𝕜]
{f g : α → 𝕜}
{l : filter α} :
(∀ (x : α), g x = 0 → f x = 0) → (asymptotics.is_o f g l ↔ filter.tendsto (λ (x : α), f x / g x) l (nhds 0))
Miscellanous lemmas
theorem
asymptotics.is_o_pow_pow
{𝕜 : Type u_11}
[normed_field 𝕜]
{m n : ℕ} :
m < n → asymptotics.is_o (λ (x : 𝕜), x ^ n) (λ (x : 𝕜), x ^ m) (nhds 0)
theorem
asymptotics.is_o_pow_id
{𝕜 : Type u_11}
[normed_field 𝕜]
{n : ℕ} :
1 < n → asymptotics.is_o (λ (x : 𝕜), x ^ n) (λ (x : 𝕜), x) (nhds 0)
theorem
asymptotics.is_O_with.right_le_sub_of_lt_1
{α : Type u_1}
{E' : Type u_6}
[normed_group E']
{c : ℝ}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c f₁ f₂ l → c < 1 → asymptotics.is_O_with (1 / (1 - c)) f₂ (λ (x : α), f₂ x - f₁ x) l
theorem
asymptotics.is_O_with.right_le_add_of_lt_1
{α : Type u_1}
{E' : Type u_6}
[normed_group E']
{c : ℝ}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c f₁ f₂ l → c < 1 → asymptotics.is_O_with (1 / (1 - c)) f₂ (λ (x : α), f₁ x + f₂ x) l
theorem
asymptotics.is_o.right_is_O_sub
{α : Type u_1}
{E' : Type u_6}
[normed_group E']
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o f₁ f₂ l → asymptotics.is_O f₂ (λ (x : α), f₂ x - f₁ x) l
theorem
asymptotics.is_o.right_is_O_add
{α : Type u_1}
{E' : Type u_6}
[normed_group E']
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_o f₁ f₂ l → asymptotics.is_O f₂ (λ (x : α), f₁ x + f₂ x) l
theorem
local_homeomorph.is_O_with_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{E : Type u_3}
[has_norm E]
{F : Type u_4}
[has_norm F]
(e : local_homeomorph α β)
{b : β}
(hb : b ∈ e.to_local_equiv.target)
{f : β → E}
{g : β → F}
{C : ℝ} :
Transfer is_O_with over a local_homeomorph.
theorem
local_homeomorph.is_O_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{E : Type u_3}
[has_norm E]
{F : Type u_4}
[has_norm F]
(e : local_homeomorph α β)
{b : β}
(hb : b ∈ e.to_local_equiv.target)
{f : β → E}
{g : β → F} :
Transfer is_O over a local_homeomorph.
theorem
local_homeomorph.is_o_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{E : Type u_3}
[has_norm E]
{F : Type u_4}
[has_norm F]
(e : local_homeomorph α β)
{b : β}
(hb : b ∈ e.to_local_equiv.target)
{f : β → E}
{g : β → F} :
Transfer is_o over a local_homeomorph.
theorem
homeomorph.is_O_with_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{E : Type u_3}
[has_norm E]
{F : Type u_4}
[has_norm F]
(e : α ≃ₜ β)
{b : β}
{f : β → E}
{g : β → F}
{C : ℝ} :
Transfer is_O_with over a homeomorph.
theorem
homeomorph.is_O_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{E : Type u_3}
[has_norm E]
{F : Type u_4}
[has_norm F]
(e : α ≃ₜ β)
{b : β}
{f : β → E}
{g : β → F} :
Transfer is_O over a homeomorph.
theorem
homeomorph.is_o_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{E : Type u_3}
[has_norm E]
{F : Type u_4}
[has_norm F]
(e : α ≃ₜ β)
{b : β}
{f : β → E}
{g : β → F} :
Transfer is_o over a homeomorph.