Basic properties of asymptotic relations #
This file establishes conversions, congruence and transitivity properties, behavior under filter
operations, and norm simplification lemmas for the asymptotic relations defined in
Mathlib.Analysis.Asymptotics.Defs.
Conversions #
theorem
Asymptotics.IsBigOWith.weaken
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c c' : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
(h : IsBigOWith c l f g')
(hc : c ≤ c')
:
IsBigOWith c' l f g'
theorem
Asymptotics.IsBigOWith.exists_pos
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
(h : IsBigOWith c l f g')
:
∃ c' > 0, IsBigOWith c' l f g'
theorem
Asymptotics.IsBigO.exists_pos
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
(h : f =O[l] g')
:
∃ c > 0, IsBigOWith c l f g'
theorem
Asymptotics.IsBigOWith.exists_nonneg
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
(h : IsBigOWith c l f g')
:
∃ c' ≥ 0, IsBigOWith c' l f g'
theorem
Asymptotics.IsBigO.exists_nonneg
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
(h : f =O[l] g')
:
∃ c ≥ 0, IsBigOWith c l f g'
theorem
Asymptotics.isBigO_iff_eventually_isBigOWith
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
f = O(g) if and only if IsBigOWith c f g for all sufficiently large c.
theorem
Asymptotics.isBigO_iff_eventually
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup 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.isLittleO_of_subsingleton
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Subsingleton E']
:
theorem
Asymptotics.isBigO_of_subsingleton
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
[Subsingleton E']
:
Congruence #
theorem
Asymptotics.IsBigOWith.congr
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c₁ c₂ : ℝ}
{l : Filter α}
{f₁ f₂ : α → E}
{g₁ g₂ : α → F}
(h : IsBigOWith c₁ l f₁ g₁)
(hc : c₁ = c₂)
(hf : ∀ (x : α), f₁ x = f₂ x)
(hg : ∀ (x : α), g₁ x = g₂ x)
:
IsBigOWith c₂ l f₂ g₂
theorem
Asymptotics.IsBigOWith.congr_left
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c : ℝ}
{g : α → F}
{l : Filter α}
{f₁ f₂ : α → E}
(h : IsBigOWith c l f₁ g)
(hf : ∀ (x : α), f₁ x = f₂ x)
:
IsBigOWith c l f₂ g
theorem
Asymptotics.IsBigOWith.congr_right
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c : ℝ}
{f : α → E}
{l : Filter α}
{g₁ g₂ : α → F}
(h : IsBigOWith c l f g₁)
(hg : ∀ (x : α), g₁ x = g₂ x)
:
IsBigOWith c l f g₂
theorem
Asymptotics.IsBigOWith.congr_const
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c₁ c₂ : ℝ}
{f : α → E}
{g : α → F}
{l : Filter α}
(h : IsBigOWith c₁ l f g)
(hc : c₁ = c₂)
:
IsBigOWith c₂ l f g
Filter operations and transitivity #
theorem
Asymptotics.IsBigOWith.comp_tendsto
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l : Filter α}
(hcfg : IsBigOWith c l f g)
{k : β → α}
{l' : Filter β}
(hk : Filter.Tendsto k l' l)
:
IsBigOWith c l' (f ∘ k) (g ∘ k)
theorem
Asymptotics.IsBigOWith.mono
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l l' : Filter α}
(h : IsBigOWith c l' f g)
(hl : l ≤ l')
:
IsBigOWith c l f g
theorem
Asymptotics.IsBigOWith.trans
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[Norm E]
[Norm F]
[Norm G]
{c c' : ℝ}
{f : α → E}
{g : α → F}
{k : α → G}
{l : Filter α}
(hfg : IsBigOWith c l f g)
(hgk : IsBigOWith c' l g k)
(hc : 0 ≤ c)
:
IsBigOWith (c * c') l f k
@[instance_reducible]
instance
Asymptotics.transIsBigOIsBigO
{α : Type u_1}
{E : Type u_3}
{G : Type u_5}
{F' : Type u_7}
[Norm E]
[Norm G]
[SeminormedAddCommGroup F']
{l : Filter α}
:
Equations
- Asymptotics.transIsBigOIsBigO = { trans := ⋯ }
@[instance_reducible]
instance
Asymptotics.transIsLittleOIsBigO
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
{G' : Type u_8}
[Norm E]
[Norm F]
[SeminormedAddCommGroup G']
{l : Filter α}
:
Equations
- Asymptotics.transIsLittleOIsBigO = { trans := ⋯ }
@[instance_reducible]
instance
Asymptotics.transIsBigOIsLittleO
{α : Type u_1}
{E : Type u_3}
{G : Type u_5}
{F' : Type u_7}
[Norm E]
[Norm G]
[SeminormedAddCommGroup F']
{l : Filter α}
:
Equations
- Asymptotics.transIsBigOIsLittleO = { trans := ⋯ }
theorem
Filter.Eventually.isBigO
{α : Type u_1}
{E : Type u_3}
[Norm E]
{f : α → E}
{g : α → ℝ}
{l : Filter α}
(hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ g x)
:
See also Asymptotics.IsBigO.of_norm_eventuallyLE, which is the same lemma
stated using Filter.EventuallyLE instead of Filter.Eventually.
theorem
Asymptotics.isBigOWith_refl
{α : Type u_1}
{E : Type u_3}
[Norm E]
(f : α → E)
(l : Filter α)
:
IsBigOWith 1 l f f
@[simp]
theorem
Asymptotics.isBigOWith_bot
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
(c : ℝ)
(f : α → E)
(g : α → F)
:
IsBigOWith c ⊥ f g
theorem
Asymptotics.IsBigOWith.sup
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
{c : ℝ}
{f : α → E}
{g : α → F}
{l l' : Filter α}
(h : IsBigOWith c l f g)
(h' : IsBigOWith c l' f g)
:
IsBigOWith c (l ⊔ l') f g
theorem
Asymptotics.IsBigOWith.sup'
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c c' : ℝ}
{f : α → E}
{g' : α → F'}
{l l' : Filter α}
(h : IsBigOWith c l f g')
(h' : IsBigOWith c' l' f g')
:
IsBigOWith (max c c') (l ⊔ l') f g'
theorem
Asymptotics.IsBigOWith.insert
{α : Type u_1}
{E : Type u_3}
{F : Type u_4}
[Norm E]
[Norm F]
[TopologicalSpace α]
{x : α}
{s : Set α}
{C : ℝ}
{g : α → E}
{g' : α → F}
(h1 : IsBigOWith C (nhdsWithin x s) g g')
(h2 : ‖g x‖ ≤ C * ‖g' x‖)
:
IsBigOWith C (nhdsWithin x (insert x s)) g g'
theorem
Asymptotics.isLittleO_insert
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[TopologicalSpace α]
{x : α}
{s : Set α}
{g : α → E'}
{g' : α → F'}
(h : g x = 0)
:
theorem
Asymptotics.IsLittleO.insert
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
[TopologicalSpace α]
{x : α}
{s : Set α}
{g : α → E'}
{g' : α → F'}
(h1 : g =o[nhdsWithin x s] g')
(h2 : g x = 0)
:
Simplification: norm #
@[simp]
theorem
Asymptotics.isBigOWith_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
theorem
Asymptotics.IsBigOWith.norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
IsBigOWith c l f g' → IsBigOWith c l f fun (x : α) => ‖g' x‖
Alias of the reverse direction of Asymptotics.isBigOWith_norm_right.
theorem
Asymptotics.IsBigOWith.of_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{c : ℝ}
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
(IsBigOWith c l f fun (x : α) => ‖g' x‖) → IsBigOWith c l f g'
Alias of the forward direction of Asymptotics.isBigOWith_norm_right.
theorem
Asymptotics.IsBigO.of_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isBigO_norm_right.
theorem
Asymptotics.IsBigO.norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isBigO_norm_right.
theorem
Asymptotics.IsLittleO.norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isLittleO_norm_right.
theorem
Asymptotics.IsLittleO.of_norm_right
{α : Type u_1}
{E : Type u_3}
{F' : Type u_7}
[Norm E]
[SeminormedAddCommGroup F']
{f : α → E}
{g' : α → F'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isLittleO_norm_right.
@[simp]
theorem
Asymptotics.isBigOWith_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
theorem
Asymptotics.IsBigOWith.norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
IsBigOWith c l f' g → IsBigOWith c l (fun (x : α) => ‖f' x‖) g
Alias of the reverse direction of Asymptotics.isBigOWith_norm_left.
theorem
Asymptotics.IsBigOWith.of_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{c : ℝ}
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
IsBigOWith c l (fun (x : α) => ‖f' x‖) g → IsBigOWith c l f' g
Alias of the forward direction of Asymptotics.isBigOWith_norm_left.
theorem
Asymptotics.IsBigO.of_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isBigO_norm_left.
theorem
Asymptotics.IsBigO.norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isBigO_norm_left.
theorem
Asymptotics.IsLittleO.norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isLittleO_norm_left.
theorem
Asymptotics.IsLittleO.of_norm_left
{α : Type u_1}
{F : Type u_4}
{E' : Type u_6}
[Norm F]
[SeminormedAddCommGroup E']
{g : α → F}
{f' : α → E'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isLittleO_norm_left.
theorem
Asymptotics.isBigOWith_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
theorem
Asymptotics.IsBigOWith.norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
IsBigOWith c l f' g' → IsBigOWith c l (fun (x : α) => ‖f' x‖) fun (x : α) => ‖g' x‖
Alias of the reverse direction of Asymptotics.isBigOWith_norm_norm.
theorem
Asymptotics.IsBigOWith.of_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{c : ℝ}
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
(IsBigOWith c l (fun (x : α) => ‖f' x‖) fun (x : α) => ‖g' x‖) → IsBigOWith c l f' g'
Alias of the forward direction of Asymptotics.isBigOWith_norm_norm.
theorem
Asymptotics.IsBigO.norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isBigO_norm_norm.
theorem
Asymptotics.IsBigO.of_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isBigO_norm_norm.
theorem
Asymptotics.IsLittleO.of_norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
Alias of the forward direction of Asymptotics.isLittleO_norm_norm.
theorem
Asymptotics.IsLittleO.norm_norm
{α : Type u_1}
{E' : Type u_6}
{F' : Type u_7}
[SeminormedAddCommGroup E']
[SeminormedAddCommGroup F']
{f' : α → E'}
{g' : α → F'}
{l : Filter α}
:
Alias of the reverse direction of Asymptotics.isLittleO_norm_norm.