Documentation

Mathlib.Analysis.Asymptotics.Asymptotics

Asymptotics #

We introduce these relations:

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 IsBigOWith c is introduced to factor out common algebraic arguments in the proofs of similar properties of IsBigO and IsLittleO. Usually proofs outside of this file should use IsBigO 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 ↔ (fun x ↦ ‖f x‖) =O[l] (fun x ↦ ‖g x‖),

and similarly for IsLittleO. 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 (fun 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 #

theorem Asymptotics.IsBigOWith_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (c : ) (l : Filter α) (f : αE) (g : αF) :
Asymptotics.IsBigOWith c l f g = ∀ᶠ (x : α) in l, f x c * g x
@[irreducible]
def Asymptotics.IsBigOWith {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (c : ) (l : Filter α) (f : αE) (g : αF) :

This version of the Landau notation IsBigOWith 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 IsBigO instead of this relation.

Equations
Instances For
    theorem Asymptotics.isBigOWith_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} :
    Asymptotics.IsBigOWith c l f g ∀ᶠ (x : α) in l, f x c * g x

    Definition of IsBigOWith. We record it in a lemma as IsBigOWith is irreducible.

    theorem Asymptotics.IsBigOWith.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} :
    Asymptotics.IsBigOWith c l f g∀ᶠ (x : α) in l, f x c * g x

    Alias of the forward direction of Asymptotics.isBigOWith_iff.


    Definition of IsBigOWith. We record it in a lemma as IsBigOWith is irreducible.

    theorem Asymptotics.IsBigOWith.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} :
    (∀ᶠ (x : α) in l, f x c * g x)Asymptotics.IsBigOWith c l f g

    Alias of the reverse direction of Asymptotics.isBigOWith_iff.


    Definition of IsBigOWith. We record it in a lemma as IsBigOWith is irreducible.

    theorem Asymptotics.IsBigO_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : Filter α) (f : αE) (g : αF) :
    f =O[l] g = ∃ (c : ), Asymptotics.IsBigOWith c l f g
    @[irreducible]
    def Asymptotics.IsBigO {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : Filter α) (f : αE) (g : αF) :

    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.

    Equations
    Instances For

      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Asymptotics.isBigO_iff_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
        f =O[l] g ∃ (c : ), Asymptotics.IsBigOWith c l f g

        Definition of IsBigO in terms of IsBigOWith. We record it in a lemma as IsBigO is irreducible.

        theorem Asymptotics.isBigO_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
        f =O[l] g ∃ (c : ), ∀ᶠ (x : α) in l, f x c * g x

        Definition of IsBigO in terms of filters.

        theorem Asymptotics.isBigO_iff' {α : Type u_1} {E : Type u_3} {E''' : Type u_12} [Norm E] [SeminormedAddGroup E'''] {f : αE} {l : Filter α} {g : αE'''} :
        f =O[l] g ∃ c > 0, ∀ᶠ (x : α) in l, f x c * g x

        Definition of IsBigO in terms of filters, with a positive constant.

        theorem Asymptotics.isBigO_iff'' {α : Type u_1} {E : Type u_3} {E''' : Type u_12} [Norm E] [SeminormedAddGroup E'''] {f : αE} {l : Filter α} {g : αE'''} :
        f =O[l] g ∃ c > 0, ∀ᶠ (x : α) in l, c * f x g x

        Definition of IsBigO in terms of filters, with the constant in the lower bound.

        theorem Asymptotics.IsBigO.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (c : ) (h : ∀ᶠ (x : α) in l, f x c * g x) :
        f =O[l] g
        theorem Asymptotics.IsBigO.of_bound' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h : ∀ᶠ (x : α) in l, f x g x) :
        f =O[l] g
        theorem Asymptotics.IsBigO.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
        f =O[l] g∃ (c : ), ∀ᶠ (x : α) in l, f x c * g x
        @[irreducible]
        def Asymptotics.IsLittleO {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : Filter α) (f : αE) (g : αF) :

        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.

        Equations
        Instances For
          theorem Asymptotics.IsLittleO_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : Filter α) (f : αE) (g : αF) :
          f =o[l] g = ∀ ⦃c : ⦄, 0 < cAsymptotics.IsBigOWith c l f g

          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.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Asymptotics.isLittleO_iff_forall_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            f =o[l] g ∀ ⦃c : ⦄, 0 < cAsymptotics.IsBigOWith c l f g

            Definition of IsLittleO in terms of IsBigOWith.

            theorem Asymptotics.IsLittleO.forall_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            f =o[l] g∀ ⦃c : ⦄, 0 < cAsymptotics.IsBigOWith c l f g

            Alias of the forward direction of Asymptotics.isLittleO_iff_forall_isBigOWith.


            Definition of IsLittleO in terms of IsBigOWith.

            theorem Asymptotics.IsLittleO.of_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            (∀ ⦃c : ⦄, 0 < cAsymptotics.IsBigOWith c l f g)f =o[l] g

            Alias of the reverse direction of Asymptotics.isLittleO_iff_forall_isBigOWith.


            Definition of IsLittleO in terms of IsBigOWith.

            theorem Asymptotics.isLittleO_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            f =o[l] g ∀ ⦃c : ⦄, 0 < c∀ᶠ (x : α) in l, f x c * g x

            Definition of IsLittleO in terms of filters.

            theorem Asymptotics.IsLittleO.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            (∀ ⦃c : ⦄, 0 < c∀ᶠ (x : α) in l, f x c * g x)f =o[l] g

            Alias of the reverse direction of Asymptotics.isLittleO_iff.


            Definition of IsLittleO in terms of filters.

            theorem Asymptotics.IsLittleO.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            f =o[l] g∀ ⦃c : ⦄, 0 < c∀ᶠ (x : α) in l, f x c * g x

            Alias of the forward direction of Asymptotics.isLittleO_iff.


            Definition of IsLittleO in terms of filters.

            theorem Asymptotics.IsLittleO.definition {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} (h : f =o[l] g) (hc : 0 < c) :
            ∀ᶠ (x : α) in l, f x c * g x
            theorem Asymptotics.IsLittleO.def' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} (h : f =o[l] g) (hc : 0 < c) :
            theorem Asymptotics.IsLittleO.eventuallyLE {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h : f =o[l] g) :
            ∀ᶠ (x : α) in l, f x g x

            Conversions #

            theorem Asymptotics.IsBigOWith.isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} (h : Asymptotics.IsBigOWith c l f g) :
            f =O[l] g
            theorem Asymptotics.IsLittleO.isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (hgf : f =o[l] g) :
            theorem Asymptotics.IsLittleO.isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (hgf : f =o[l] g) :
            f =O[l] g
            theorem Asymptotics.IsBigO.isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} :
            f =O[l] g∃ (c : ), Asymptotics.IsBigOWith c l f g
            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 : Asymptotics.IsBigOWith c l f g') (hc : c c') :
            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 : Asymptotics.IsBigOWith c l f g') :
            ∃ c' > 0, Asymptotics.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, Asymptotics.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 : Asymptotics.IsBigOWith c l f g') :
            ∃ c' ≥ 0, Asymptotics.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, Asymptotics.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[l] g' ∀ᶠ (c : ) in Filter.atTop, Asymptotics.IsBigOWith c l f g'

            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[l] g' ∀ᶠ (c : ) in Filter.atTop, ∀ᶠ (x : α) in l, f x c * g' x

            f = O(g) if and only if ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ for all sufficiently large c.

            theorem Asymptotics.IsBigO.exists_mem_basis {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} {ι : Sort u_17} {p : ιProp} {s : ιSet α} (h : f =O[l] g') (hb : Filter.HasBasis l p s) :
            ∃ c > 0, ∃ (i : ι), p i xs i, f x c * g' x
            theorem Asymptotics.isBigOWith_inv {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : Filter α} (hc : 0 < c) :
            Asymptotics.IsBigOWith c⁻¹ l f g ∀ᶠ (x : α) in l, c * f x g x
            theorem Asymptotics.isLittleO_iff_nat_mul_le_aux {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (h₀ : (∀ (x : α), 0 f x) ∀ (x : α), 0 g x) :
            f =o[l] g ∀ (n : ), ∀ᶠ (x : α) in l, n * f x g x
            theorem Asymptotics.isLittleO_iff_nat_mul_le {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            f =o[l] g' ∀ (n : ), ∀ᶠ (x : α) in l, n * f x g' x
            theorem Asymptotics.isLittleO_iff_nat_mul_le' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            f' =o[l] g ∀ (n : ), ∀ᶠ (x : α) in l, n * f' x g x

            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'] :
            f' =o[l] g'
            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'] :
            f' =O[l] g'

            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₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
            Asymptotics.IsBigOWith c₁ l f₁ g₁ Asymptotics.IsBigOWith c₂ l f₂ g₂
            theorem Asymptotics.IsBigOWith.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c₁ : } {c₂ : } {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : Asymptotics.IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
            Asymptotics.IsBigOWith c₂ l f₂ g₂
            theorem Asymptotics.IsBigOWith.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c₁ : } {c₂ : } {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : Asymptotics.IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
            Asymptotics.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₁ : αE} {f₂ : αE} (h : Asymptotics.IsBigOWith c l f₁ g) (hf : ∀ (x : α), f₁ x = f₂ x) :
            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₁ : αF} {g₂ : αF} (h : Asymptotics.IsBigOWith c l f g₁) (hg : ∀ (x : α), g₁ x = g₂ x) :
            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 : Asymptotics.IsBigOWith c₁ l f g) (hc : c₁ = c₂) :
            theorem Asymptotics.isBigO_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
            f₁ =O[l] g₁ f₂ =O[l] g₂
            theorem Asymptotics.IsBigO.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =O[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
            f₂ =O[l] g₂
            theorem Asymptotics.IsBigO.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =O[l] g₁) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
            f₂ =O[l] g₂
            theorem Asymptotics.IsBigO.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {g : αF} {l : Filter α} {f₁ : αE} {f₂ : αE} (h : f₁ =O[l] g) (hf : ∀ (x : α), f₁ x = f₂ x) :
            f₂ =O[l] g
            theorem Asymptotics.IsBigO.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {l : Filter α} {g₁ : αF} {g₂ : αF} (h : f =O[l] g₁) (hg : ∀ (x : α), g₁ x = g₂ x) :
            f =O[l] g₂
            theorem Asymptotics.isLittleO_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
            f₁ =o[l] g₁ f₂ =o[l] g₂
            theorem Asymptotics.IsLittleO.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =o[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
            f₂ =o[l] g₂
            theorem Asymptotics.IsLittleO.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =o[l] g₁) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
            f₂ =o[l] g₂
            theorem Asymptotics.IsLittleO.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {g : αF} {l : Filter α} {f₁ : αE} {f₂ : αE} (h : f₁ =o[l] g) (hf : ∀ (x : α), f₁ x = f₂ x) :
            f₂ =o[l] g
            theorem Asymptotics.IsLittleO.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {l : Filter α} {g₁ : αF} {g₂ : αF} (h : f =o[l] g₁) (hg : ∀ (x : α), g₁ x = g₂ x) :
            f =o[l] g₂
            theorem Filter.EventuallyEq.trans_isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g : αF} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =O[l] g) :
            f₁ =O[l] g
            instance Asymptotics.transEventuallyEqIsBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} :
            Trans (fun (x x_1 : αE) => x =ᶠ[l] x_1) (fun (x : αE) (x_1 : αF) => x =O[l] x_1) fun (x : αE) (x_1 : αF) => x =O[l] x_1
            Equations
            • Asymptotics.transEventuallyEqIsBigO = { trans := }
            theorem Filter.EventuallyEq.trans_isLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f₁ : αE} {f₂ : αE} {g : αF} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =o[l] g) :
            f₁ =o[l] g
            instance Asymptotics.transEventuallyEqIsLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} :
            Trans (fun (x x_1 : αE) => x =ᶠ[l] x_1) (fun (x : αE) (x_1 : αF) => x =o[l] x_1) fun (x : αE) (x_1 : αF) => x =o[l] x_1
            Equations
            • Asymptotics.transEventuallyEqIsLittleO = { trans := }
            theorem Asymptotics.IsBigO.trans_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : αE} {g₁ : αF} {g₂ : αF} (h : f =O[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
            f =O[l] g₂
            instance Asymptotics.transIsBigOEventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} :
            Trans (fun (x : αE) (x_1 : αF) => x =O[l] x_1) (fun (x x_1 : αF) => x =ᶠ[l] x_1) fun (x : αE) (x_1 : αF) => x =O[l] x_1
            Equations
            • Asymptotics.transIsBigOEventuallyEq = { trans := }
            theorem Asymptotics.IsLittleO.trans_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : αE} {g₁ : αF} {g₂ : αF} (h : f =o[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
            f =o[l] g₂
            instance Asymptotics.transIsLittleOEventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} :
            Trans (fun (x : αE) (x_1 : αF) => x =o[l] x_1) (fun (x x_1 : αF) => x =ᶠ[l] x_1) fun (x : αE) (x_1 : αF) => x =o[l] x_1
            Equations
            • Asymptotics.transIsLittleOEventuallyEq = { trans := }

            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 : Asymptotics.IsBigOWith c l f g) {k : βα} {l' : Filter β} (hk : Filter.Tendsto k l' l) :
            Asymptotics.IsBigOWith c l' (f k) (g k)
            theorem Asymptotics.IsBigO.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (hfg : f =O[l] g) {k : βα} {l' : Filter β} (hk : Filter.Tendsto k l' l) :
            (f k) =O[l'] (g k)
            theorem Asymptotics.IsLittleO.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} (hfg : f =o[l] g) {k : βα} {l' : Filter β} (hk : Filter.Tendsto k l' l) :
            (f k) =o[l'] (g k)
            @[simp]
            theorem Asymptotics.isBigOWith_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {k : βα} {l : Filter β} :
            @[simp]
            theorem Asymptotics.isBigO_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {k : βα} {l : Filter β} :
            f =O[Filter.map k l] g (f k) =O[l] (g k)
            @[simp]
            theorem Asymptotics.isLittleO_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {k : βα} {l : Filter β} :
            f =o[Filter.map k l] g (f k) =o[l] (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 : Filter α} {l' : Filter α} (h : Asymptotics.IsBigOWith c l' f g) (hl : l l') :
            theorem Asymptotics.IsBigO.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} {l' : Filter α} (h : f =O[l'] g) (hl : l l') :
            f =O[l] g
            theorem Asymptotics.IsLittleO.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} {l' : Filter α} (h : f =o[l'] g) (hl : l l') :
            f =o[l] 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 : Asymptotics.IsBigOWith c l f g) (hgk : Asymptotics.IsBigOWith c' l g k) (hc : 0 c) :
            theorem Asymptotics.IsBigO.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (hfg : f =O[l] g) (hgk : g =O[l] k) :
            f =O[l] k
            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 α} :
            Trans (fun (x : αE) (x_1 : αF') => x =O[l] x_1) (fun (x : αF') (x_1 : αG) => x =O[l] x_1) fun (x : αE) (x_1 : αG) => x =O[l] x_1
            Equations
            • Asymptotics.transIsBigOIsBigO = { trans := }
            theorem Asymptotics.IsLittleO.trans_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {f : αE} {g : αF} {k : αG} {l : Filter α} (hfg : f =o[l] g) (hgk : Asymptotics.IsBigOWith c l g k) (hc : 0 < c) :
            f =o[l] k
            theorem Asymptotics.IsLittleO.trans_isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [Norm E] [Norm F] [SeminormedAddCommGroup G'] {l : Filter α} {f : αE} {g : αF} {k : αG'} (hfg : f =o[l] g) (hgk : g =O[l] k) :
            f =o[l] k
            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 α} :
            Trans (fun (x : αE) (x_1 : αF) => x =o[l] x_1) (fun (x : αF) (x_1 : αG') => x =O[l] x_1) fun (x : αE) (x_1 : αG') => x =o[l] x_1
            Equations
            • Asymptotics.transIsLittleOIsBigO = { trans := }
            theorem Asymptotics.IsBigOWith.trans_isLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {f : αE} {g : αF} {k : αG} {l : Filter α} (hfg : Asymptotics.IsBigOWith c l f g) (hgk : g =o[l] k) (hc : 0 < c) :
            f =o[l] k
            theorem Asymptotics.IsBigO.trans_isLittleO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (hfg : f =O[l] g) (hgk : g =o[l] k) :
            f =o[l] k
            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 α} :
            Trans (fun (x : αE) (x_1 : αF') => x =O[l] x_1) (fun (x : αF') (x_1 : αG) => x =o[l] x_1) fun (x : αE) (x_1 : αG) => x =o[l] x_1
            Equations
            • Asymptotics.transIsBigOIsLittleO = { trans := }
            theorem Asymptotics.IsLittleO.trans {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {l : Filter α} {f : αE} {g : αF} {k : αG} (hfg : f =o[l] g) (hgk : g =o[l] k) :
            f =o[l] k
            instance Asymptotics.transIsLittleOIsLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {l : Filter α} :
            Trans (fun (x : αE) (x_1 : αF) => x =o[l] x_1) (fun (x : αF) (x_1 : αG) => x =o[l] x_1) fun (x : αE) (x_1 : αG) => x =o[l] x_1
            Equations
            • Asymptotics.transIsLittleOIsLittleO = { trans := }
            theorem Filter.Eventually.trans_isBigO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {f : αE} {g : αF'} {k : αG} (hfg : ∀ᶠ (x : α) in l, f x g x) (hgk : g =O[l] k) :
            f =O[l] k
            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) :
            f =O[l] g
            theorem Asymptotics.isBigOWith_of_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} (l : Filter α) (hfg : ∀ (x : α), f x c * g x) :
            theorem Asymptotics.isBigOWith_of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} (l : Filter α) (hfg : ∀ (x : α), f x g x) :
            theorem Asymptotics.isBigO_of_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} (l : Filter α) (hfg : ∀ (x : α), f x c * g x) :
            f =O[l] g
            theorem Asymptotics.isBigO_of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} (l : Filter α) (hfg : ∀ (x : α), f x g x) :
            f =O[l] g
            theorem Asymptotics.isBigOWith_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : αE) (l : Filter α) :
            theorem Asymptotics.isBigO_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : αE) (l : Filter α) :
            f =O[l] f
            theorem Filter.EventuallyEq.isBigO {α : Type u_1} {E : Type u_3} [Norm E] {l : Filter α} {f₁ : αE} {f₂ : αE} (hf : f₁ =ᶠ[l] f₂) :
            f₁ =O[l] f₂
            theorem Asymptotics.IsBigOWith.trans_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {f : αE} {g : αF} {k : αG} {l : Filter α} (hfg : Asymptotics.IsBigOWith c l f g) (hgk : ∀ (x : α), g x k x) (hc : 0 c) :
            theorem Asymptotics.IsBigO.trans_le {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {f : αE} {k : αG} {g' : αF'} {l : Filter α} (hfg : f =O[l] g') (hgk : ∀ (x : α), g' x k x) :
            f =O[l] k
            theorem Asymptotics.IsLittleO.trans_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {f : αE} {g : αF} {k : αG} {l : Filter α} (hfg : f =o[l] g) (hgk : ∀ (x : α), g x k x) :
            f =o[l] k
            theorem Asymptotics.isLittleO_irrefl' {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {f' : αE'} {l : Filter α} (h : ∃ᶠ (x : α) in l, f' x 0) :
            ¬f' =o[l] f'
            theorem Asymptotics.isLittleO_irrefl {α : Type u_1} {E'' : Type u_9} [NormedAddCommGroup E''] {f'' : αE''} {l : Filter α} (h : ∃ᶠ (x : α) in l, f'' x 0) :
            ¬f'' =o[l] f''
            theorem Asymptotics.IsBigO.not_isLittleO {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : αF'} {f'' : αE''} {l : Filter α} (h : f'' =O[l] g') (hf : ∃ᶠ (x : α) in l, f'' x 0) :
            ¬g' =o[l] f''
            theorem Asymptotics.IsLittleO.not_isBigO {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : αF'} {f'' : αE''} {l : Filter α} (h : f'' =o[l] g') (hf : ∃ᶠ (x : α) in l, f'' x 0) :
            ¬g' =O[l] 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) :
            @[simp]
            theorem Asymptotics.isBigO_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (f : αE) (g : αF) :
            @[simp]
            theorem Asymptotics.isLittleO_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (f : αE) (g : αF) :
            @[simp]
            theorem Asymptotics.isBigOWith_pure {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {x : α} :
            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 : Filter α} {l' : Filter α} (h : Asymptotics.IsBigOWith c l f g) (h' : Asymptotics.IsBigOWith c 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 : Filter α} {l' : Filter α} (h : Asymptotics.IsBigOWith c l f g') (h' : Asymptotics.IsBigOWith c' l' f g') :
            Asymptotics.IsBigOWith (max c c') (l l') f g'
            theorem Asymptotics.IsBigO.sup {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} {l' : Filter α} (h : f =O[l] g') (h' : f =O[l'] g') :
            f =O[l l'] g'
            theorem Asymptotics.IsLittleO.sup {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} {l' : Filter α} (h : f =o[l] g) (h' : f =o[l'] g) :
            f =o[l l'] g
            @[simp]
            theorem Asymptotics.isBigO_sup {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} {l' : Filter α} :
            f =O[l l'] g' f =O[l] g' f =O[l'] g'
            @[simp]
            theorem Asymptotics.isLittleO_sup {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : Filter α} {l' : Filter α} :
            f =o[l l'] g f =o[l] g f =o[l'] 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} (h : g x C * g' x) :
            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 : Asymptotics.IsBigOWith C (nhdsWithin x s) g g') (h2 : g x C * g' x) :
            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) :
            g =o[nhdsWithin x (insert x s)] g' g =o[nhdsWithin x s] 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'} (h1 : g =o[nhdsWithin x s] g') (h2 : g x = 0) :
            g =o[nhdsWithin x (insert x s)] g'

            Simplification : norm, abs #

            @[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 α} :
            (Asymptotics.IsBigOWith c l f fun (x : α) => g' x) Asymptotics.IsBigOWith c l f g'
            @[simp]
            theorem Asymptotics.isBigOWith_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {c : } {f : αE} {l : Filter α} {u : α} :
            (Asymptotics.IsBigOWith c l f fun (x : α) => |u x|) Asymptotics.IsBigOWith c l f u
            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 α} :
            Asymptotics.IsBigOWith c l f g'Asymptotics.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 α} :
            (Asymptotics.IsBigOWith c l f fun (x : α) => g' x)Asymptotics.IsBigOWith c l f g'

            Alias of the forward direction of Asymptotics.isBigOWith_norm_right.

            theorem Asymptotics.IsBigOWith.of_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {c : } {f : αE} {l : Filter α} {u : α} :
            (Asymptotics.IsBigOWith c l f fun (x : α) => |u x|)Asymptotics.IsBigOWith c l f u

            Alias of the forward direction of Asymptotics.isBigOWith_abs_right.

            theorem Asymptotics.IsBigOWith.abs_right {α : Type u_1} {E : Type u_3} [Norm E] {c : } {f : αE} {l : Filter α} {u : α} :
            Asymptotics.IsBigOWith c l f uAsymptotics.IsBigOWith c l f fun (x : α) => |u x|

            Alias of the reverse direction of Asymptotics.isBigOWith_abs_right.

            @[simp]
            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 α} :
            (f =O[l] fun (x : α) => g' x) f =O[l] g'
            @[simp]
            theorem Asymptotics.isBigO_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} {u : α} :
            (f =O[l] fun (x : α) => |u x|) f =O[l] u
            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 α} :
            (f =O[l] fun (x : α) => g' x)f =O[l] g'

            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 α} :
            f =O[l] g'f =O[l] fun (x : α) => g' x

            Alias of the reverse direction of Asymptotics.isBigO_norm_right.

            theorem Asymptotics.IsBigO.abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} {u : α} :
            f =O[l] uf =O[l] fun (x : α) => |u x|

            Alias of the reverse direction of Asymptotics.isBigO_abs_right.

            theorem Asymptotics.IsBigO.of_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} {u : α} :
            (f =O[l] fun (x : α) => |u x|)f =O[l] u

            Alias of the forward direction of Asymptotics.isBigO_abs_right.

            @[simp]
            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 α} :
            (f =o[l] fun (x : α) => g' x) f =o[l] g'
            @[simp]
            theorem Asymptotics.isLittleO_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} {u : α} :
            (f =o[l] fun (x : α) => |u x|) f =o[l] u
            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 α} :
            (f =o[l] fun (x : α) => g' x)f =o[l] g'

            Alias of the forward direction of Asymptotics.isLittleO_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 α} :
            f =o[l] g'f =o[l] fun (x : α) => g' x

            Alias of the reverse direction of Asymptotics.isLittleO_norm_right.

            theorem Asymptotics.IsLittleO.of_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} {u : α} :
            (f =o[l] fun (x : α) => |u x|)f =o[l] u

            Alias of the forward direction of Asymptotics.isLittleO_abs_right.

            theorem Asymptotics.IsLittleO.abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : Filter α} {u : α} :
            f =o[l] uf =o[l] fun (x : α) => |u x|

            Alias of the reverse direction of Asymptotics.isLittleO_abs_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 α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => f' x) g Asymptotics.IsBigOWith c l f' g
            @[simp]
            theorem Asymptotics.isBigOWith_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {c : } {g : αF} {l : Filter α} {u : α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) g Asymptotics.IsBigOWith c l u g
            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 α} :
            Asymptotics.IsBigOWith c l f' gAsymptotics.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 α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => f' x) gAsymptotics.IsBigOWith c l f' g

            Alias of the forward direction of Asymptotics.isBigOWith_norm_left.

            theorem Asymptotics.IsBigOWith.of_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {c : } {g : αF} {l : Filter α} {u : α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) gAsymptotics.IsBigOWith c l u g

            Alias of the forward direction of Asymptotics.isBigOWith_abs_left.

            theorem Asymptotics.IsBigOWith.abs_left {α : Type u_1} {F : Type u_4} [Norm F] {c : } {g : αF} {l : Filter α} {u : α} :
            Asymptotics.IsBigOWith c l u gAsymptotics.IsBigOWith c l (fun (x : α) => |u x|) g

            Alias of the reverse direction of Asymptotics.isBigOWith_abs_left.

            @[simp]
            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 α} :
            (fun (x : α) => f' x) =O[l] g f' =O[l] g
            @[simp]
            theorem Asymptotics.isBigO_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : Filter α} {u : α} :
            (fun (x : α) => |u x|) =O[l] g u =O[l] g
            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 α} :
            f' =O[l] g(fun (x : α) => f' x) =O[l] g

            Alias of the reverse direction of Asymptotics.isBigO_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 α} :
            (fun (x : α) => f' x) =O[l] gf' =O[l] g

            Alias of the forward direction of Asymptotics.isBigO_norm_left.

            theorem Asymptotics.IsBigO.abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : Filter α} {u : α} :
            u =O[l] g(fun (x : α) => |u x|) =O[l] g

            Alias of the reverse direction of Asymptotics.isBigO_abs_left.

            theorem Asymptotics.IsBigO.of_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : Filter α} {u : α} :
            (fun (x : α) => |u x|) =O[l] gu =O[l] g

            Alias of the forward direction of Asymptotics.isBigO_abs_left.

            @[simp]
            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 α} :
            (fun (x : α) => f' x) =o[l] g f' =o[l] g
            @[simp]
            theorem Asymptotics.isLittleO_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : Filter α} {u : α} :
            (fun (x : α) => |u x|) =o[l] g u =o[l] g
            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 α} :
            f' =o[l] g(fun (x : α) => f' x) =o[l] g

            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 α} :
            (fun (x : α) => f' x) =o[l] gf' =o[l] g

            Alias of the forward direction of Asymptotics.isLittleO_norm_left.

            theorem Asymptotics.IsLittleO.abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : Filter α} {u : α} :
            u =o[l] g(fun (x : α) => |u x|) =o[l] g

            Alias of the reverse direction of Asymptotics.isLittleO_abs_left.

            theorem Asymptotics.IsLittleO.of_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : Filter α} {u : α} :
            (fun (x : α) => |u x|) =o[l] gu =o[l] g

            Alias of the forward direction of Asymptotics.isLittleO_abs_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 α} :
            (Asymptotics.IsBigOWith c l (fun (x : α) => f' x) fun (x : α) => g' x) Asymptotics.IsBigOWith c l f' g'
            theorem Asymptotics.isBigOWith_abs_abs {α : Type u_1} {c : } {l : Filter α} {u : α} {v : α} :
            (Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|) Asymptotics.IsBigOWith c l u v
            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 α} :
            (Asymptotics.IsBigOWith c l (fun (x : α) => f' x) fun (x : α) => g' x)Asymptotics.IsBigOWith c l f' g'

            Alias of the forward direction of Asymptotics.isBigOWith_norm_norm.

            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 α} :
            Asymptotics.IsBigOWith c l f' g'Asymptotics.IsBigOWith c l (fun (x : α) => f' x) fun (x : α) => g' x

            Alias of the reverse direction of Asymptotics.isBigOWith_norm_norm.

            theorem Asymptotics.IsBigOWith.abs_abs {α : Type u_1} {c : } {l : Filter α} {u : α} {v : α} :
            Asymptotics.IsBigOWith c l u vAsymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|

            Alias of the reverse direction of Asymptotics.isBigOWith_abs_abs.

            theorem Asymptotics.IsBigOWith.of_abs_abs {α : Type u_1} {c : } {l : Filter α} {u : α} {v : α} :
            (Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|)Asymptotics.IsBigOWith c l u v

            Alias of the forward direction of Asymptotics.isBigOWith_abs_abs.

            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 α} :
            ((fun (x : α) => f' x) =O[l] fun (x : α) => g' x) f' =O[l] g'
            theorem Asymptotics.isBigO_abs_abs {α : Type u_1} {l : Filter α} {u : α} {v : α} :
            ((fun (x : α) => |u x|) =O[l] fun (x : α) => |v x|) u =O[l] v
            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 α} :
            ((fun (x : α) => f' x) =O[l] fun (x : α) => g' x)f' =O[l] g'

            Alias of the forward direction of Asymptotics.isBigO_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 α} :
            f' =O[l] g'(fun (x : α) => f' x) =O[l] fun (x : α) => g' x

            Alias of the reverse direction of Asymptotics.isBigO_norm_norm.

            theorem Asymptotics.IsBigO.of_abs_abs {α : Type u_1} {l : Filter α} {u : α} {v : α} :
            ((fun (x : α) => |u x|) =O[l] fun (x : α) => |v x|)u =O[l] v

            Alias of the forward direction of Asymptotics.isBigO_abs_abs.

            theorem Asymptotics.IsBigO.abs_abs {α : Type u_1} {l : Filter α} {u : α} {v : α} :
            u =O[l] v(fun (x : α) => |u x|) =O[l] fun (x : α) => |v x|

            Alias of the reverse direction of Asymptotics.isBigO_abs_abs.

            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 α} :
            ((fun (x : α) => f' x) =o[l] fun (x : α) => g' x) f' =o[l] g'
            theorem Asymptotics.isLittleO_abs_abs {α : Type u_1} {l : Filter α} {u : α} {v : α} :
            ((fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|) u =o[l] v
            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 α} :
            f' =o[l] g'(fun (x : α) => f' x) =o[l] fun (x : α) => g' x

            Alias of the reverse direction of Asymptotics.isLittleO_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 α} :
            ((fun (x : α) => f' x) =o[l] fun (x : α) => g' x)f' =o[l] g'

            Alias of the forward direction of Asymptotics.isLittleO_norm_norm.

            theorem Asymptotics.IsLittleO.of_abs_abs {α : Type u_1} {l : Filter α} {u : α} {v : α} :
            ((fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|)u =o[l] v

            Alias of the forward direction of Asymptotics.isLittleO_abs_abs.

            theorem Asymptotics.IsLittleO.abs_abs {α : Type u_1} {l : Filter α} {u : α} {v : α} :
            u =o[l] v(fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|

            Alias of the reverse direction of Asymptotics.isLittleO_abs_abs.

            Simplification: negate #

            @[simp]
            theorem Asymptotics.isBigOWith_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : } {f : αE} {g' : αF'} {l : Filter α} :
            (Asymptotics.IsBigOWith c l f fun (x : α) => -g' x) Asymptotics.IsBigOWith c l f g'
            theorem Asymptotics.IsBigOWith.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : } {f : αE} {g' : αF'} {l : Filter α} :
            (Asymptotics.IsBigOWith c l f fun (x : α) => -g' x)Asymptotics.IsBigOWith c l f g'

            Alias of the forward direction of Asymptotics.isBigOWith_neg_right.

            theorem Asymptotics.IsBigOWith.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : } {f : αE} {g' : αF'} {l : Filter α} :
            Asymptotics.IsBigOWith c l f g'Asymptotics.IsBigOWith c l f fun (x : α) => -g' x

            Alias of the reverse direction of Asymptotics.isBigOWith_neg_right.

            @[simp]
            theorem Asymptotics.isBigO_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            (f =O[l] fun (x : α) => -g' x) f =O[l] g'
            theorem Asymptotics.IsBigO.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            f =O[l] g'f =O[l] fun (x : α) => -g' x

            Alias of the reverse direction of Asymptotics.isBigO_neg_right.

            theorem Asymptotics.IsBigO.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            (f =O[l] fun (x : α) => -g' x)f =O[l] g'

            Alias of the forward direction of Asymptotics.isBigO_neg_right.

            @[simp]
            theorem Asymptotics.isLittleO_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            (f =o[l] fun (x : α) => -g' x) f =o[l] g'
            theorem Asymptotics.IsLittleO.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            f =o[l] g'f =o[l] fun (x : α) => -g' x

            Alias of the reverse direction of Asymptotics.isLittleO_neg_right.

            theorem Asymptotics.IsLittleO.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} :
            (f =o[l] fun (x : α) => -g' x)f =o[l] g'

            Alias of the forward direction of Asymptotics.isLittleO_neg_right.

            @[simp]
            theorem Asymptotics.isBigOWith_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : } {g : αF} {f' : αE'} {l : Filter α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => -f' x) g Asymptotics.IsBigOWith c l f' g
            theorem Asymptotics.IsBigOWith.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : } {g : αF} {f' : αE'} {l : Filter α} :
            Asymptotics.IsBigOWith c l f' gAsymptotics.IsBigOWith c l (fun (x : α) => -f' x) g

            Alias of the reverse direction of Asymptotics.isBigOWith_neg_left.

            theorem Asymptotics.IsBigOWith.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : } {g : αF} {f' : αE'} {l : Filter α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => -f' x) gAsymptotics.IsBigOWith c l f' g

            Alias of the forward direction of Asymptotics.isBigOWith_neg_left.

            @[simp]
            theorem Asymptotics.isBigO_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            (fun (x : α) => -f' x) =O[l] g f' =O[l] g
            theorem Asymptotics.IsBigO.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            f' =O[l] g(fun (x : α) => -f' x) =O[l] g

            Alias of the reverse direction of Asymptotics.isBigO_neg_left.

            theorem Asymptotics.IsBigO.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            (fun (x : α) => -f' x) =O[l] gf' =O[l] g

            Alias of the forward direction of Asymptotics.isBigO_neg_left.

            @[simp]
            theorem Asymptotics.isLittleO_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            (fun (x : α) => -f' x) =o[l] g f' =o[l] g
            theorem Asymptotics.IsLittleO.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            f' =o[l] g(fun (x : α) => -f' x) =o[l] g

            Alias of the reverse direction of Asymptotics.isLittleO_neg_left.

            theorem Asymptotics.IsLittleO.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {f' : αE'} {l : Filter α} :
            (fun (x : α) => -f' x) =o[l] gf' =o[l] g

            Alias of the forward direction of Asymptotics.isLittleO_neg_left.

            Product of functions (right) #

            theorem Asymptotics.isBigOWith_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} :
            Asymptotics.IsBigOWith 1 l f' fun (x : α) => (f' x, g' x)
            theorem Asymptotics.isBigOWith_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} :
            Asymptotics.IsBigOWith 1 l g' fun (x : α) => (f' x, g' x)
            theorem Asymptotics.isBigO_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} :
            f' =O[l] fun (x : α) => (f' x, g' x)
            theorem Asymptotics.isBigO_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} {g' : αF'} {l : Filter α} :
            g' =O[l] fun (x : α) => (f' x, g' x)
            theorem Asymptotics.isBigO_fst_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {f' : αE' × F'} :
            (fun (x : α) => (f' x).1) =O[l] f'
            theorem Asymptotics.isBigO_snd_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {f' : αE' × F'} :
            (fun (x : α) => (f' x).2) =O[l] f'
            theorem Asymptotics.IsBigOWith.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : } {f : αE} {g' : αF'} (k' : αG') {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') (hc : 0 c) :
            Asymptotics.IsBigOWith c l f fun (x : α) => (g' x, k' x)
            theorem Asymptotics.IsBigO.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : αE} {g' : αF'} (k' : αG') {l : Filter α} (h : f =O[l] g') :
            f =O[l] fun (x : α) => (g' x, k' x)
            theorem Asymptotics.IsLittleO.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : αE} {g' : αF'} (k' : αG') {l : Filter α} (h : f =o[l] g') :
            f =o[l] fun (x : α) => (g' x, k' x)
            theorem Asymptotics.IsBigOWith.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : } {f : αE} (f' : αE') {g' : αF'} {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') (hc : 0 c) :
            Asymptotics.IsBigOWith c l f fun (x : α) => (f' x, g' x)
            theorem Asymptotics.IsBigO.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f : αE} (f' : αE') {g' : αF'} {l : Filter α} (h : f =O[l] g') :
            f =O[l] fun (x : α) => (f' x, g' x)
            theorem Asymptotics.IsLittleO.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f : αE} (f' : αE') {g' : αF'} {l : Filter α} (h : f =o[l] g') :
            f =o[l] fun (x : α) => (f' x, g' x)
            theorem Asymptotics.IsBigOWith.prod_left_same {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} (hf : Asymptotics.IsBigOWith c l f' k') (hg : Asymptotics.IsBigOWith c l g' k') :
            Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k'
            theorem Asymptotics.IsBigOWith.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : } {c' : } {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} (hf : Asymptotics.IsBigOWith c l f' k') (hg : Asymptotics.IsBigOWith c' l g' k') :
            Asymptotics.IsBigOWith (max c c') l (fun (x : α) => (f' x, g' x)) k'
            theorem Asymptotics.IsBigOWith.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} (h : Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') :
            theorem Asymptotics.IsBigOWith.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} (h : Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') :
            theorem Asymptotics.isBigOWith_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k' Asymptotics.IsBigOWith c l f' k' Asymptotics.IsBigOWith c l g' k'
            theorem Asymptotics.IsBigO.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} (hf : f' =O[l] k') (hg : g' =O[l] k') :
            (fun (x : α) => (f' x, g' x)) =O[l] k'
            theorem Asymptotics.IsBigO.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            (fun (x : α) => (f' x, g' x)) =O[l] k'f' =O[l] k'
            theorem Asymptotics.IsBigO.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            (fun (x : α) => (f' x, g' x)) =O[l] k'g' =O[l] k'
            @[simp]
            theorem Asymptotics.isBigO_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            (fun (x : α) => (f' x, g' x)) =O[l] k' f' =O[l] k' g' =O[l] k'
            theorem Asymptotics.IsLittleO.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} (hf : f' =o[l] k') (hg : g' =o[l] k') :
            (fun (x : α) => (f' x, g' x)) =o[l] k'
            theorem Asymptotics.IsLittleO.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            (fun (x : α) => (f' x, g' x)) =o[l] k'f' =o[l] k'
            theorem Asymptotics.IsLittleO.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            (fun (x : α) => (f' x, g' x)) =o[l] k'g' =o[l] k'
            @[simp]
            theorem Asymptotics.isLittleO_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : αE'} {g' : αF'} {k' : αG'} {l : Filter α} :
            (fun (x : α) => (f' x, g' x)) =o[l] k' f' =o[l] k' g' =o[l] k'
            theorem Asymptotics.IsBigOWith.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {c : } {f'' : αE''} {g'' : αF''} {l : Filter α} (h : Asymptotics.IsBigOWith c l f'' g'') :
            ∀ᶠ (x : α) in l, g'' x = 0f'' x = 0
            theorem Asymptotics.IsBigO.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {g'' : αF''} {l : Filter α} (h : f'' =O[l] g'') :
            ∀ᶠ (x : α) in l, g'' x = 0f'' x = 0

            Addition and subtraction #

            theorem Asymptotics.IsBigOWith.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c₁ : } {c₂ : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : Asymptotics.IsBigOWith c₂ l f₂ g) :
            Asymptotics.IsBigOWith (c₁ + c₂) l (fun (x : α) => f₁ x + f₂ x) g
            theorem Asymptotics.IsBigO.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) :
            (fun (x : α) => f₁ x + f₂ x) =O[l] g
            theorem Asymptotics.IsLittleO.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) :
            (fun (x : α) => f₁ x + f₂ x) =o[l] g
            theorem Asymptotics.IsLittleO.add_add {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {f₁ : αE'} {f₂ : αE'} {g₁ : αF'} {g₂ : αF'} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
            (fun (x : α) => f₁ x + f₂ x) =o[l] fun (x : α) => g₁ x + g₂ x
            theorem Asymptotics.IsBigO.add_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =o[l] g) :
            (fun (x : α) => f₁ x + f₂ x) =O[l] g
            theorem Asymptotics.IsLittleO.add_isBigO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =O[l] g) :
            (fun (x : α) => f₁ x + f₂ x) =O[l] g
            theorem Asymptotics.IsBigOWith.add_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c₁ : } {c₂ : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
            Asymptotics.IsBigOWith c₂ l (fun (x : α) => f₁ x + f₂ x) g
            theorem Asymptotics.IsLittleO.add_isBigOWith {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c₁ : } {c₂ : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : Asymptotics.IsBigOWith c₁ l f₂ g) (hc : c₁ < c₂) :
            Asymptotics.IsBigOWith c₂ l (fun (x : α) => f₁ x + f₂ x) g
            theorem Asymptotics.IsBigOWith.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c₁ : } {c₂ : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : Asymptotics.IsBigOWith c₂ l f₂ g) :
            Asymptotics.IsBigOWith (c₁ + c₂) l (fun (x : α) => f₁ x - f₂ x) g
            theorem Asymptotics.IsBigOWith.sub_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c₁ : } {c₂ : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
            Asymptotics.IsBigOWith c₂ l (fun (x : α) => f₁ x - f₂ x) g
            theorem Asymptotics.IsBigO.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) :
            (fun (x : α) => f₁ x - f₂ x) =O[l] g
            theorem Asymptotics.IsLittleO.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) :
            (fun (x : α) => f₁ x - f₂ x) =o[l] g

            Lemmas about IsBigO (f₁ - f₂) g l / IsLittleO (f₁ - f₂) g l treated as a binary relation #

            theorem Asymptotics.IsBigOWith.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : Asymptotics.IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g) :
            Asymptotics.IsBigOWith c l (fun (x : α) => f₂ x - f₁ x) g
            theorem Asymptotics.isBigOWith_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} :
            Asymptotics.IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g Asymptotics.IsBigOWith c l (fun (x : α) => f₂ x - f₁ x) g
            theorem Asymptotics.IsBigO.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =O[l] g) :
            (fun (x : α) => f₂ x - f₁ x) =O[l] g
            theorem Asymptotics.isBigO_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} :
            (fun (x : α) => f₁ x - f₂ x) =O[l] g (fun (x : α) => f₂ x - f₁ x) =O[l] g
            theorem Asymptotics.IsLittleO.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =o[l] g) :
            (fun (x : α) => f₂ x - f₁ x) =o[l] g
            theorem Asymptotics.isLittleO_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} :
            (fun (x : α) => f₁ x - f₂ x) =o[l] g (fun (x : α) => f₂ x - f₁ x) =o[l] g
            theorem Asymptotics.IsBigOWith.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : } {c' : } {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} {f₃ : αE'} (h₁ : Asymptotics.IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g) (h₂ : Asymptotics.IsBigOWith c' l (fun (x : α) => f₂ x - f₃ x) g) :
            Asymptotics.IsBigOWith (c + c') l (fun (x : α) => f₁ x - f₃ x) g
            theorem Asymptotics.IsBigO.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} {f₃ : αE'} (h₁ : (fun (x : α) => f₁ x - f₂ x) =O[l] g) (h₂ : (fun (x : α) => f₂ x - f₃ x) =O[l] g) :
            (fun (x : α) => f₁ x - f₃ x) =O[l] g
            theorem Asymptotics.IsLittleO.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} {f₃ : αE'} (h₁ : (fun (x : α) => f₁ x - f₂ x) =o[l] g) (h₂ : (fun (x : α) => f₂ x - f₃ x) =o[l] g) :
            (fun (x : α) => f₁ x - f₃ x) =o[l] g
            theorem Asymptotics.IsBigO.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =O[l] g) :
            f₁ =O[l] g f₂ =O[l] g
            theorem Asymptotics.IsLittleO.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =o[l] g) :
            f₁ =o[l] g f₂ =o[l] g

            Zero, one, and other constants #

            theorem Asymptotics.isLittleO_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] (g' : αF') (l : Filter α) :
            (fun (_x : α) => 0) =o[l] g'
            theorem Asymptotics.isBigOWith_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : } (g' : αF') (l : Filter α) (hc : 0 c) :
            Asymptotics.IsBigOWith c l (fun (_x : α) => 0) g'
            theorem Asymptotics.isBigOWith_zero' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] (g : αF) (l : Filter α) :
            Asymptotics.IsBigOWith 0 l (fun (_x : α) => 0) g
            theorem Asymptotics.isBigO_zero {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] (g : αF) (l : Filter α) :
            (fun (_x : α) => 0) =O[l] g
            theorem Asymptotics.isBigO_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} (g' : αF') (l : Filter α) :
            (fun (x : α) => f' x - f' x) =O[l] g'
            theorem Asymptotics.isLittleO_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : αE'} (g' : αF') (l : Filter α) :
            (fun (x : α) => f' x - f' x) =o[l] g'
            @[simp]
            theorem Asymptotics.isBigOWith_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {c : } {f'' : αE''} {l : Filter α} :
            (Asymptotics.IsBigOWith c l f'' fun (_x : α) => 0) f'' =ᶠ[l] 0
            @[simp]
            theorem Asymptotics.isBigO_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {f'' : αE''} {l : Filter α} :
            (f'' =O[l] fun (_x : α) => 0) f'' =ᶠ[l] 0
            @[simp]
            theorem Asymptotics.isLittleO_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {f'' : αE''} {l : Filter α} :
            (f'' =o[l] fun (_x : α) => 0) f'' =ᶠ[l] 0
            theorem Asymptotics.isBigOWith_const_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] (c : E) {c' : F''} (hc' : c' 0) (l : Filter α) :
            Asymptotics.IsBigOWith (c / c') l (fun (_x : α) => c) fun (_x : α) => c'
            theorem Asymptotics.isBigO_const_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] (c : E) {c' : F''} (hc' : c' 0) (l : Filter α) :
            (fun (_x : α) => c) =O[l] fun (_x : α) => c'
            @[simp]
            theorem Asymptotics.isBigO_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {c : E''} {c' : F''} (l : Filter α) [Filter.NeBot l] :
            ((fun (_x : α) => c) =O[l] fun (_x : α) => c') c' = 0c = 0
            @[simp]
            theorem Asymptotics.isBigO_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {g'' : αF''} {x : α} :
            f'' =O[pure x] g'' g'' x = 0f'' x = 0
            @[simp]
            theorem Asymptotics.isBigOWith_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {s : Set α} :
            theorem Asymptotics.isBigO_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {s : Set α} :
            f =O[Filter.principal s] g ∃ (c : ), xs, f x c * g x
            @[simp]
            theorem Asymptotics.isLittleO_principal {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : αF'} {f'' : αE''} {s : Set α} :
            f'' =o[Filter.principal s] g' xs, f'' x = 0
            @[simp]
            theorem Asymptotics.isBigOWith_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} :
            Asymptotics.IsBigOWith c f g ∀ (x : α), f x c * g x
            @[simp]
            theorem Asymptotics.isBigO_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} :
            f =O[] g ∃ (C : ), ∀ (x : α), f x C * g x
            @[simp]
            theorem Asymptotics.isLittleO_top {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : αF'} {f'' : αE''} :
            f'' =o[] g' ∀ (x : α), f'' x = 0
            theorem Asymptotics.isBigOWith_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] [One F] [NormOneClass F] (c : E) (l : Filter α) :
            Asymptotics.IsBigOWith c l (fun (_x : α) => c) fun (_x : α) => 1
            theorem Asymptotics.isBigO_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] [One F] [NormOneClass F] (c : E) (l : Filter α) :
            (fun (_x : α) => c) =O[l] fun (_x : α) => 1
            theorem Asymptotics.isLittleO_const_iff_isLittleO_one {α : Type u_1} {E : Type u_3} (F : Type u_4) {F'' : Type u_10} [Norm E] [Norm F] [NormedAddCommGroup F''] {f : αE} {l : Filter α} [One F] [NormOneClass F] {c : F''} (hc : c 0) :
            (f =o[l] fun (_x : α) => c) f =o[l] fun (_x : α) => 1
            @[simp]
            theorem Asymptotics.isLittleO_one_iff {α : Type u_1} (F : Type u_4) {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {f' : αE'} {l : Filter α} [One F] [NormOneClass F] :
            (f' =o[l] fun (_x : α) => 1) Filter.Tendsto f' l (nhds 0)
            @[simp]
            theorem Asymptotics.isBigO_one_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} {l : Filter α} [One F] [NormOneClass F] :
            (f =O[l] fun (_x : α) => 1) Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x
            theorem Filter.IsBoundedUnder.isBigO_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} {l : Filter α} [One F] [NormOneClass F] :
            (Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x)f =O[l] fun (_x : α) => 1

            Alias of the reverse direction of Asymptotics.isBigO_one_iff.

            @[simp]
            theorem Asymptotics.isLittleO_one_left_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} {l : Filter α} [One F] [NormOneClass F] :
            (fun (_x : α) => 1) =o[l] f Filter.Tendsto (fun (x : α) => f x) l Filter.atTop
            theorem Filter.Tendsto.isBigO_one {α : Type u_1} (F : Type u_4) {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {f' : αE'} {l : Filter α} [One F] [NormOneClass F] {c : E'} (h : Filter.Tendsto f' l (nhds c)) :
            f' =O[l] fun (_x : α) => 1
            theorem Asymptotics.IsBigO.trans_tendsto_nhds {α : Type u_1} {E : Type u_3} (F : Type u_4) {F' : Type u_7} [Norm E] [Norm F] [SeminormedAddCommGroup F'] {f : αE} {g' : αF'} {l : Filter α} [One F] [NormOneClass F] (hfg : f =O[l] g') {y : F'} (hg : Filter.Tendsto g' l (nhds y)) :
            f =O[l] fun (_x : α) => 1
            theorem Asymptotics.isLittleO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {l : Filter α} {c : F''} (hc : c 0) :
            (f'' =o[l] fun (_x : α) => c) Filter.Tendsto f'' l (nhds 0)
            theorem Asymptotics.isLittleO_id_const {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {c : F''} (hc : c 0) :
            (fun (x : E'') => x) =o[nhds 0] fun (_x : E'') => c
            theorem Filter.IsBoundedUnder.isBigO_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : αE} {l : Filter α} (h : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)) {c : F''} (hc : c 0) :
            f =O[l] fun (_x : α) => c
            theorem Asymptotics.isBigO_const_of_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {l : Filter α} {y : E''} (h : Filter.Tendsto f'' l (nhds y)) {c : F''} (hc : c 0) :
            f'' =O[l] fun (_x : α) => c
            theorem Asymptotics.IsBigO.isBoundedUnder_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {l : Filter α} {c : F} (h : f =O[l] fun (_x : α) => c) :
            Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)
            theorem Asymptotics.isBigO_const_of_ne {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : αE} {l : Filter α} {c : F''} (hc : c 0) :
            (f =O[l] fun (_x : α) => c) Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)
            theorem Asymptotics.isBigO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {l : Filter α} {c : F''} :
            (f'' =O[l] fun (_x : α) => c) (c = 0f'' =ᶠ[l] 0) Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f'' x
            theorem Asymptotics.isBigO_iff_isBoundedUnder_le_div {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : αE} {g'' : αF''} {l : Filter α} (h : ∀ᶠ (x : α) in l, g'' x 0) :
            f =O[l] g'' Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x / g'' x
            theorem Asymptotics.isBigO_const_left_iff_pos_le_norm {α : Type u_1} {E' : Type u_6} {E'' : Type u_9} [SeminormedAddCommGroup E'] [NormedAddCommGroup E''] {f' : αE'} {l : Filter α} {c : E''} (hc : c 0) :
            (fun (_x : α) => c) =O[l] f' ∃ (b : ), 0 < b ∀ᶠ (x : α) in l, b f' x

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

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

            Multiplication by a constant #

            theorem Asymptotics.isBigOWith_const_mul_self {α : Type u_1} {R : Type u_13} [SeminormedRing R] (c : R) (f : αR) (l : Filter α) :
            Asymptotics.IsBigOWith c l (fun (x : α) => c * f x) f
            theorem Asymptotics.isBigO_const_mul_self {α : Type u_1} {R : Type u_13} [SeminormedRing R] (c : R) (f : αR) (l : Filter α) :
            (fun (x : α) => c * f x) =O[l] f
            theorem Asymptotics.IsBigOWith.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {c : } {g : αF} {l : Filter α} {f : αR} (h : Asymptotics.IsBigOWith c l f g) (c' : R) :
            Asymptotics.IsBigOWith (c' * c) l (fun (x : α) => c' * f x) g
            theorem Asymptotics.IsBigO.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {g : αF} {l : Filter α} {f : αR} (h : f =O[l] g) (c' : R) :
            (fun (x : α) => c' * f x) =O[l] g
            theorem Asymptotics.isBigOWith_self_const_mul' {α : Type u_1} {R : Type u_13} [SeminormedRing R] (u : Rˣ) (f : αR) (l : Filter α) :
            Asymptotics.IsBigOWith u⁻¹ l f fun (x : α) => u * f x
            theorem Asymptotics.isBigOWith_self_const_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] (c : 𝕜) (hc : c 0) (f : α𝕜) (l : Filter α) :
            Asymptotics.IsBigOWith c⁻¹ l f fun (x : α) => c * f x
            theorem Asymptotics.isBigO_self_const_mul' {α : Type u_1} {R : Type u_13} [SeminormedRing R] {c : R} (hc : IsUnit c) (f : αR) (l : Filter α) :
            f =O[l] fun (x : α) => c * f x
            theorem Asymptotics.isBigO_self_const_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] (c : 𝕜) (hc : c 0) (f : α𝕜) (l : Filter α) :
            f =O[l] fun (x : α) => c * f x
            theorem Asymptotics.isBigO_const_mul_left_iff' {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {g : αF} {l : Filter α} {f : αR} {c : R} (hc : IsUnit c) :
            (fun (x : α) => c * f x) =O[l] g f =O[l] g
            theorem Asymptotics.isBigO_const_mul_left_iff {α : Type u_1} {F : Type u_4} {𝕜 : Type u_15} [Norm F] [NormedDivisionRing 𝕜] {g : αF} {l : Filter α} {f : α𝕜} {c : 𝕜} (hc : c 0) :
            (fun (x : α) => c * f x) =O[l] g f =O[l] g
            theorem Asymptotics.IsLittleO.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {g : αF} {l : Filter α} {f : αR} (h : f =o[l] g) (c : R) :
            (fun (x : α) => c * f x) =o[l] g
            theorem Asymptotics.isLittleO_const_mul_left_iff' {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {g : αF} {l : Filter α} {f : αR} {c : R} (hc : IsUnit c) :
            (fun (x : α) => c * f x) =o[l] g f =o[l] g
            theorem Asymptotics.isLittleO_const_mul_left_iff {α : Type u_1} {F : Type u_4} {𝕜 : Type u_15} [Norm F] [NormedDivisionRing 𝕜] {g : αF} {l : Filter α} {f : α𝕜} {c : 𝕜} (hc : c 0) :
            (fun (x : α) => c * f x) =o[l] g f =o[l] g
            theorem Asymptotics.IsBigOWith.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {c' : } {f : αE} {l : Filter α} {g : αR} {c : R} (hc' : 0 c') (h : Asymptotics.IsBigOWith c' l f fun (x : α) => c * g x) :
            theorem Asymptotics.IsBigO.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {c : R} (h : f =O[l] fun (x : α) => c * g x) :
            f =O[l] g
            theorem Asymptotics.IsBigOWith.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {u : Rˣ} {c' : } (hc' : 0 c') (h : Asymptotics.IsBigOWith c' l f g) :
            Asymptotics.IsBigOWith (c' * u⁻¹) l f fun (x : α) => u * g x
            theorem Asymptotics.IsBigOWith.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : αE} {l : Filter α} {g : α𝕜} {c : 𝕜} (hc : c 0) {c' : } (hc' : 0 c') (h : Asymptotics.IsBigOWith c' l f g) :
            Asymptotics.IsBigOWith (c' * c⁻¹) l f fun (x : α) => c * g x
            theorem Asymptotics.IsBigO.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {c : R} (hc : IsUnit c) (h : f =O[l] g) :
            f =O[l] fun (x : α) => c * g x
            theorem Asymptotics.IsBigO.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : αE} {l : Filter α} {g : α𝕜} {c : 𝕜} (hc : c 0) (h : f =O[l] g) :
            f =O[l] fun (x : α) => c * g x
            theorem Asymptotics.isBigO_const_mul_right_iff' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {c : R} (hc : IsUnit c) :
            (f =O[l] fun (x : α) => c * g x) f =O[l] g
            theorem Asymptotics.isBigO_const_mul_right_iff {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : αE} {l : Filter α} {g : α𝕜} {c : 𝕜} (hc : c 0) :
            (f =O[l] fun (x : α) => c * g x) f =O[l] g
            theorem Asymptotics.IsLittleO.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {c : R} (h : f =o[l] fun (x : α) => c * g x) :
            f =o[l] g
            theorem Asymptotics.IsLittleO.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {c : R} (hc : IsUnit c) (h : f =o[l] g) :
            f =o[l] fun (x : α) => c * g x
            theorem Asymptotics.IsLittleO.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : αE} {l : Filter α} {g : α𝕜} {c : 𝕜} (hc : c 0) (h : f =o[l] g) :
            f =o[l] fun (x : α) => c * g x
            theorem Asymptotics.isLittleO_const_mul_right_iff' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : αE} {l : Filter α} {g : αR} {c : R} (hc : IsUnit c) :
            (f =o[l] fun (x : α) => c * g x) f =o[l] g
            theorem Asymptotics.isLittleO_const_mul_right_iff {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : αE} {l : Filter α} {g : α𝕜} {c : 𝕜} (hc : c 0) :
            (f =o[l] fun (x : α) => c * g x) f =o[l] g

            Multiplication #

            theorem Asymptotics.IsBigOWith.mul {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : αR} {f₂ : αR} {g₁ : α𝕜} {g₂ : α𝕜} {c₁ : } {c₂ : } (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g₁) (h₂ : Asymptotics.IsBigOWith c₂ l f₂ g₂) :
            Asymptotics.IsBigOWith (c₁ * c₂) l (fun (x : α) => f₁ x * f₂ x) fun (x : α) => g₁ x * g₂ x
            theorem Asymptotics.IsBigO.mul {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : αR} {f₂ : αR} {g₁ : α𝕜} {g₂ : α𝕜} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
            (fun (x : α) => f₁ x * f₂ x) =O[l] fun (x : α) => g₁ x * g₂ x
            theorem Asymptotics.IsBigO.mul_isLittleO {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : αR} {f₂ : αR} {g₁ : α𝕜} {g₂ : α𝕜} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
            (fun (x : α) => f₁ x * f₂ x) =o[l] fun (x : α) => g₁ x * g₂ x
            theorem Asymptotics.IsLittleO.mul_isBigO {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : αR} {f₂ : αR} {g₁ : α𝕜} {g₂ : α𝕜} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =O[l] g₂) :
            (fun (x : α) => f₁ x * f₂ x) =o[l] fun (x : α) => g₁ x * g₂ x
            theorem Asymptotics.IsLittleO.mul {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : αR} {f₂ : αR} {g₁ : α𝕜} {g₂ : α𝕜} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
            (fun (x : α) => f₁ x * f₂ x) =o[l] fun (x : α) => g₁ x * g₂ x
            theorem Asymptotics.IsBigOWith.pow' {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {c : } {l : Filter α} {f : αR} {g : α𝕜} (h : Asymptotics.IsBigOWith c l f g) (n : ) :
            Asymptotics.IsBigOWith (Nat.casesOn n 1 fun (n : ) => c ^ (n + 1)) l (fun (x : α) => f x ^ n) fun (x : α) => g x ^ n
            theorem Asymptotics.IsBigOWith.pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {c : } {l : Filter α} [NormOneClass R] {f : αR} {g : α𝕜} (h : Asymptotics.IsBigOWith c l f g) (n : ) :
            Asymptotics.IsBigOWith (c ^ n) l (fun (x : α) => f x ^ n) fun (x : α) => g x ^ n
            theorem Asymptotics.IsBigOWith.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {c : } {c' : } {l : Filter α} {n : } {f : α𝕜} {g : αR} (h : Asymptotics.IsBigOWith c l (f ^ n) (g ^ n)) (hn : n 0) (hc : c c' ^ n) (hc' : 0 c') :
            theorem Asymptotics.IsBigO.pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : αR} {g : α𝕜} (h : f =O[l] g) (n : ) :
            (fun (x : α) => f x ^ n) =O[l] fun (x : α) => g x ^ n
            theorem Asymptotics.IsBigO.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α𝕜} {g : αR} {n : } (hn : n 0) (h : (f ^ n) =O[l] (g ^ n)) :
            f =O[l] g
            theorem Asymptotics.IsLittleO.pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : αR} {g : α𝕜} (h : f =o[l] g) {n : } (hn : 0 < n) :
            (fun (x : α) => f x ^ n) =o[l] fun (x : α) => g x ^ n
            theorem Asymptotics.IsLittleO.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α𝕜} {g : αR} {n : } (h : (f ^ n) =o[l] (g ^ n)) (hn : n 0) :
            f =o[l] g

            Inverse #

            theorem Asymptotics.IsBigOWith.inv_rev {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜'] {c : } {l : Filter α} {f : α𝕜} {g : α𝕜'} (h : Asymptotics.IsBigOWith c l f g) (h₀ : ∀ᶠ (x : α) in l, f x = 0g x = 0) :
            Asymptotics.IsBigOWith c l (fun (x : α) => (g x)⁻¹) fun (x : α) => (f x)⁻¹
            theorem Asymptotics.IsBigO.inv_rev {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜'] {l : Filter α} {f : α𝕜} {g : α𝕜'} (h : f =O[l] g) (h₀ : ∀ᶠ (x : α) in l, f x = 0g x = 0) :
            (fun (x : α) => (g x)⁻¹) =O[l] fun (x : α) => (f x)⁻¹
            theorem Asymptotics.IsLittleO.inv_rev {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜'] {l : Filter α} {f : α𝕜} {g : α𝕜'} (h : f =o[l] g) (h₀ : ∀ᶠ (x : α) in l, f x = 0g x = 0) :
            (fun (x : α) => (g x)⁻¹) =o[l] fun (x : α) => (f x)⁻¹

            Scalar multiplication #

            theorem Asymptotics.IsBigOWith.const_smul_self {α : Type u_1} {E' : Type u_6} {R : Type u_13} [SeminormedAddCommGroup E'] [SeminormedRing R] {f' : αE'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (c' : R) :
            Asymptotics.IsBigOWith c' l (fun (x : α) => c' f' x) f'
            theorem Asymptotics.IsBigO.const_smul_self {α : Type u_1} {E' : Type u_6} {R : Type u_13} [SeminormedAddCommGroup E'] [SeminormedRing R] {f' : αE'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (c' : R) :
            (fun (x : α) => c' f' x) =O[l] f'
            theorem Asymptotics.IsBigOWith.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {c : } {g : αF} {f' : αE'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : Asymptotics.IsBigOWith c l f' g) (c' : R) :
            Asymptotics.IsBigOWith (c' * c) l (fun (x : α) => c' f' x) g
            theorem Asymptotics.IsBigO.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {g : αF} {f' : αE'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : f' =O[l] g) (c : R) :
            (c f') =O[l] g
            theorem Asymptotics.IsLittleO.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {g : αF} {f' : αE'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : f' =o[l] g) (c : R) :
            (c f') =o[l] g
            theorem Asymptotics.isBigO_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [Norm F] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {g : αF} {f' : αE'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c 0) :
            (fun (x : α) => c f' x) =O[l] g f' =O[l] g
            theorem Asymptotics.isLittleO_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [Norm F] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {g : αF} {f' : αE'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c 0) :
            (fun (x : α) => c f' x) =o[l] g f' =o[l] g
            theorem Asymptotics.isBigO_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [Norm E] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {f : αE} {f' : αE'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c 0) :
            (f =O[l] fun (x : α) => c f' x) f =O[l] f'
            theorem Asymptotics.isLittleO_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [Norm E] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {f : αE} {f' : αE'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c 0) :
            (f =o[l] fun (x : α) => c f' x) f =o[l] f'
            theorem Asymptotics.IsBigOWith.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {c : } {c' : } {f' : αE'} {g' : αF'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : αR} {k₂ : α𝕜'} (h₁ : Asymptotics.IsBigOWith c l k₁ k₂) (h₂ : Asymptotics.IsBigOWith c' l f' g') :
            Asymptotics.IsBigOWith (c * c') l (fun (x : α) => k₁ x f' x) fun (x : α) => k₂ x g' x
            theorem Asymptotics.IsBigO.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : αE'} {g' : αF'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : αR} {k₂ : α𝕜'} (h₁ : k₁ =O[l] k₂) (h₂ : f' =O[l] g') :
            (fun (x : α) => k₁ x f' x) =O[l] fun (x : α) => k₂ x g' x
            theorem Asymptotics.IsBigO.smul_isLittleO {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : αE'} {g' : αF'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : αR} {k₂ : α𝕜'} (h₁ : k₁ =O[l] k₂) (h₂ : f' =o[l] g') :
            (fun (x : α) => k₁ x f' x) =o[l] fun (x : α) => k₂ x g' x
            theorem Asymptotics.IsLittleO.smul_isBigO {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : αE'} {g' : αF'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : αR} {k₂ : α𝕜'} (h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') :
            (fun (x : α) => k₁ x f' x) =o[l] fun (x : α) => k₂ x g' x
            theorem Asymptotics.IsLittleO.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : αE'} {g' : αF'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : αR} {k₂ : α𝕜'} (h₁ : k₁ =o[l] k₂) (h₂ : f' =o[l] g') :
            (fun (x : α) => k₁ x f' x) =o[l] fun (x : α) => k₂ x g' x

            Sum #

            theorem Asymptotics.IsBigOWith.sum {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {ι : Type u_17} {A : ιαE'} {C : ι} {s : Finset ι} (h : is, Asymptotics.IsBigOWith (C i) l (A i) g) :
            Asymptotics.IsBigOWith (Finset.sum s fun (i : ι) => C i) l (fun (x : α) => Finset.sum s fun (i : ι) => A i x) g
            theorem Asymptotics.IsBigO.sum {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : αF} {l : Filter α} {ι : Type u_17} {A : ιαE'} {s : Finset ι} (h : is, A i =O[l] g) :
            (fun (x : α) => Finset.sum s fun (i : ι) => A i x) =O[l] g
            theorem Asymptotics.IsLittleO.sum {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {g' : αF'} {l : Filter α} {ι : Type u_17} {A : ιαE'} {s : Finset ι} (h : is, A i =o[l] g') :
            (fun (x : α) => Finset.sum s fun (i : ι) => A i x) =o[l] g'

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

            theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α𝕜} {g : α𝕜} (h : f =o[l] g) :
            Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)
            theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero {α : Type u_1} {E' : Type u_6} {𝕜 : Type u_15} [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {f : αE'} {g : α𝕜} {l : Filter α} (h : f =o[l] g) :
            Filter.Tendsto (fun (x : α) => (g x)⁻¹ f x) l (nhds 0)
            theorem Asymptotics.isLittleO_iff_tendsto' {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α𝕜} {g : α𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0f x = 0) :
            f =o[l] g Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)
            theorem Asymptotics.isLittleO_iff_tendsto {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α𝕜} {g : α𝕜} (hgf : ∀ (x : α), g x = 0f x = 0) :
            f =o[l] g Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)
            theorem Asymptotics.isLittleO_of_tendsto' {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α𝕜} {g : α𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0f x = 0) :
            Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)f =o[l] g

            Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto'.

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

            Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto.

            theorem Asymptotics.isLittleO_const_left_of_ne {α : Type u_1} {F : Type u_4} {E'' : Type u_9} [Norm F] [NormedAddCommGroup E''] {g : αF} {l : Filter α} {c : E''} (hc : c 0) :
            (fun (_x : α) => c) =o[l] g Filter.Tendsto (fun (x : α) => g x) l Filter.atTop
            @[simp]
            theorem Asymptotics.isLittleO_const_left {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {g'' : αF''} {l : Filter α} {c : E''} :
            (fun (_x : α) => c) =o[l] g'' c = 0 Filter.Tendsto (norm g'') l Filter.atTop
            @[simp]
            theorem Asymptotics.isLittleO_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} [Filter.NeBot l] {d : E''} {c : F''} :
            ((fun (_x : α) => d) =o[l] fun (_x : α) => c) d = 0
            @[simp]
            theorem Asymptotics.isLittleO_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {g'' : αF''} {x : α} :
            f'' =o[pure x] g'' f'' x = 0
            theorem Asymptotics.isLittleO_const_id_cobounded {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] (c : F'') :
            (fun (x : E'') => c) =o[Bornology.cobounded E''] id
            theorem Asymptotics.isLittleO_const_id_atTop {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') :
            (fun (_x : ) => c) =o[Filter.atTop] id
            theorem Asymptotics.isLittleO_const_id_atBot {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') :
            (fun (_x : ) => c) =o[Filter.atBot] id

            Eventually (u / v) * v = u #

            If u and v are linked by an IsBigOWith relation, then we eventually have (u / v) * v = u, even if v vanishes.

            theorem Asymptotics.IsBigOWith.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : } {l : Filter α} {u : α𝕜} {v : α𝕜} (h : Asymptotics.IsBigOWith c l u v) :
            u / v * v =ᶠ[l] u
            theorem Asymptotics.IsBigO.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α𝕜} {v : α𝕜} (h : u =O[l] v) :
            u / v * v =ᶠ[l] u

            If u = O(v) along l, then (u / v) * v = u eventually at l.

            theorem Asymptotics.IsLittleO.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α𝕜} {v : α𝕜} (h : u =o[l] v) :
            u / v * v =ᶠ[l] u

            If u = o(v) along l, then (u / v) * v = u eventually at l.

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

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

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

            theorem Asymptotics.isBigOWith_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : } {l : Filter α} {u : α𝕜} {v : α𝕜} (hc : 0 c) :
            Asymptotics.IsBigOWith c l u v ∃ (φ : α𝕜), (∀ᶠ (x : α) in l, φ x c) u =ᶠ[l] φ * v
            theorem Asymptotics.IsBigOWith.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : } {l : Filter α} {u : α𝕜} {v : α𝕜} (h : Asymptotics.IsBigOWith c l u v) (hc : 0 c) :
            ∃ (φ : α𝕜), (∀ᶠ (x : α) in l, φ x c) u =ᶠ[l] φ * v
            theorem Asymptotics.isBigO_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α𝕜} {v : α𝕜} :
            u =O[l] v ∃ (φ : α𝕜), Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm φ) u =ᶠ[l] φ * v
            theorem Asymptotics.IsBigO.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α𝕜} {v : α𝕜} :
            u =O[l] v∃ (φ : α𝕜), Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm φ) u =ᶠ[l] φ * v

            Alias of the forward direction of Asymptotics.isBigO_iff_exists_eq_mul.

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

            Alias of the forward direction of Asymptotics.isLittleO_iff_exists_eq_mul.

            Miscellaneous lemmas #

            theorem Asymptotics.div_isBoundedUnder_of_isBigO {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f : α𝕜} {g : α𝕜} (h : f =O[l] g) :
            Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x / g x
            theorem Asymptotics.isBigO_iff_div_isBoundedUnder {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f : α𝕜} {g : α𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0f x = 0) :
            f =O[l] g Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x / g x
            theorem Asymptotics.isBigO_of_div_tendsto_nhds {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f : α𝕜} {g : α𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0f x = 0) (c : 𝕜) (H : Filter.Tendsto (f / g) l (nhds c)) :
            f =O[l] g
            theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto {α : Type u_17} {E : Type u_18} {𝕜 : Type u_19} [NormedAddCommGroup E] [NormedField 𝕜] {u : αE} {v : α𝕜} {l : Filter α} {y : 𝕜} (huv : u =o[l] v) (hv : Filter.Tendsto v l (nhds y)) :
            theorem Asymptotics.isLittleO_pow_pow {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {m : } {n : } (h : m < n) :
            (fun (x : 𝕜) => x ^ n) =o[nhds 0] fun (x : 𝕜) => x ^ m
            theorem Asymptotics.isLittleO_norm_pow_norm_pow {E' : Type u_6} [SeminormedAddCommGroup E'] {m : } {n : } (h : m < n) :
            (fun (x : E') => x ^ n) =o[nhds 0] fun (x : E') => x ^ m
            theorem Asymptotics.isLittleO_pow_id {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {n : } (h : 1 < n) :
            (fun (x : 𝕜) => x ^ n) =o[nhds 0] fun (x : 𝕜) => x
            theorem Asymptotics.isLittleO_norm_pow_id {E' : Type u_6} [SeminormedAddCommGroup E'] {n : } (h : 1 < n) :
            (fun (x : E') => x ^ n) =o[nhds 0] fun (x : E') => x
            theorem Asymptotics.IsBigO.eq_zero_of_norm_pow_within {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E''F''} {s : Set E''} {x₀ : E''} {n : } (h : f =O[nhdsWithin x₀ s] fun (x : E'') => x - x₀ ^ n) (hx₀ : x₀ s) (hn : n 0) :
            f x₀ = 0
            theorem Asymptotics.IsBigO.eq_zero_of_norm_pow {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E''F''} {x₀ : E''} {n : } (h : f =O[nhds x₀] fun (x : E'') => x - x₀ ^ n) (hn : n 0) :
            f x₀ = 0
            theorem Asymptotics.isLittleO_pow_sub_pow_sub {E' : Type u_6} [SeminormedAddCommGroup E'] (x₀ : E') {n : } {m : } (h : n < m) :
            (fun (x : E') => x - x₀ ^ m) =o[nhds x₀] fun (x : E') => x - x₀ ^ n
            theorem Asymptotics.isLittleO_pow_sub_sub {E' : Type u_6} [SeminormedAddCommGroup E'] (x₀ : E') {m : } (h : 1 < m) :
            (fun (x : E') => x - x₀ ^ m) =o[nhds x₀] fun (x : E') => x - x₀
            theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : } {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : Asymptotics.IsBigOWith c l f₁ f₂) (hc : c < 1) :
            Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₂ x - f₁ x
            @[deprecated Asymptotics.IsBigOWith.right_le_sub_of_lt_one]
            theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_1 {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : } {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : Asymptotics.IsBigOWith c l f₁ f₂) (hc : c < 1) :
            Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₂ x - f₁ x

            Alias of Asymptotics.IsBigOWith.right_le_sub_of_lt_one.

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

            Alias of Asymptotics.IsBigOWith.right_le_add_of_lt_one.

            theorem Asymptotics.IsLittleO.right_isBigO_sub {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : f₁ =o[l] f₂) :
            f₂ =O[l] fun (x : α) => f₂ x - f₁ x
            theorem Asymptotics.IsLittleO.right_isBigO_add {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : f₁ =o[l] f₂) :
            f₂ =O[l] fun (x : α) => f₁ x + f₂ x
            theorem Asymptotics.IsLittleO.right_isBigO_add' {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : αE'} {f₂ : αE'} (h : f₁ =o[l] f₂) :
            f₂ =O[l] (f₂ + f₁)
            theorem Asymptotics.bound_of_isBigO_cofinite {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : αE} {g'' : αF''} (h : f =O[Filter.cofinite] g'') :
            ∃ C > 0, ∀ ⦃x : α⦄, g'' x 0f x C * g'' x

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

            theorem Asymptotics.isBigO_cofinite_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : αE''} {g'' : αF''} (h : ∀ (x : α), g'' x = 0f'' x = 0) :
            f'' =O[Filter.cofinite] g'' ∃ (C : ), ∀ (x : α), f'' x C * g'' x
            theorem Asymptotics.bound_of_isBigO_nat_atTop {E : Type u_3} {E'' : Type u_9} [Norm E] [NormedAddCommGroup E''] {f : E} {g'' : E''} (h : f =O[Filter.atTop] g'') :
            ∃ C > 0, ∀ ⦃x : ⦄, g'' x 0f x C * g'' x
            theorem Asymptotics.isBigO_nat_atTop_iff {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E''} {g : F''} (h : ∀ (x : ), g x = 0f x = 0) :
            f =O[Filter.atTop] g ∃ (C : ), ∀ (x : ), f x C * g x
            theorem Asymptotics.isBigO_one_nat_atTop_iff {E'' : Type u_9} [NormedAddCommGroup E''] {f : E''} :
            (f =O[Filter.atTop] fun (_n : ) => 1) ∃ (C : ), ∀ (n : ), f n C
            theorem Asymptotics.isBigOWith_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : αF'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ιType u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α(i : ι) → E' i} {C : } (hC : 0 C) :
            Asymptotics.IsBigOWith C l f g' ∀ (i : ι), Asymptotics.IsBigOWith C l (fun (x : α) => f x i) g'
            @[simp]
            theorem Asymptotics.isBigO_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : αF'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ιType u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α(i : ι) → E' i} :
            f =O[l] g' ∀ (i : ι), (fun (x : α) => f x i) =O[l] g'
            @[simp]
            theorem Asymptotics.isLittleO_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : αF'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ιType u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α(i : ι) → E' i} :
            f =o[l] g' ∀ (i : ι), (fun (x : α) => f x i) =o[l] g'
            theorem Asymptotics.IsBigO.nat_cast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : RE} {g : RF} (h : f =O[Filter.atTop] g) :
            (fun (n : ) => f n) =O[Filter.atTop] fun (n : ) => g n
            theorem Asymptotics.IsLittleO.nat_cast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : RE} {g : RF} (h : f =o[Filter.atTop] g) :
            (fun (n : ) => f n) =o[Filter.atTop] fun (n : ) => g n
            theorem Asymptotics.isBigO_atTop_iff_eventually_exists {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {α : Type u_17} [SemilatticeSup α] [Nonempty α] {f : αE} {g : αF} :
            f =O[Filter.atTop] g ∀ᶠ (n₀ : α) in Filter.atTop, ∃ (c : ), nn₀, f n c * g n
            theorem Asymptotics.isBigO_atTop_iff_eventually_exists_pos {G : Type u_5} {G' : Type u_8} [Norm G] [SeminormedAddCommGroup G'] {α : Type u_17} [SemilatticeSup α] [Nonempty α] {f : αG} {g : αG'} :
            f =O[Filter.atTop] g ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c > 0, nn₀, c * f n g n
            theorem summable_of_isBigO {ι : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ιE} {g : ι} (hg : Summable g) (h : f =O[Filter.cofinite] g) :
            theorem summable_of_isBigO_nat {E : Type u_1} [SeminormedAddCommGroup E] [CompleteSpace E] {f : E} {g : } (hg : Summable g) (h : f =O[Filter.atTop] g) :
            theorem Asymptotics.IsBigO.comp_summable_norm {ι : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : EF} {g : ιE} (hf : f =O[nhds 0] id) (hg : Summable fun (x : ι) => g x) :
            Summable fun (x : ι) => f (g x)
            theorem PartialHomeomorph.isBigOWith_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b e.target) {f : βE} {g : βF} {C : } :

            Transfer IsBigOWith over a PartialHomeomorph.

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

            Transfer IsBigO over a PartialHomeomorph.

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

            Transfer IsLittleO over a PartialHomeomorph.

            theorem Homeomorph.isBigOWith_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : βE} {g : βF} {C : } :

            Transfer IsBigOWith over a Homeomorph.

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

            Transfer IsBigO over a Homeomorph.

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

            Transfer IsLittleO over a Homeomorph.