Asymptotics #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We introduce these relations:
is_O_with c l f g: "f is big O of g along l with constant c";f =O[l] g: "f is big O of g along l";f =o[l] g: "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
f =O[l] g ↔ (λ x, ‖f x‖) =O[l] (λ x, ‖g x‖),
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
f =o[l] g ↔ 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 #
@[irreducible]
def
asymptotics.is_O_with
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
(c : ℝ)
(l : filter α)
(f : α → E)
(g : α → F) :
Prop
This version of the Landau notation is_O_with C l f g 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.
@[irreducible]
def
asymptotics.is_O
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
(l : filter α)
(f : α → E)
(g : α → F) :
Prop
The Landau notation f =O[l] g 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.
@[irreducible]
def
asymptotics.is_o
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
(l : filter α)
(f : α → E)
(g : α → F) :
Prop
The Landau notation f =o[l] g 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.
Conversions #
theorem
asymptotics.is_O_with.weaken
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c c' : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α}
(h : asymptotics.is_O_with c l f g')
(hc : c ≤ c') :
asymptotics.is_O_with c' l f g'
theorem
asymptotics.is_O_with.exists_pos
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α}
(h : asymptotics.is_O_with c l f g') :
∃ (c' : ℝ) (H : 0 < c'), asymptotics.is_O_with c' l f g'
theorem
asymptotics.is_O_with.exists_nonneg
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α}
(h : asymptotics.is_O_with c l f g') :
∃ (c' : ℝ) (H : 0 ≤ c'), asymptotics.is_O_with c' l f g'
theorem
asymptotics.is_O_iff_eventually_is_O_with
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
f =O[l] g' ↔ ∀ᶠ (c : ℝ) in filter.at_top, asymptotics.is_O_with c l f g'
f = O(g) if and only if is_O_with c f g for all sufficiently large c.
theorem
asymptotics.is_O_iff_eventually
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{f : α → E}
{g' : α → F'}
{l : filter α} :
f = O(g) if and only if ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ for all sufficiently large c.
Subsingleton #
theorem
asymptotics.is_o_of_subsingleton
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[subsingleton E'] :
theorem
asymptotics.is_O_of_subsingleton
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[subsingleton E'] :
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₂ : ℝ}
{l : filter α}
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
(h : asymptotics.is_O_with c₁ l f₁ g₁)
(hc : c₁ = c₂)
(hf : ∀ (x : α), f₁ x = f₂ x)
(hg : ∀ (x : α), g₁ x = g₂ x) :
asymptotics.is_O_with c₂ l f₂ g₂
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}
{l : filter α}
{f₁ f₂ : α → E}
(h : asymptotics.is_O_with c l f₁ g)
(hf : ∀ (x : α), f₁ x = f₂ x) :
asymptotics.is_O_with c l f₂ g
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}
{l : filter α}
{g₁ g₂ : α → F}
(h : asymptotics.is_O_with c l f g₁)
(hg : ∀ (x : α), g₁ x = g₂ x) :
asymptotics.is_O_with c l f g₂
theorem
asymptotics.is_O_with.congr_const
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
{c₁ c₂ : ℝ}
{f : α → E}
{g : α → F}
{l : filter α}
(h : asymptotics.is_O_with c₁ l f g)
(hc : c₁ = c₂) :
asymptotics.is_O_with c₂ l f g
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 l f g)
{k : β → α}
{l' : filter β}
(hk : filter.tendsto k l' l) :
asymptotics.is_O_with c l' (f ∘ k) (g ∘ k)
@[simp]
theorem
asymptotics.is_O_with_map
{α : 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}
{k : β → α}
{l : filter β} :
asymptotics.is_O_with c (filter.map k l) f g ↔ asymptotics.is_O_with c l (f ∘ k) (g ∘ k)
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 α}
(h : asymptotics.is_O_with c l' f g)
(hl : l ≤ l') :
asymptotics.is_O_with c l f g
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 α}
(hfg : asymptotics.is_O_with c l f g)
(hgk : asymptotics.is_O_with c' l g k)
(hc : 0 ≤ c) :
asymptotics.is_O_with (c * c') l f k
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 l f f
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 α}
(hfg : asymptotics.is_O_with c l f g)
(hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖)
(hc : 0 ≤ c) :
asymptotics.is_O_with c l f k
theorem
asymptotics.is_O_with.sup
{α : 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 α}
(h : asymptotics.is_O_with c l f g)
(h' : asymptotics.is_O_with c l' f g) :
asymptotics.is_O_with c (l ⊔ l') f g
theorem
asymptotics.is_O_with.sup'
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c c' : ℝ}
{f : α → E}
{g' : α → F'}
{l l' : filter α}
(h : asymptotics.is_O_with c l f g')
(h' : asymptotics.is_O_with c' l' f g') :
asymptotics.is_O_with (linear_order.max c c') (l ⊔ l') f g'
theorem
asymptotics.is_O_with_insert
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
[topological_space α]
{x : α}
{s : set α}
{C : ℝ}
{g : α → E}
{g' : α → F}
(h : ‖g x‖ ≤ C * ‖g' x‖) :
asymptotics.is_O_with C (nhds_within x (has_insert.insert x s)) g g' ↔ asymptotics.is_O_with C (nhds_within x s) g g'
theorem
asymptotics.is_O_with.insert
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[has_norm E]
[has_norm F]
[topological_space α]
{x : α}
{s : set α}
{C : ℝ}
{g : α → E}
{g' : α → F}
(h1 : asymptotics.is_O_with C (nhds_within x s) g g')
(h2 : ‖g x‖ ≤ C * ‖g' x‖) :
asymptotics.is_O_with C (nhds_within x (has_insert.insert x s)) g g'
theorem
asymptotics.is_o_insert
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[topological_space α]
{x : α}
{s : set α}
{g : α → E'}
{g' : α → F'}
(h : g x = 0) :
g =o[nhds_within x (has_insert.insert x s)] g' ↔ g =o[nhds_within x s] g'
theorem
asymptotics.is_o.insert
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[topological_space α]
{x : α}
{s : set α}
{g : α → E'}
{g' : α → F'}
(h1 : g =o[nhds_within x s] g')
(h2 : g x = 0) :
g =o[nhds_within x (has_insert.insert x s)] g'
Simplification : norm, abs #
@[simp]
theorem
asymptotics.is_O_with_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f (λ (x : α), ‖g' x‖) ↔ asymptotics.is_O_with c l f g'
@[simp]
theorem
asymptotics.is_O_with_abs_right
{α : Type u_1}
{E : Type u_3}
[has_norm E]
{c : ℝ}
{f : α → E}
{l : filter α}
{u : α → ℝ} :
asymptotics.is_O_with c l f (λ (x : α), |u x|) ↔ asymptotics.is_O_with c l f u
theorem
asymptotics.is_O_with.norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f g' → asymptotics.is_O_with c l f (λ (x : α), ‖g' x‖)
Alias of the reverse direction of asymptotics.is_O_with_norm_right.
theorem
asymptotics.is_O_with.of_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f (λ (x : α), ‖g' x‖) → asymptotics.is_O_with c l f g'
Alias of the forward direction of asymptotics.is_O_with_norm_right.
theorem
asymptotics.is_O_with.of_abs_right
{α : Type u_1}
{E : Type u_3}
[has_norm E]
{c : ℝ}
{f : α → E}
{l : filter α}
{u : α → ℝ} :
asymptotics.is_O_with c l f (λ (x : α), |u x|) → asymptotics.is_O_with c l f u
Alias of the forward direction of asymptotics.is_O_with_abs_right.
theorem
asymptotics.is_O_with.abs_right
{α : Type u_1}
{E : Type u_3}
[has_norm E]
{c : ℝ}
{f : α → E}
{l : filter α}
{u : α → ℝ} :
asymptotics.is_O_with c l f u → asymptotics.is_O_with c l f (λ (x : α), |u x|)
Alias of the reverse direction of asymptotics.is_O_with_abs_right.
@[simp]
theorem
asymptotics.is_O_with_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) g ↔ asymptotics.is_O_with c l f' g
@[simp]
theorem
asymptotics.is_O_with_abs_left
{α : Type u_1}
{F : Type u_4}
[has_norm F]
{c : ℝ}
{g : α → F}
{l : filter α}
{u : α → ℝ} :
asymptotics.is_O_with c l (λ (x : α), |u x|) g ↔ asymptotics.is_O_with c l u g
theorem
asymptotics.is_O_with.of_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) g → asymptotics.is_O_with c l f' g
Alias of the forward direction of asymptotics.is_O_with_norm_left.
theorem
asymptotics.is_O_with.norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c l f' g → asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) g
Alias of the reverse direction of asymptotics.is_O_with_norm_left.
theorem
asymptotics.is_O_with.of_abs_left
{α : Type u_1}
{F : Type u_4}
[has_norm F]
{c : ℝ}
{g : α → F}
{l : filter α}
{u : α → ℝ} :
asymptotics.is_O_with c l (λ (x : α), |u x|) g → asymptotics.is_O_with c l u g
Alias of the forward direction of asymptotics.is_O_with_abs_left.
theorem
asymptotics.is_O_with.abs_left
{α : Type u_1}
{F : Type u_4}
[has_norm F]
{c : ℝ}
{g : α → F}
{l : filter α}
{u : α → ℝ} :
asymptotics.is_O_with c l u g → asymptotics.is_O_with c l (λ (x : α), |u x|) g
Alias of the reverse direction of asymptotics.is_O_with_abs_left.
theorem
asymptotics.is_O_with_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) (λ (x : α), ‖g' x‖) ↔ asymptotics.is_O_with c l f' g'
theorem
asymptotics.is_O_with_abs_abs
{α : Type u_1}
{c : ℝ}
{l : filter α}
{u v : α → ℝ} :
asymptotics.is_O_with c l (λ (x : α), |u x|) (λ (x : α), |v x|) ↔ asymptotics.is_O_with c l u v
theorem
asymptotics.is_O_with.of_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) (λ (x : α), ‖g' x‖) → asymptotics.is_O_with c l f' g'
Alias of the forward direction of asymptotics.is_O_with_norm_norm.
theorem
asymptotics.is_O_with.norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f' g' → asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) (λ (x : α), ‖g' x‖)
Alias of the reverse direction of asymptotics.is_O_with_norm_norm.
theorem
asymptotics.is_O_with.of_abs_abs
{α : Type u_1}
{c : ℝ}
{l : filter α}
{u v : α → ℝ} :
asymptotics.is_O_with c l (λ (x : α), |u x|) (λ (x : α), |v x|) → asymptotics.is_O_with c l u v
Alias of the forward direction of asymptotics.is_O_with_abs_abs.
theorem
asymptotics.is_O_with.abs_abs
{α : Type u_1}
{c : ℝ}
{l : filter α}
{u v : α → ℝ} :
asymptotics.is_O_with c l u v → asymptotics.is_O_with c l (λ (x : α), |u x|) (λ (x : α), |v x|)
Alias of the reverse direction of asymptotics.is_O_with_abs_abs.
theorem
asymptotics.is_O.norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
Alias of the reverse direction of asymptotics.is_O_norm_norm.
theorem
asymptotics.is_O.of_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
Alias of the forward direction of asymptotics.is_O_norm_norm.
theorem
asymptotics.is_o.of_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
Alias of the forward direction of asymptotics.is_o_norm_norm.
theorem
asymptotics.is_o.norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
Alias of the reverse direction of asymptotics.is_o_norm_norm.
Simplification: negate #
@[simp]
theorem
asymptotics.is_O_with_neg_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f (λ (x : α), -g' x) ↔ asymptotics.is_O_with c l f g'
theorem
asymptotics.is_O_with.neg_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f g' → asymptotics.is_O_with c l f (λ (x : α), -g' x)
Alias of the reverse direction of asymptotics.is_O_with_neg_right.
theorem
asymptotics.is_O_with.of_neg_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[has_norm E]
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with c l f (λ (x : α), -g' x) → asymptotics.is_O_with c l f g'
Alias of the forward direction of asymptotics.is_O_with_neg_right.
@[simp]
theorem
asymptotics.is_O_with_neg_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), -f' x) g ↔ asymptotics.is_O_with c l f' g
theorem
asymptotics.is_O_with.of_neg_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), -f' x) g → asymptotics.is_O_with c l f' g
Alias of the forward direction of asymptotics.is_O_with_neg_left.
theorem
asymptotics.is_O_with.neg_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α} :
asymptotics.is_O_with c l f' g → asymptotics.is_O_with c l (λ (x : α), -f' x) g
Alias of the reverse direction of asymptotics.is_O_with_neg_left.
Product of functions (right) #
theorem
asymptotics.is_O_with_fst_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with 1 l f' (λ (x : α), (f' x, g' x))
theorem
asymptotics.is_O_with_snd_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
asymptotics.is_O_with 1 l g' (λ (x : α), (f' x, g' x))
theorem
asymptotics.is_O_fst_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
theorem
asymptotics.is_O_snd_prod
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
{g' : α → F'}
{l : filter α} :
theorem
asymptotics.is_O_fst_prod'
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{l : filter α}
{f' : α → E' × F'} :
theorem
asymptotics.is_O_snd_prod'
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{l : filter α}
{f' : α → E' × F'} :
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]
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{c : ℝ}
{f : α → E}
{g' : α → F'}
(k' : α → G')
{l : filter α}
(h : asymptotics.is_O_with c l f g')
(hc : 0 ≤ c) :
asymptotics.is_O_with c l f (λ (x : α), (g' x, k' x))
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]
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{c : ℝ}
{f : α → E}
(f' : α → E')
{g' : α → F'}
{l : filter α}
(h : asymptotics.is_O_with c l f g')
(hc : 0 ≤ c) :
asymptotics.is_O_with c l f (λ (x : α), (f' x, g' x))
theorem
asymptotics.is_O_with.prod_left_same
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(hf : asymptotics.is_O_with c l f' k')
(hg : asymptotics.is_O_with c l g' k') :
asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k'
theorem
asymptotics.is_O_with.prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{c c' : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(hf : asymptotics.is_O_with c l f' k')
(hg : asymptotics.is_O_with c' l g' k') :
asymptotics.is_O_with (linear_order.max c c') l (λ (x : α), (f' x, g' x)) k'
theorem
asymptotics.is_O_with.prod_left_fst
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(h : asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k') :
asymptotics.is_O_with c l f' k'
theorem
asymptotics.is_O_with.prod_left_snd
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(h : asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k') :
asymptotics.is_O_with c l g' k'
theorem
asymptotics.is_O_with_prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k' ↔ asymptotics.is_O_with c l f' k' ∧ asymptotics.is_O_with c l g' k'
theorem
asymptotics.is_O.prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(hf : f' =O[l] k')
(hg : g' =O[l] k') :
theorem
asymptotics.is_O.prod_left_fst
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
theorem
asymptotics.is_O.prod_left_snd
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
@[simp]
theorem
asymptotics.is_O_prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
theorem
asymptotics.is_o.prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α}
(hf : f' =o[l] k')
(hg : g' =o[l] k') :
theorem
asymptotics.is_o.prod_left_fst
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
theorem
asymptotics.is_o.prod_left_snd
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
@[simp]
theorem
asymptotics.is_o_prod_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{G' : Type u_8}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[seminormed_add_comm_group G']
{f' : α → E'}
{g' : α → F'}
{k' : α → G'}
{l : filter α} :
theorem
asymptotics.is_O_with.eq_zero_imp
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{c : ℝ}
{f'' : α → E''}
{g'' : α → F''}
{l : filter α}
(h : asymptotics.is_O_with c l f'' g'') :
Addition and subtraction #
theorem
asymptotics.is_O_with.add
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'}
(h₁ : asymptotics.is_O_with c₁ l f₁ g)
(h₂ : asymptotics.is_O_with c₂ l f₂ g) :
asymptotics.is_O_with (c₁ + c₂) l (λ (x : α), f₁ x + f₂ x) g
theorem
asymptotics.is_O_with.add_is_o
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'}
(h₁ : asymptotics.is_O_with c₁ l f₁ g)
(h₂ : f₂ =o[l] g)
(hc : c₁ < c₂) :
asymptotics.is_O_with c₂ l (λ (x : α), f₁ x + f₂ x) g
theorem
asymptotics.is_o.add_is_O_with
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'}
(h₁ : f₁ =o[l] g)
(h₂ : asymptotics.is_O_with c₁ l f₂ g)
(hc : c₁ < c₂) :
asymptotics.is_O_with c₂ l (λ (x : α), f₁ x + f₂ x) g
theorem
asymptotics.is_O_with.sub
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'}
(h₁ : asymptotics.is_O_with c₁ l f₁ g)
(h₂ : asymptotics.is_O_with c₂ l f₂ g) :
asymptotics.is_O_with (c₁ + c₂) l (λ (x : α), f₁ x - f₂ x) g
theorem
asymptotics.is_O_with.sub_is_o
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c₁ c₂ : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'}
(h₁ : asymptotics.is_O_with c₁ l f₁ g)
(h₂ : f₂ =o[l] g)
(hc : c₁ < c₂) :
asymptotics.is_O_with c₂ l (λ (x : α), f₁ x - f₂ x) g
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]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'}
(h : asymptotics.is_O_with c l (λ (x : α), f₁ x - f₂ x) g) :
asymptotics.is_O_with c l (λ (x : α), f₂ x - f₁ x) g
theorem
asymptotics.is_O_with_comm
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ : α → E'} :
asymptotics.is_O_with c l (λ (x : α), f₁ x - f₂ x) g ↔ asymptotics.is_O_with c l (λ (x : α), f₂ x - f₁ x) g
theorem
asymptotics.is_O_with.triangle
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{c c' : ℝ}
{g : α → F}
{l : filter α}
{f₁ f₂ f₃ : α → E'}
(h₁ : asymptotics.is_O_with c l (λ (x : α), f₁ x - f₂ x) g)
(h₂ : asymptotics.is_O_with c' l (λ (x : α), f₂ x - f₃ x) g) :
asymptotics.is_O_with (c + c') l (λ (x : α), f₁ x - f₃ x) g
Zero, one, and other constants #
theorem
asymptotics.is_o_zero
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
(g' : α → F')
(l : filter α) :
theorem
asymptotics.is_O_with_zero
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{c : ℝ}
(g' : α → F')
(l : filter α)
(hc : 0 ≤ c) :
asymptotics.is_O_with c l (λ (x : α), 0) g'
theorem
asymptotics.is_O_with_zero'
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
(g : α → F)
(l : filter α) :
asymptotics.is_O_with 0 l (λ (x : α), 0) g
theorem
asymptotics.is_O_refl_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
(g' : α → F')
(l : filter α) :
theorem
asymptotics.is_o_refl_left
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
{f' : α → E'}
(g' : α → F')
(l : filter α) :
@[simp]
theorem
asymptotics.is_O_with_zero_right_iff
{α : Type u_1}
{F' : Type u_7}
{E'' : Type u_9}
[seminormed_add_comm_group F']
[normed_add_comm_group E'']
{c : ℝ}
{f'' : α → E''}
{l : filter α} :
asymptotics.is_O_with c l f'' (λ (x : α), 0) ↔ f'' =ᶠ[l] 0
@[simp]
theorem
asymptotics.is_O_zero_right_iff
{α : Type u_1}
{F' : Type u_7}
{E'' : Type u_9}
[seminormed_add_comm_group F']
[normed_add_comm_group E'']
{f'' : α → E''}
{l : filter α} :
@[simp]
theorem
asymptotics.is_o_zero_right_iff
{α : Type u_1}
{F' : Type u_7}
{E'' : Type u_9}
[seminormed_add_comm_group F']
[normed_add_comm_group E'']
{f'' : α → E''}
{l : filter α} :
theorem
asymptotics.is_O_with_const_const
{α : Type u_1}
{E : Type u_3}
{F'' : Type u_10}
[has_norm E]
[normed_add_comm_group F'']
(c : E)
{c' : F''}
(hc' : c' ≠ 0)
(l : filter α) :
@[simp]
theorem
asymptotics.is_O_const_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{c : E''}
{c' : F''}
(l : filter α)
[l.ne_bot] :
@[simp]
theorem
asymptotics.is_O_pure
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{g'' : α → F''}
{x : α} :
@[simp]
theorem
asymptotics.is_o_top
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{g'' : α → F''} :
theorem
asymptotics.is_O_with_const_one
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[has_norm E]
[has_norm F]
[has_one F]
[norm_one_class F]
(c : E)
(l : filter α) :
asymptotics.is_O_with ‖c‖ l (λ (x : α), c) (λ (x : α), 1)
@[simp]
theorem
asymptotics.is_o_one_iff
{α : Type u_1}
(F : Type u_4)
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{f' : α → E'}
{l : filter α}
[has_one F]
[norm_one_class F] :
(f' =o[l] λ (x : α), 1) ↔ filter.tendsto f' l (nhds 0)
theorem
filter.is_bounded_under.is_O_one
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[has_norm E]
[has_norm F]
{f : α → E}
{l : filter α}
[has_one F]
[norm_one_class F] :
Alias of the reverse direction of asymptotics.is_O_one_iff.
@[simp]
theorem
asymptotics.is_o_one_left_iff
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
[has_norm E]
[has_norm F]
{f : α → E}
{l : filter α}
[has_one F]
[norm_one_class F] :
(λ (x : α), 1) =o[l] f ↔ filter.tendsto (λ (x : α), ‖f x‖) l filter.at_top
theorem
filter.tendsto.is_O_one
{α : Type u_1}
(F : Type u_4)
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{f' : α → E'}
{l : filter α}
[has_one F]
[norm_one_class F]
{c : E'}
(h : filter.tendsto f' l (nhds c)) :
theorem
asymptotics.is_O.trans_tendsto_nhds
{α : Type u_1}
{E : Type u_3}
(F : Type u_4)
{F' : Type u_7}
[has_norm E]
[has_norm F]
[seminormed_add_comm_group F']
{f : α → E}
{g' : α → F'}
{l : filter α}
[has_one F]
[norm_one_class F]
(hfg : f =O[l] g')
{y : F'}
(hg : filter.tendsto g' l (nhds y)) :
theorem
asymptotics.is_o_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{l : filter α}
{c : F''}
(hc : c ≠ 0) :
(f'' =o[l] λ (x : α), c) ↔ filter.tendsto f'' l (nhds 0)
theorem
asymptotics.is_o_id_const
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{c : F''}
(hc : c ≠ 0) :
theorem
filter.is_bounded_under.is_O_const
{α : Type u_1}
{E : Type u_3}
{F'' : Type u_10}
[has_norm E]
[normed_add_comm_group F'']
{f : α → E}
{l : filter α}
(h : filter.is_bounded_under has_le.le l (has_norm.norm ∘ f))
{c : F''}
(hc : c ≠ 0) :
theorem
asymptotics.is_O_const_of_tendsto
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{l : filter α}
{y : E''}
(h : filter.tendsto f'' l (nhds y))
{c : F''}
(hc : c ≠ 0) :
theorem
asymptotics.is_O_const_of_ne
{α : Type u_1}
{E : Type u_3}
{F'' : Type u_10}
[has_norm E]
[normed_add_comm_group F'']
{f : α → E}
{l : filter α}
{c : F''}
(hc : c ≠ 0) :
(f =O[l] λ (x : α), c) ↔ filter.is_bounded_under has_le.le l (has_norm.norm ∘ f)
theorem
asymptotics.is_O_const_left_iff_pos_le_norm
{α : Type u_1}
{E' : Type u_6}
{E'' : Type u_9}
[seminormed_add_comm_group E']
[normed_add_comm_group E'']
{f' : α → E'}
{l : filter α}
{c : E''}
(hc : c ≠ 0) :
(λ x, c) =O[l] f if and only if f is bounded away from zero.
theorem
asymptotics.is_O.trans_tendsto
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group 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.is_o.trans_tendsto
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group 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)
Multiplication by a constant #
theorem
asymptotics.is_O_with_const_mul_self
{α : Type u_1}
{R : Type u_12}
[semi_normed_ring R]
(c : R)
(f : α → R)
(l : filter α) :
asymptotics.is_O_with ‖c‖ l (λ (x : α), c * f x) f
theorem
asymptotics.is_O_const_mul_self
{α : Type u_1}
{R : Type u_12}
[semi_normed_ring R]
(c : R)
(f : α → R)
(l : filter α) :
theorem
asymptotics.is_O_with.const_mul_left
{α : Type u_1}
{F : Type u_4}
{R : Type u_12}
[has_norm F]
[semi_normed_ring R]
{c : ℝ}
{g : α → F}
{l : filter α}
{f : α → R}
(h : asymptotics.is_O_with c l f g)
(c' : R) :
asymptotics.is_O_with (‖c'‖ * c) l (λ (x : α), c' * f x) g
theorem
asymptotics.is_O_with_self_const_mul'
{α : Type u_1}
{R : Type u_12}
[semi_normed_ring R]
(u : Rˣ)
(f : α → R)
(l : filter α) :
theorem
asymptotics.is_O_with_self_const_mul
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
(c : 𝕜)
(hc : c ≠ 0)
(f : α → 𝕜)
(l : filter α) :
asymptotics.is_O_with ‖c‖⁻¹ l f (λ (x : α), c * f x)
theorem
asymptotics.is_O_with.of_const_mul_right
{α : Type u_1}
{E : Type u_3}
{R : Type u_12}
[has_norm E]
[semi_normed_ring R]
{c' : ℝ}
{f : α → E}
{l : filter α}
{g : α → R}
{c : R}
(hc' : 0 ≤ c')
(h : asymptotics.is_O_with c' l f (λ (x : α), c * g x)) :
asymptotics.is_O_with (c' * ‖c‖) l f g
theorem
asymptotics.is_O_with.const_mul_right
{α : Type u_1}
{E : Type u_3}
{𝕜 : Type u_14}
[has_norm E]
[normed_field 𝕜]
{f : α → E}
{l : filter α}
{g : α → 𝕜}
{c : 𝕜}
(hc : c ≠ 0)
{c' : ℝ}
(hc' : 0 ≤ c')
(h : asymptotics.is_O_with c' l f g) :
Multiplication #
theorem
asymptotics.is_O_with.mul
{α : Type u_1}
{R : Type u_12}
{𝕜 : Type u_14}
[semi_normed_ring R]
[normed_field 𝕜]
{l : filter α}
{f₁ f₂ : α → R}
{g₁ g₂ : α → 𝕜}
{c₁ c₂ : ℝ}
(h₁ : asymptotics.is_O_with c₁ l f₁ g₁)
(h₂ : asymptotics.is_O_with c₂ l f₂ g₂) :
asymptotics.is_O_with (c₁ * c₂) l (λ (x : α), f₁ x * f₂ x) (λ (x : α), g₁ x * g₂ x)
theorem
asymptotics.is_O_with.pow'
{α : Type u_1}
{R : Type u_12}
{𝕜 : Type u_14}
[semi_normed_ring R]
[normed_field 𝕜]
{c : ℝ}
{l : filter α}
{f : α → R}
{g : α → 𝕜}
(h : asymptotics.is_O_with c l f g)
(n : ℕ) :
theorem
asymptotics.is_O_with.pow
{α : Type u_1}
{R : Type u_12}
{𝕜 : Type u_14}
[semi_normed_ring R]
[normed_field 𝕜]
{c : ℝ}
{l : filter α}
[norm_one_class R]
{f : α → R}
{g : α → 𝕜}
(h : asymptotics.is_O_with c l f g)
(n : ℕ) :
asymptotics.is_O_with (c ^ n) l (λ (x : α), f x ^ n) (λ (x : α), g x ^ n)
theorem
asymptotics.is_O_with.of_pow
{α : Type u_1}
{R : Type u_12}
{𝕜 : Type u_14}
[semi_normed_ring R]
[normed_field 𝕜]
{c c' : ℝ}
{l : filter α}
{n : ℕ}
{f : α → 𝕜}
{g : α → R}
(h : asymptotics.is_O_with c l (f ^ n) (g ^ n))
(hn : n ≠ 0)
(hc : c ≤ c' ^ n)
(hc' : 0 ≤ c') :
asymptotics.is_O_with c' l f g
Inverse #
theorem
asymptotics.is_O_with.inv_rev
{α : Type u_1}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[normed_field 𝕜]
[normed_field 𝕜']
{c : ℝ}
{l : filter α}
{f : α → 𝕜}
{g : α → 𝕜'}
(h : asymptotics.is_O_with c l f g)
(h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) :
asymptotics.is_O_with c l (λ (x : α), (g x)⁻¹) (λ (x : α), (f x)⁻¹)
Scalar multiplication #
theorem
asymptotics.is_O_with.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm F]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
(h : asymptotics.is_O_with c l f' g)
(c' : 𝕜) :
asymptotics.is_O_with (‖c'‖ * c) l (λ (x : α), c' • f' x) g
theorem
asymptotics.is_O.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm F]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
(h : f' =O[l] g)
(c : 𝕜) :
theorem
asymptotics.is_o.const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm F]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
(h : f' =o[l] g)
(c : 𝕜) :
theorem
asymptotics.is_O_const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm F]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
theorem
asymptotics.is_o_const_smul_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm F]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{g : α → F}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
theorem
asymptotics.is_O_const_smul_right
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm E]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{f : α → E}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
theorem
asymptotics.is_o_const_smul_right
{α : Type u_1}
{E : Type u_3}
{E' : Type u_6}
{𝕜 : Type u_14}
[has_norm E]
[seminormed_add_comm_group E']
[normed_field 𝕜]
{f : α → E}
{f' : α → E'}
{l : filter α}
[normed_space 𝕜 E']
{c : 𝕜}
(hc : c ≠ 0) :
theorem
asymptotics.is_O_with.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[normed_field 𝕜]
[normed_field 𝕜']
{c c' : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜' F']
{k₁ : α → 𝕜}
{k₂ : α → 𝕜'}
(h₁ : asymptotics.is_O_with c l k₁ k₂)
(h₂ : asymptotics.is_O_with c' l f' g') :
asymptotics.is_O_with (c * c') l (λ (x : α), k₁ x • f' x) (λ (x : α), k₂ x • g' x)
theorem
asymptotics.is_O.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[normed_field 𝕜]
[normed_field 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜' F']
{k₁ : α → 𝕜}
{k₂ : α → 𝕜'}
(h₁ : k₁ =O[l] k₂)
(h₂ : f' =O[l] g') :
theorem
asymptotics.is_O.smul_is_o
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[normed_field 𝕜]
[normed_field 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜' F']
{k₁ : α → 𝕜}
{k₂ : α → 𝕜'}
(h₁ : k₁ =O[l] k₂)
(h₂ : f' =o[l] g') :
theorem
asymptotics.is_o.smul_is_O
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[normed_field 𝕜]
[normed_field 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜' F']
{k₁ : α → 𝕜}
{k₂ : α → 𝕜'}
(h₁ : k₁ =o[l] k₂)
(h₂ : f' =O[l] g') :
theorem
asymptotics.is_o.smul
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
{𝕜 : Type u_14}
{𝕜' : Type u_15}
[seminormed_add_comm_group E']
[seminormed_add_comm_group F']
[normed_field 𝕜]
[normed_field 𝕜']
{f' : α → E'}
{g' : α → F'}
{l : filter α}
[normed_space 𝕜 E']
[normed_space 𝕜' F']
{k₁ : α → 𝕜}
{k₂ : α → 𝕜'}
(h₁ : k₁ =o[l] k₂)
(h₂ : f' =o[l] g') :
Sum #
theorem
asymptotics.is_O_with.sum
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[has_norm F]
[seminormed_add_comm_group E']
{g : α → F}
{l : filter α}
{ι : Type u_16}
{A : ι → α → E'}
{C : ι → ℝ}
{s : finset ι}
(h : ∀ (i : ι), i ∈ s → asymptotics.is_O_with (C i) l (A i) g) :
asymptotics.is_O_with (s.sum (λ (i : ι), C i)) l (λ (x : α), s.sum (λ (i : ι), A i x)) g
Relation between f = o(g) and f / g → 0 #
theorem
asymptotics.is_o.tendsto_div_nhds_zero
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{l : filter α}
{f g : α → 𝕜}
(h : f =o[l] g) :
filter.tendsto (λ (x : α), f x / g x) l (nhds 0)
theorem
asymptotics.is_o.tendsto_inv_smul_nhds_zero
{α : Type u_1}
{E' : Type u_6}
{𝕜 : Type u_14}
[seminormed_add_comm_group E']
[normed_field 𝕜]
[normed_space 𝕜 E']
{f : α → E'}
{g : α → 𝕜}
{l : filter α}
(h : f =o[l] g) :
filter.tendsto (λ (x : α), (g x)⁻¹ • f x) l (nhds 0)
theorem
asymptotics.is_o_of_tendsto
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{l : filter α}
{f g : α → 𝕜}
(hgf : ∀ (x : α), g x = 0 → f x = 0) :
Alias of the reverse direction of asymptotics.is_o_iff_tendsto.
theorem
asymptotics.is_o_const_left_of_ne
{α : Type u_1}
{F : Type u_4}
{E'' : Type u_9}
[has_norm F]
[normed_add_comm_group E'']
{g : α → F}
{l : filter α}
{c : E''}
(hc : c ≠ 0) :
(λ (x : α), c) =o[l] g ↔ filter.tendsto (λ (x : α), ‖g x‖) l filter.at_top
@[simp]
theorem
asymptotics.is_o_const_left
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{g'' : α → F''}
{l : filter α}
{c : E''} :
(λ (x : α), c) =o[l] g'' ↔ c = 0 ∨ filter.tendsto (has_norm.norm ∘ g'') l filter.at_top
@[simp]
theorem
asymptotics.is_o_const_const_iff
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{l : filter α}
[l.ne_bot]
{d : E''}
{c : F''} :
@[simp]
theorem
asymptotics.is_o_pure
{α : Type u_1}
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f'' : α → E''}
{g'' : α → F''}
{x : α} :
f'' =o[has_pure.pure x] g'' ↔ f'' x = 0
theorem
asymptotics.is_o_const_id_comap_norm_at_top
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
(c : F'') :
(λ (x : E''), c) =o[filter.comap has_norm.norm filter.at_top] id
theorem
asymptotics.is_o_const_id_at_top
{E'' : Type u_9}
[normed_add_comm_group E'']
(c : E'') :
(λ (x : ℝ), c) =o[filter.at_top] id
theorem
asymptotics.is_o_const_id_at_bot
{E'' : Type u_9}
[normed_add_comm_group E'']
(c : E'') :
(λ (x : ℝ), c) =o[filter.at_bot] id
Eventually (u / v) * v = u #
If u and v are linked by an is_O_with relation, then we
eventually have (u / v) * v = u, even if v vanishes.
theorem
asymptotics.is_O_with.eventually_mul_div_cancel
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{c : ℝ}
{l : filter α}
{u v : α → 𝕜}
(h : asymptotics.is_O_with c l u v) :
Equivalent definitions of the form ∃ φ, u =ᶠ[l] φ * v in a normed_field. #
theorem
asymptotics.is_O_with_of_eq_mul
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{c : ℝ}
{l : filter α}
{u v : α → 𝕜}
(φ : α → 𝕜)
(hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c)
(h : u =ᶠ[l] φ * v) :
asymptotics.is_O_with c l u v
If ‖φ‖ is eventually bounded by c, and u =ᶠ[l] φ * v, then we have is_O_with c u v l.
This does not require any assumptions on c, which is why we keep this version along with
is_O_with_iff_exists_eq_mul.
theorem
asymptotics.is_O_iff_exists_eq_mul
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{l : filter α}
{u v : α → 𝕜} :
theorem
asymptotics.is_O.exists_eq_mul
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{l : filter α}
{u v : α → 𝕜} :
Alias of the forward direction of asymptotics.is_O_iff_exists_eq_mul.
theorem
asymptotics.is_o.exists_eq_mul
{α : Type u_1}
{𝕜 : Type u_14}
[normed_field 𝕜]
{l : filter α}
{u v : α → 𝕜} :
Alias of the forward direction of asymptotics.is_o_iff_exists_eq_mul.
Miscellanous lemmas #
theorem
asymptotics.div_is_bounded_under_of_is_O
{𝕜 : Type u_14}
[normed_field 𝕜]
{α : Type u_1}
{l : filter α}
{f g : α → 𝕜}
(h : f =O[l] g) :
filter.is_bounded_under has_le.le l (λ (x : α), ‖f x / g x‖)
theorem
asymptotics.is_o.tendsto_zero_of_tendsto
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_3}
[normed_add_comm_group E]
[normed_field 𝕜]
{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.is_O.eq_zero_of_norm_pow_within
{E'' : Type u_9}
{F'' : Type u_10}
[normed_add_comm_group E'']
[normed_add_comm_group F'']
{f : E'' → F''}
{s : set E''}
{x₀ : E''}
{n : ℕ}
(h : f =O[nhds_within x₀ s] λ (x : E''), ‖x - x₀‖ ^ n)
(hx₀ : x₀ ∈ s)
(hn : 0 < n) :
f x₀ = 0
theorem
asymptotics.is_O_with.right_le_sub_of_lt_1
{α : Type u_1}
{E' : Type u_6}
[seminormed_add_comm_group E']
{c : ℝ}
{l : filter α}
{f₁ f₂ : α → E'}
(h : asymptotics.is_O_with c l f₁ f₂)
(hc : c < 1) :
asymptotics.is_O_with (1 / (1 - c)) l f₂ (λ (x : α), f₂ x - f₁ x)
theorem
asymptotics.is_O_with.right_le_add_of_lt_1
{α : Type u_1}
{E' : Type u_6}
[seminormed_add_comm_group E']
{c : ℝ}
{l : filter α}
{f₁ f₂ : α → E'}
(h : asymptotics.is_O_with c l f₁ f₂)
(hc : c < 1) :
asymptotics.is_O_with (1 / (1 - c)) l f₂ (λ (x : α), f₁ x + f₂ x)
theorem
asymptotics.bound_of_is_O_cofinite
{α : Type u_1}
{E : Type u_3}
{F'' : Type u_10}
[has_norm E]
[normed_add_comm_group F'']
{f : α → E}
{g'' : α → F''}
(h : f =O[filter.cofinite] g'') :
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.is_O_with_pi
{α : Type u_1}
{F' : Type u_7}
[seminormed_add_comm_group F']
{g' : α → F'}
{l : filter α}
{ι : Type u_2}
[fintype ι]
{E' : ι → Type u_3}
[Π (i : ι), normed_add_comm_group (E' i)]
{f : α → Π (i : ι), E' i}
{C : ℝ}
(hC : 0 ≤ C) :
asymptotics.is_O_with C l f g' ↔ ∀ (i : ι), asymptotics.is_O_with C l (λ (x : α), f x i) g'
@[simp]
@[simp]
theorem
summable_of_is_O
{ι : Type u_1}
{E : Type u_2}
[normed_add_comm_group E]
[complete_space E]
{f : ι → E}
{g : ι → ℝ}
(hg : summable g)
(h : f =O[filter.cofinite] g) :
summable f
theorem
summable_of_is_O_nat
{E : Type u_1}
[normed_add_comm_group E]
[complete_space E]
{f : ℕ → E}
{g : ℕ → ℝ}
(hg : summable g)
(h : f =O[filter.at_top] g) :
summable f
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.