Asymptotics.IsEquivalent.isLittleO
theorem Asymptotics.IsEquivalent.isLittleO :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u v → (u - v) =o[l] v
The theorem `Asymptotics.IsEquivalent.isLittleO` states that for any types `α` and `β`, where `β` is a `NormedAddCommGroup`, if two functions `u` and `v` (both from `α` to `β`) are asymptotically equivalent along a filter `l`, then the difference between `u` and `v` is little-o of `v` along that filter. In other words, if `u` and `v` have the same asymptotic behaviour as `x` approaches along the filter `l` (i.e., `(u - v) = o(v)`), then `u - v` is an infinitesimally small quantity compared to `v` as `x` converges along `l`.
More concisely: If functions `u` and `v` are asymptotically equivalent to each other along filter `l` on types `α` and `β` (where `β` is a normed additive commutative group), then the difference `u - v` is little-o of `v` along `l`.
|
Asymptotics.IsEquivalent.tendsto_nhds
theorem Asymptotics.IsEquivalent.tendsto_nhds :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β},
Asymptotics.IsEquivalent l u v → Filter.Tendsto u l (nhds c) → Filter.Tendsto v l (nhds c)
The theorem `Asymptotics.IsEquivalent.tendsto_nhds` states that given any two functions `u` and `v` from a type `α` to a normed add commutative group `β` that are asymptotically equivalent along a filter `l` on `α`, and a value `c` in `β`, if the function `u` converges to `c` along `l` (in the sense that for every neighborhood of `c`, the preimage under `u` of that neighborhood is an `l`-neighborhood), then the function `v` also converges to `c` along `l`. In mathematical terms, if `u` and `v` are asymptotically equivalent and `u` tends to `c`, then `v` also tends to `c`.
More concisely: If functions `u` and `v` from type `α` to a normed add commutative group `β` are asymptotically equivalent along filter `l` on `α`, and `u` converges to a value `c` in `β` along `l`, then `v` also converges to `c` along `l`.
|
Asymptotics.IsEquivalent.trans
theorem Asymptotics.IsEquivalent.trans :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {u v w : α → β},
Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l v w → Asymptotics.IsEquivalent l u w
The theorem `Asymptotics.IsEquivalent.trans` states that for any type `α` and a normed add commutative group `β`, if two functions `u` and `v` are asymptotically equivalent along a filter `l`, and also `v` and `w` are asymptotically equivalent along the same filter `l`, then `u` and `w` are also asymptotically equivalent along the filter `l`. This property, known as transitivity, suggests that the asymptotic equivalence of functions along a filter behaves similarly to an equivalence relation.
More concisely: If `u`, `v`, and `w` are functions, and `α` is a type, and `β` is a normed add commutative group, and `l` is a filter, then if `u ≈_l v` and `v ≈_l w`, it follows that `u ≈_l w`.
|
Asymptotics.isEquivalent_const_iff_tendsto
theorem Asymptotics.isEquivalent_const_iff_tendsto :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α} {c : β},
c ≠ 0 → (Asymptotics.IsEquivalent l u (Function.const α c) ↔ Filter.Tendsto u l (nhds c))
The theorem `Asymptotics.isEquivalent_const_iff_tendsto` states that, for every type `α` and `β` where `β` is a normed additive commutative group, for every function `u` from `α` to `β`, for every filter `l` on `α`, and for every non-zero constant `c` of type `β`, the function `u` is asymptotically equivalent to the constant function with value `c` along the filter `l` if and only if the function `u` tends to `c` along the filter `l`. In other words, the difference between the function `u` and the constant function `c` becomes insignificant compared to `c` as we follow the filter `l` if and only if the function `u` approaches the constant value `c` when followed along the filter `l`.
More concisely: A function from a type to a normed additive commutative group is asymptotically equivalent to a constant function along a filter if and only if it tends to that constant along the filter.
|
Asymptotics.IsEquivalent.isBigO
theorem Asymptotics.IsEquivalent.isBigO :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u v → u =O[l] v
This theorem states that for any two functions `u` and `v` mapping from some type `α` to a normed add-commutative group `β`, and a filter `l` on `α`, if `u` and `v` are asymptotically equivalent along `l` (which means the difference between `u` and `v` is infinitesimal as `x` converges along `l`), then `u` is a big-O of `v` along `l`. In other words, `u` is bounded above by some constant multiple of `v` when `x` converges along `l`. This is a statement about the limiting behavior of functions when inputs approach specific values.
More concisely: If functions `u` and `v` from type `α` to a normed add-commutative group `β` are asymptotically equivalent along filter `l`, then `u` is a big-O of `v` along `l`, i.e., there exists a constant `C` such that `∀ x (x ∈ l → ||u x - v x|| ≤ C * ||v x||` where `||.||` denotes the norm.
|
Asymptotics.IsEquivalent.tendsto_atTop
theorem Asymptotics.IsEquivalent.tendsto_atTop :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedLinearOrderedField β] {u v : α → β} {l : Filter α}
[inst_1 : OrderTopology β],
Asymptotics.IsEquivalent l u v → Filter.Tendsto u l Filter.atTop → Filter.Tendsto v l Filter.atTop
The theorem `Asymptotics.IsEquivalent.tendsto_atTop` states that for any types `α` and `β`, where `β` is a normed linear ordered field with an order topology, and given any two functions `u` and `v` from `α` to `β`, and a filter `l` on `α`. If `u` and `v` are asymptotically equivalent along the filter `l`, and if `u` tends to positive infinity along `l`, then `v` also tends to positive infinity along `l`. In other words, if two functions are asymptotically equivalent and one of them tends towards infinity, then the other one also tends towards infinity.
More concisely: If two functions from a type to a normed linear ordered field with an order topology are asymptotically equivalent along a filter and one tends to positive infinity along the filter, then the other function also tends to positive infinity along the filter.
|
Asymptotics.IsEquivalent.add_isLittleO
theorem Asymptotics.IsEquivalent.add_isLittleO :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u v → w =o[l] v → Asymptotics.IsEquivalent l (u + w) v
The theorem `Asymptotics.IsEquivalent.add_isLittleO` states that for any types `α` and `β`, where `β` is a normed additive commutative group, and for any functions `u`, `v`, and `w` from `α` to `β`, and any filter `l` on `α`, if `u` and `v` are asymptotically equivalent along `l` and `w` is little-o of `v` along `l`, then the function `u` added to `w` is also asymptotically equivalent to `v` along `l`. In mathematical terms, if `u(x) - v(x) = o(v(x))` as `x` approaches along `l`, and `w(x) = o(v(x))` as `x` approaches along `l`, then `(u(x) + w(x)) - v(x) = o(v(x))` as `x` approaches along `l`.
More concisely: If `u`, `v`, and `w` are functions from a normed additive commutative group `α` to another normed additive commutative group `β`, and `u` is asymptotically equivalent to `v` along a filter `l` on `α` with `w = o(v)` along `l`, then `u + w` is asymptotically equivalent to `v` along `l`.
|
Asymptotics.IsEquivalent.refl
theorem Asymptotics.IsEquivalent.refl :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u u
The theorem `Asymptotics.IsEquivalent.refl` states that for any type `α`, another type `β` which forms a normed add commutative group, a function `u` from `α` to `β`, and a filter `l` on `α`, the function `u` is asymptotically equivalent to itself along the filter `l`. In the mathematical language, as `x` tends to the limit along the filter `l`, the difference between `u(x)` and `u(x)` (which is `0`) is infinitely smaller than `u(x)`, which holds for all functions and filters.
More concisely: For any type `α`, normed add commutative group `β`, function `u` from `α` to `β`, and filter `l` on `α`, `u` is asymptotically equivalent to itself along `l`, i.e., for all `ε > 0`, there exists `N` such that for all `x` in `α` with `l.contains x`, the norm of `u(x) - u(x)` is less than `ε` times the norm of `u(x)`.
|
Filter.EventuallyEq.isEquivalent
theorem Filter.EventuallyEq.isEquivalent :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {u v : α → β},
l.EventuallyEq u v → Asymptotics.IsEquivalent l u v
This theorem states that for any type `α`, any normed additive commutative group `β`, any filter `l` on `α`, and any two functions `u` and `v` from `α` to `β`, if `u` and `v` are eventually equal along `l` (meaning that there exists a neighborhood within `l` where `u` and `v` are equal), then `u` and `v` are asymptotically equivalent along `l`. In mathematical terms, if $u(x) = v(x)$ eventually as `x` converges along `l`, then $u(x) - v(x) = o(v(x))$ as `x` converges along `l`.
More concisely: If two functions from a type `α` to a normed additive commutative group `β` are eventually equal along a filter `l`, then their difference is asymptotically equivalent to zero along `l`.
|
Asymptotics.IsEquivalent.isTheta
theorem Asymptotics.IsEquivalent.isTheta :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u v → u =Θ[l] v
This theorem states that for any given types `α` and `β`, where `β` is a normed add commutative group, and any given functions `u` and `v` from `α` to `β`, along with a filter `l` on `α`, if `u` and `v` are asymptotically equivalent along `l` (i.e., the difference between `u` and `v` is little-o of `v` as `x` converges along `l`), then `u` is Theta of `v` along `l`, denoted as `u =Θ[l] v`. In terms of Big O notation, this implies that `u` and `v` have the same order of growth along the filter `l`.
More concisely: If functions `u` and `v` from type `α` to a normed add commutative group `β` are asymptotically equivalent along filter `l` (little-o of `v` as `x` converges along `l`), then `u` is Theta of `v` along `l` (same order of growth).
|
Asymptotics.IsEquivalent.symm
theorem Asymptotics.IsEquivalent.symm :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l v u
The theorem `Asymptotics.IsEquivalent.symm` states that for any two functions `u` and `v` over a normed additive commutative group `β` and a filter `l` in `α`, if `u` and `v` are asymptotically equivalent along `l` (in the sense that the difference between `u x` and `v x` is infinitesimal compared to `v x` as `x` approaches `l`), then `v` and `u` are also asymptotically equivalent along `l`. In other words, the relationship of asymptotic equivalence between two functions along a filter is symmetric.
More concisely: If functions `u` and `v` are asymptotically equivalent along filter `l` in a normed additive commutative group `β`, then `v` and `u` are also asymptotically equivalent along `l`.
|
Asymptotics.IsEquivalent.isBigO_symm
theorem Asymptotics.IsEquivalent.isBigO_symm :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
Asymptotics.IsEquivalent l u v → v =O[l] u
The theorem `Asymptotics.IsEquivalent.isBigO_symm` states that for any types `α` and `β`, with `β` being a normed addition commutative group, and for any functions `u` and `v` from `α` to `β` and a filter `l` on `α`, if `u` and `v` are asymptotically equivalent along `l`, then `v` is a big O of `u` along `l`. In mathematical terms, if `u(x) - v(x) = o(v(x))` as `x` approaches `l`, then `v(x) = O(u(x))` as `x` approaches `l`.
More concisely: If functions `u` and `v` from type `α` to a normed additive commutative group `β` are asymptotically equivalent along filter `l` on `α`, then `v` is a big O of `u` along `l`.
|
Asymptotics.IsEquivalent.mul
theorem Asymptotics.IsEquivalent.mul :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] {t u v w : α → β} {l : Filter α},
Asymptotics.IsEquivalent l t u → Asymptotics.IsEquivalent l v w → Asymptotics.IsEquivalent l (t * v) (u * w)
The theorem `Asymptotics.IsEquivalent.mul` states that for any type `α` and any normed field `β`, given any four functions `t`, `u`, `v`, and `w` from `α` to `β` and a filter `l` on `α`, if the function `t` is asymptotically equivalent to the function `u` along the filter `l` and the function `v` is asymptotically equivalent to the function `w` along the filter `l`, then the product of the functions `t` and `v` is asymptotically equivalent to the product of the functions `u` and `w` along the filter `l`. Here, asymptotic equivalence of two functions `f` and `g` along a filter `l` means that `f(x) - g(x) = o(g(x))` as `x` converges along `l`.
More concisely: If functions `t`, `u`, `v`, `w` from type `α` to normed field `β` are asymptotically equivalent along filter `l` with `t ~ o u` and `v ~ o w`, then their product `tv` is asymptotically equivalent to the product `uw` along filter `l`, i.e., `tv ~ o uw`.
|