Asymptotics.IsLittleO.bound
theorem Asymptotics.IsLittleO.bound :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
This theorem, `Asymptotics.IsLittleO.bound`, establishes the forward direction of the `IsLittleO` definition in terms of filters. Specifically, for all types `α`, `E`, `F` and functions `f: α → E`, `g: α → F` with a filter `l` on `α`, if `f` is little o of `g` at filter `l`, then for any real number `c` greater than 0, all elements `x` in `l` eventually satisfy the inequality `‖f x‖ ≤ c * ‖g x‖`. Here, `‖_‖` represents the norm on types `E` and `F`.
More concisely: For all types `α`, `E`, `F`, functions `f: α → E`, `g: α → F`, and filters `l` on `α`, if `f` is little o of `g` at filter `l`, then for any positive real number `c`, all elements `x` in `l` eventually satisfy `‖f x‖ ≤ c * ‖g x‖`, where `‖_‖` denotes the norm on `E` and `F`.
|
Asymptotics.IsBigOWith_def
theorem Asymptotics.IsBigOWith_def :
∀ {α : Type u_17} {E : Type u_18} {F : Type u_19} [inst : Norm E] [inst_1 : Norm F] (c : ℝ) (l : Filter α)
(f : α → E) (g : α → F), Asymptotics.IsBigOWith c l f g = ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
The theorem `Asymptotics.IsBigOWith_def` states that for any real number `c`, any filter `l` over a type `α`, and any two functions `f` and `g` mapping from `α` to normed types `E` and `F` respectively, the property of `f` being Big O of `g` with respect to `c` and `l` (denoted as `Asymptotics.IsBigOWith c l f g`) is equivalent to the statement that, eventually for every element `x` in the filter `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`. In other words, the value of `f` is eventually bounded above by `c` times the value of `g` for all inputs in the filter `l`.
More concisely: For any real number `c`, filter `l`, functions `f` and `g` mapping from `α` to normed types `E` and `F` respectively, `Asymptotics.IsBigOWith c l f g` if and only if for all `x` in `l`, `||f(x)|| ≤ c * ||g(x)||`.
|
Asymptotics.isLittleO_norm_left
theorem Asymptotics.isLittleO_norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g
This theorem, `Asymptotics.isLittleO_norm_left`, states that for any types `α`, `F`, and `E'`, where `F` has a norm structure and `E'` has a semi-normed additive commutative group structure, and for any functions `g : α → F` and `f' : α → E'`, as well as for any filter `l` on `α`, the norm of `f'` is little-o of `g` with respect to `l` if and only if `f'` itself is little-o of `g` with respect to `l`. Here, being "little-o" is a mathematical notation used to describe limiting behavior, meaning that the growth rate of `f'` is asymptotically less than the growth rate of `g` as they approach the limit `l`.
More concisely: For functions `g : α → F` and `f' : α → E'` on types `α` with filter `l`, where `F` has a norm structure and `E'` is a semi-normed additive commutative group, `f'` is little-o of `g` with respect to `l` in norm if and only if `f'` is little-o of `g` with respect to `l` in `E'`.
|
Asymptotics.IsLittleO.comp_tendsto
theorem Asymptotics.IsLittleO.comp_tendsto :
∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E}
{g : α → F} {l : Filter α},
f =o[l] g → ∀ {k : β → α} {l' : Filter β}, Filter.Tendsto k l' l → (f ∘ k) =o[l'] (g ∘ k)
The theorem `Asymptotics.IsLittleO.comp_tendsto` states that for all types `α`, `β`, `E`, and `F` (with `E` and `F` both having a norm), given a function `f` from `α` to `E`, a function `g` from `α` to `F`, and a filter `l` on `α`, if `f` is little-o of `g` at filter `l`, then for any function `k` from `β` to `α` and any filter `l'` on `β`, if `k` tends to `l` with respect to `l'`, then the composition of `f` and `k` is also little-o of the composition of `g` and `k` at filter `l'`.
In mathematical terms, if $f(x)$ is little-o of $g(x)$ as $x$ approaches a filter $l$ and if a function $k(x)$ tends to filter $l$ as $x$ approaches a filter $l'$, then $f(k(x))$ is little-o of $g(k(x))$ as $x$ approaches the filter $l'$.
More concisely: If a function $f(x)$ is little-o of $g(x)$ as $x$ approaches filter $l$, and a function $k(x)$ tends to filter $l$ as $x$ approaches filter $l'$, then $f(k(x))$ is little-o of $g(k(x))$ as $x$ approaches filter $l'$.
|
Asymptotics.IsLittleO.add
theorem Asymptotics.IsLittleO.add :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{l : Filter α} {f₁ f₂ : α → E'}, f₁ =o[l] g → f₂ =o[l] g → (fun x => f₁ x + f₂ x) =o[l] g
The theorem `Asymptotics.IsLittleO.add` states that for any types `α`, `F`, and `E'`, where `F` is a normed space and `E'` is a seminormed additive commutative group, and for any functions `f₁`, `f₂`, `g` from `α` to `F` and a filter `l` on `α`, if `f₁` and `f₂` are both little-o of `g` at `l`, then their sum function `(fun x => f₁ x + f₂ x)` is also little-o of `g` at `l`. In other words, the little-o notation and the sum of functions obey a distributive law in Asymptotic analysis.
More concisely: If `f₁` and `f₂` are little-o of `g` at filter `l` in the normed space `F` over the seminormed additive commutative group `E'`, then their sum `(fun x => f₁ x + f₂ x)` is also little-o of `g` at filter `l`.
|
Asymptotics.IsBigO.trans_isLittleO
theorem Asymptotics.IsBigO.trans_isLittleO :
∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
[inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
f =O[l] g → g =o[l] k → f =o[l] k
This theorem, `Asymptotics.IsBigO.trans_isLittleO`, states that for any types `α`, `E`, `G`, and `F'`, where `E`, `G`, and `F'` have a norm (i.e., they are normed spaces), and `F'` is a seminormed additive commutative group, and given a filter `l` and functions `f`, `g`, and `k` from `α` to `E`, `F'`, and `G` respectively, if `f` is Big-O of `g` (the function `f` is asymptotically no more than `g` times a constant, as we approach a limit along filter `l`), and `g` is little-o of `k` (the function `g` becomes insignificant compared to `k` along filter `l`), then `f` is also little-o of `k` (the function `f` becomes insignificant compared to `k` along filter `l`). In effect, it is a transitivity rule for Big-O and little-o asymptotic notations.
More concisely: If `f` is Big-O of `g` and `g` is little-o of `k` along a filter `l`, then `f` is little-o of `k` along `l`. (Transitivity rule for Big-O and little-o asymptotic notations in the context of normed spaces and seminormed additive commutative groups.)
|
Homeomorph.isLittleO_congr
theorem Homeomorph.isLittleO_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
[inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F},
f =o[nhds b] g ↔ (f ∘ ⇑e) =o[nhds (e.symm b)] (g ∘ ⇑e)
The theorem `Homeomorph.isLittleO_congr` states that for any two types `α` and `β` equipped with topological spaces, along with two other types `E` and `F` equipped with norms, if there is a homeomorphism `e` from `α` to `β`, a point `b` in `β`, and two functions `f` and `g` from `β` to `E` and `F` respectively, then `f` is little-o of `g` at the neighborhood of `b` if and only if the composition of `f` and `g` with the application of `e` is little-o of the composition of `f` and `g` with the application of `e` at the neighborhood of the inverse image of `b` under `e`. In simpler terms, the little-o order of functions is preserved under a homeomorphism.
More concisely: For types `α`, `β` with topological spaces, `E` and `F` with norms, and a homeomorphism `e: α ↔ β` between them, if `f: β → E` and `g: β → F` are such that `f` is little-o of `g` at a neighborhood of `b ∈ β`, then `(f ∘ e)` is little-o of `(g ∘ e)` at the neighborhood of `e⁻¹(b) ∈ α`.
|
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|
This theorem, **Asymptotics.IsLittleO.abs_abs**, is an alias of the reverse direction of `Asymptotics.isLittleO_abs_abs`. It states that for any type `α` and any filter `l` on `α`, if a function `u` is "little-o" of function `v` at filter `l` (i.e., `u =o[l] v`), then the absolute value function applied to `u` is also "little-o" of the absolute value function applied to `v` at the same filter (i.e., `|u(x)| =o[l] |v(x)|`). In other words, if `u` grows asymptotically slower than `v`, then the absolute value of `u` also grows asymptotically slower than the absolute value of `v`.
More concisely: If `u =o[l] v`, then `|u(x)| =o[l] |v(x)|` for any filter `l` and types `α` where the absolute value function is defined.
|
Asymptotics.IsLittleO.abs_left
theorem Asymptotics.IsLittleO.abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
u =o[l] g → (fun x => |u x|) =o[l] g
This is an alias of the reverse direction of `Asymptotics.isLittleO_abs_left` theorem in Asymptotics. For any types `α` and `F`, where `F` is a type with a norm, given a function `g` from `α` to `F`, a filter `l` on `α`, and another function `u` from `α` to real numbers `ℝ`, if `u` is little-o of `g` at filter `l` (denoted by `u =o[l] g`), then the absolute value of `u` (denoted by `fun x => |u x|`) is also little-o of `g` at the same filter `l`. In other words, if a function is dominated by another at a certain level of precision (up to a constant factor), taking absolute values doesn't change this dominance relationship.
More concisely: If `u =o[l] g` for functions `g : α -> F` and `u : α -> ℝ` with `F` having a norm, then `|u| =o[l] |g|`. (In other words, taking absolute values preserves little-o dominance at filter `l`.)
|
Asymptotics.IsBigO.of_norm_left
theorem Asymptotics.IsBigO.of_norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =O[l] g → f' =O[l] g
This theorem, named `Asymptotics.IsBigO.of_norm_left`, is an alias of the forward direction of `Asymptotics.isBigO_norm_left`. It states that for any types `α`, `F`, `E'` and any functions `g : α → F` and `f' : α → E'`, under a given filter `l`, if the norm of `f'` is asymptotically bounded by `g` (i.e., `(fun x => ‖f' x‖) =O[l] g`), then `f'` itself is also asymptotically bounded by `g` (i.e., `f' =O[l] g`). Here, the norm and the seminormed add commutative group structures are assumed for `F` and `E'` respectively.
More concisely: If the norm of a function `f'` is asymptotically bounded by another function `g`, then `f'` is also asymptotically bounded by `g` (for commutative normed additive groups `F` and `E'`).
|
Asymptotics.IsLittleO.of_abs_right
theorem Asymptotics.IsLittleO.of_abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
(f =o[l] fun x => |u x|) → f =o[l] u
This theorem, `Asymptotics.IsLittleO.of_abs_right`, is an alias for the forward direction of `Asymptotics.isLittleO_abs_right`. It states that for any types `α` and `E`, where `E` has a norm, and any functions `f : α → E` and `u : α → ℝ` with a certain filter `l` on `α`, if `f` is little-o of the absolute value of `u` at `l`, then `f` is also little-o of `u` at `l`. In other words, if the function `f` grows no faster than the absolute value of `u` as we approach the limit `l`, then `f` also grows no faster than `u` itself.
More concisely: If `f : α → E` is little-o of the absolute value of `u : α → ℝ` as `α` approaches a limit `l`, then `f` is little-o of `u` at `l`.
|
Asymptotics.isBigOWith_iff
theorem Asymptotics.isBigOWith_iff :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
{l : Filter α}, Asymptotics.IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
The theorem `Asymptotics.isBigOWith_iff` expresses equivalence between two descriptions of big O notation with a constant. For any real number `c`, functions `f` and `g` from a type `α` to types `E` and `F` equipped with norms, and a filter `l` on `α`, the statement that `f` is big O of `g` with constant `c` with respect to `l` (denoted `Asymptotics.IsBigOWith c l f g`) is equivalent to the statement that, eventually for `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`. In other words, for all `x` in the neighborhood defined by the filter `l`, `‖f x‖` is bounded by `c * ‖g x‖`.
More concisely: For functions `f` and `g` from a type `α` to types `E` and `F` equipped with norms, and a filter `l` on `α`, the functions `f` is big O of `g` with constant `c` with respect to `l` if and only if for all `x` in the neighborhood defined by `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`.
|
Asymptotics.IsBigOWith.eventually_mul_div_cancel
theorem Asymptotics.IsBigOWith.eventually_mul_div_cancel :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u v : α → 𝕜},
Asymptotics.IsBigOWith c l u v → l.EventuallyEq (u / v * v) u
This theorem, named `Asymptotics.IsBigOWith.eventually_mul_div_cancel`, states that for any type `α` and `𝕜` (where `𝕜` is a normed division ring), a real number `c`, a filter `l` on `α`, and functions `u` and `v` from `α` to `𝕜`, if it is the case that the function `u` is Big-O of the function `v` with constant `c` at the filter `l` (denoted `Asymptotics.IsBigOWith c l u v`), then eventually (with respect to the filter `l`), the product of `u / v` and `v` equals `u`. In other words, if the magnitude of `u` is eventually bounded by a constant multiple of the magnitude of `v`, then multiplying the ratio of `u` to `v` by `v` will eventually yield `u` itself.
More concisely: If `u` is Big-O of `v` with constant `c` at filter `l`, then eventually `u / v * v = u` at points in `l`.
|
Asymptotics.IsBigO.mul
theorem Asymptotics.IsBigO.mul :
∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
{l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜},
f₁ =O[l] g₁ → f₂ =O[l] g₂ → (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x
This theorem, named `Asymptotics.IsBigO.mul`, states that for any type `α`, `R`, and `𝕜`, where `R` is a seminormed ring and `𝕜` is a normed division ring, and for any filter `l`, if function `f₁` is `O(g₁)` and function `f₂` is `O(g₂)` at l, then the function that multiplies `f₁` and `f₂` is `O` of the function that multiplies `g₁` and `g₂` at l. This is a statement about asymptotic behaviour, saying that if two functions each grow no faster than two other functions, then the same is true for their product.
More concisely: If functions `f₁` and `f₂` are big O of `g₁` and `g₂`, respectively, at filter `l`, then their product `f₁ * f₂` is big O of `g₁ * g₂` at `l`.
|
Asymptotics.isLittleO_pow_pow
theorem Asymptotics.isLittleO_pow_pow :
∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {m n : ℕ}, m < n → (fun x => x ^ n) =o[nhds 0] fun x => x ^ m := by
sorry
The theorem `Asymptotics.isLittleO_pow_pow` states that for any normed division ring `𝕜` and for any two natural numbers `m` and `n` such that `m` is less than `n`, the function `fun x => x ^ n` is little-o of the function `fun x => x ^ m` at a neighbourhood of 0. In other words, as `x` approaches 0, the growth rate of the function `x ^ n` is significantly smaller than that of the function `x ^ m`.
More concisely: For any normed division ring 𝕜 and natural numbers m < n, the function x => x^n is little-o of the function x => x^m as x approaches 0.
|
Homeomorph.isBigOWith_congr
theorem Homeomorph.isBigOWith_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
[inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ},
Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
The theorem `Homeomorph.isBigOWith_congr` states that for a homeomorphism `e` between two topological spaces `α` and `β`, and two real-valued functions `f` and `g` defined on `β`, the function `f` is Big-O of `g` in the neighborhood of a point `b` in `β` if and only if the function `f` composed with `e` is Big-O of `g` composed with `e` in the neighborhood of the image of `b` under the inverse of `e` in `α`. In other words, the Big-O relation between `f` and `g` is preserved under the homeomorphism `e`.
More concisely: For a homeomorphism between topological spaces and real-valued functions on one space, the Big-O relation between the functions is preserved under composition with the homeomorphism.
|
Asymptotics.IsBigO_def
theorem Asymptotics.IsBigO_def :
∀ {α : Type u_17} {E : Type u_18} {F : Type u_19} [inst : Norm E] [inst_1 : Norm F] (l : Filter α) (f : α → E)
(g : α → F), f =O[l] g = ∃ c, Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.IsBigO_def` states that for any types `α`, `E`, and `F`, with `E` and `F` having a norm, any filter `l` on `α`, and any two functions `f` and `g` from `α` to `E` and `F` respectively, we have that `f` is Big O of `g` with respect to the filter `l` if and only if there exists a real number `c` such that `f` is eventually bounded by `c * ‖g‖` for the filter `l`. In the mathematical notation, this translates to \(f = O(g)\) if and only if ∃c, `f` is \(O(c \cdot g)\) where the Big O notation denotes that `f` is asymptotically bounded by `g` times a constant factor.
More concisely: For any types `α`, `E` with `E` having a norm, and functions `f : α -> E` and `g : α -> E` with `g` having a norm, `f` is Big O of `g` with respect to a filter `l` on `α` if and only if there exists a constant `c` such that the absolute values of `f` are eventually bounded by `c` times the norm of `g` for the filter `l`.
|
Asymptotics.IsLittleO.of_norm_right
theorem Asymptotics.IsLittleO.of_norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =o[l] fun x => ‖g' x‖) → f =o[l] g'
This theorem is an alias of the forward direction of `Asymptotics.isLittleO_norm_right` in asymptotic analysis. It says that for any types `α`, `E`, and `F'`, where `E` has a `Norm` and `F'` is a `SeminormedAddCommGroup`, and for any functions `f : α → E` and `g' : α → F'` and any filter `l` on `α`, if `f` is little-o of the norm of `g'` at `l` (meaning that `f` grows no faster than the norm of `g'` as we approach the limit `l`), then `f` is also little-o of `g'` at `l`.
More concisely: If `f : α → E` is little-o of the norm of `g' : α → F'` at a filter `l` on `α`, then `f` is also little-o of `g'` at `l`.
|
Asymptotics.isBigO_const_left_iff_pos_le_norm
theorem Asymptotics.isBigO_const_left_iff_pos_le_norm :
∀ {α : Type u_1} {E' : Type u_6} {E'' : Type u_9} [inst : SeminormedAddCommGroup E']
[inst_1 : NormedAddCommGroup E''] {f' : α → E'} {l : Filter α} {c : E''},
c ≠ 0 → ((fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖)
This theorem states that for any non-zero constant `c` of type `E''` and any function `f'` from `α` to `E'` in a seminormed add commutative group, `(fun x ↦ c) =O[l] f'` (which means that the function returning `c` is Big O of `f'` at filter `l`) if and only if `f'` is bounded away from zero. In other words, there exists a positive `b` such that, eventually for all `x` in the filter `l`, `b` is less than or equal to the norm of `f'(x)`.
More concisely: For a non-zero constant `c` and a function `f` from a set `α` to a normed add commutative group `E`, `(λx, c) = O[l] f` if and only if there exists a positive `b` such that for all `x` in the filter `l`, the norm of `f(x)` is greater than or equal to `b`.
|
Asymptotics.IsBigO.exists_nonneg
theorem Asymptotics.IsBigO.exists_nonneg :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =O[l] g' → ∃ c ≥ 0, Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.IsBigO.exists_nonneg` states that for any types `α`, `E`, and `F'`, given `f` and `g'` as functions from `α` to `E` and `F'` respectively, and a filter `l` on `α`, if `f` is Big O of `g'` with respect to `l` (denoted as `f =O[l] g'`), then there exists a nonnegative real number `c` such that `f` is Big O of `g'` with constant `c` and filter `l`. In other words, `f` is eventually bounded by `c * ‖g'‖` for some nonnegative `c`.
More concisely: For any types `α`, `E`, and `F'`, given functions `f : α → E` and `g' : α → F'`, and a filter `l` on `α`, if `f` is Big O of `g'` with respect to `l`, then there exists a constant `c ≥ 0` such that `|f(x)| ≤ c * |g'(x)|` for all `x` in the filter `l`.
|
PartialHomeomorph.isBigO_congr
theorem PartialHomeomorph.isBigO_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
[inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : PartialHomeomorph α β) {b : β},
b ∈ e.target → ∀ {f : β → E} {g : β → F}, f =O[nhds b] g ↔ (f ∘ ↑e) =O[nhds (↑e.symm b)] (g ∘ ↑e)
This theorem states that for any types `α`, `β`, `E`, `F` where `α` and `β` have a topological structure and `E`, `F` have a norm, and given a partial homeomorphism `e` from `α` to `β`, and a point `b` from `β` that is in the target of `e`, for any two functions `f` and `g` from `β` to `E` and `F` respectively, the function `f` is Big O of `g` with respect to the neighborhood filter at `b` if and only if the composition of `f` and `e` is Big O of the composition of `g` and `e` with respect to the neighborhood filter at the inverse image of `b` under `e`.
In other words, the concept of Big O notation (which measures how quickly one function grows relative to another as the input approaches a particular value) is preserved under a partial homeomorphism. This is a kind of "change of coordinates" result for Big O notation in the context of topological spaces and functions with a norm.
More concisely: For any partial homeomorphism between topological spaces with normed functions, the Big O relation between two functions is preserved under composition if and only if the partial homeomorphism maps the domains of the functions appropriately.
|
Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.20
theorem Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.20 :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =O[l] fun x => ‖g' x‖) = f =O[l] g'
This theorem states that, for every types `α`, `E`, and `F'`, with `E` as a normed space and `F'` as a seminormed additive commutative group, and for every functions `f` from `α` to `E` and `g'` from `α` to `F'`, and a filter `l` on `α`, the function `f` is of the same order (big O notation) as the function that maps `x` to the norm of `g' x` under filter `l` if and only if `f` is of the same order as `g'` under filter `l`. In mathematical terms, $f=O(g'(x))$ if and only if $f=O(‖g'(x)‖)$, where $O$ is the big O notation used in Asymptotic analysis.
More concisely: For functions $f : \alpha \to E$ and $g' : \alpha \to F'$ between a type, a normed space, and a seminormed additive commutative group respectively, with $E$ being normed, the functions $f$ and $g'$ are of the same order under filter $l$ if and only if $f$ is of the same order as the norm of $g'$ under filter $l$. In symbols, $f = O(g'(x))$ if and only if $f = O(\|\,g'(x)\,\|)$.
|
Filter.EventuallyEq.trans_isBigO
theorem Filter.EventuallyEq.trans_isBigO :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
{g : α → F}, l.EventuallyEq f₁ f₂ → f₂ =O[l] g → f₁ =O[l] g
This theorem states that for any types `α`, `E`, and `F` where `E` and `F` are normed, given a filter `l` on `α`, and functions `f₁`, `f₂` from `α` to `E`, and `g` from `α` to `F`, if `f₁` is eventually equal to `f₂` at `l`, and `f₂` is Big O of `g` at `l`, then `f₁` is also Big O of `g` at `l`.
In mathematical terms, it says that if $f₁(x) = f₂(x)$ for all $x$ sufficiently close to a point in a filter `l` and $f₂(x) = O(g(x))$ (meaning $f₂(x)$ grows no faster than `g` in terms of `l`), then $f₁(x) = O(g(x))$ as well.
More concisely: If `f₁` equals `f₂` in a filter `l` where `f₂` is Big O of `g` at `l` for normed types `α`, `E`, and `F`, then `f₁` is also Big O of `g` at `l`.
|
Asymptotics.IsBigO.neg_right
theorem Asymptotics.IsBigO.neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =O[l] g' → f =O[l] fun x => -g' x
This theorem, named `Asymptotics.IsBigO.neg_right`, is an alias of the reverse direction of `Asymptotics.isBigO_neg_right`. It states that for any types `α`, `E`, and `F'` where `E` is a normed space and `F'` is a semi-normed add commutative group, and for any functions `f` and `g'` from `α` to `E` and `F'` respectively, and for any filter `l` on `α`, if `f` is Big O of `g'` at `l` (denoted as `f =O[l] g'`), then `f` is also Big O of `-g'` at `l` (denoted as `f =O[l] fun x => -g' x`). In other words, if `f` grows no faster than `g'` in terms of `l`, then `f` also grows no faster than the negation of `g'` in terms of `l`.
More concisely: If `f` is Big O of `g'` at filter `l`, then `f` is also Big O of `-g'` at filter `l` in the context of normed spaces `E` and semi-normed add commutative groups `F'`.
|
Asymptotics.isBigO_const_const
theorem Asymptotics.isBigO_const_const :
∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] (c : E)
{c' : F''}, c' ≠ 0 → ∀ (l : Filter α), (fun _x => c) =O[l] fun _x => c'
This theorem, `Asymptotics.isBigO_const_const`, states that for any types `α`, `E`, and `F''`, where `E` and `F''` are normed, for any `E`-type constant `c`, `F''`-type constant `c'` (which is not zero), and any filter `l` of type `α`, the function that always returns `c` is Big O of the function that always returns `c'`. In other words, the growth rate of a constant function is bounded above by the growth rate of another non-zero constant function, regardless of the input type or the filter used.
More concisely: For any types `α`, `E`, and `F''`, and non-zero constants `c` of type `E` and `c'` of type `F''`, the constant function `λx:α => c` is Big O of the constant function `λx:α => c'`.
|
summable_of_isBigO
theorem summable_of_isBigO :
∀ {ι : Type u_1} {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : CompleteSpace E] {f : ι → E}
{g : ι → ℝ}, Summable g → f =O[Filter.cofinite] g → Summable f
The theorem `summable_of_isBigO` asserts that for any types `ι` and `E` (where `E` is a seminormed additively commutative group and a complete space), and any functions `f: ι → E` and `g: ι → ℝ`, if `g` is summable and `f` is big O of `g` with respect to the cofinite filter (meaning that `f` is bounded above by some multiple of `g` outside of a finite set), then `f` is also summable. In other words, if a function `f` is dominated by a summable function `g` in the order of growth, then `f` is also summable.
More concisely: If `f: ι → E` is a function that is big O of the summable function `g: ι → ℝ` with respect to the cofinite filter, then `f` is summable.
|
Asymptotics.isLittleO_const_left
theorem Asymptotics.isLittleO_const_left :
∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E'']
[inst_1 : NormedAddCommGroup F''] {g'' : α → F''} {l : Filter α} {c : E''},
(fun _x => c) =o[l] g'' ↔ c = 0 ∨ Filter.Tendsto (norm ∘ g'') l Filter.atTop
The theorem `Asymptotics.isLittleO_const_left` states that for any types `α`, `E''`, and `F''` and for any function `g''` from `α` to `F''`, and any filter `l` on `α`, and any constant `c` of type `E''`, the function that is constantly equal to `c` is little-o of `g''` with respect to the filter `l` if and only if `c` is zero or the norm of `g''` tends to infinity with respect to the filter `l`. Here, a function `f` being little-o of `g` (denoted `f =o[l] g`) essentially means that `f` grows no faster than `g` near the points determined by the filter `l`.
More concisely: For any types `α`, `E''`, and `F''`, function `g''` from `α` to `F''`, filter `l` on `α`, and constant `c` of type `E''`, the constant function equal to `c` is little-o of `g''` with respect to `l` if and only if `c` is zero or the norm of `g''` approaches infinity at points in the filter `l`.
|
Asymptotics.isBigOWith_neg_right
theorem Asymptotics.isBigOWith_neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
(Asymptotics.IsBigOWith c l f fun x => -g' x) ↔ Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.isBigOWith_neg_right` states that for all types `α`, `E`, and `F'`, and for any real number `c`, functions `f : α → E` and `g' : α → F'`, and a filter `l` on `α`, the property that `f` is Big O of `-g'` (in the sense that the norm of `f` is eventually bounded by `c` times the norm of `-g'` at the limit points of the filter `l`) is equivalent to the property that `f` is Big O of `g'`. This means that negating the second function does not change the Big O relationship.
More concisely: The theorem `Asymptotics.isBigOWith_neg_right` asserts that for all types `α`, functions `f : α -> E`, `g' : α -> F'`, real number `c`, and filter `l` on `α`, `f` is Big O of `g'` if and only if `f` is Big O of `-g'`.
|
Asymptotics.isBigOWith_fst_prod
theorem Asymptotics.isBigOWith_fst_prod :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α},
Asymptotics.IsBigOWith 1 l f' fun x => (f' x, g' x)
The theorem `Asymptotics.isBigOWith_fst_prod` states that for any type `α`, `E'` and `F'`, where `E'` and `F'` are semi-normed additive commutative groups, given a filter `l` on `α` and functions `f': α → E'` and `g': α → F'`, the function `f'` is bounded by the function that maps `x` to the ordered pair `(f' x, g' x)` in the sense of Big O notation with constant factor 1, under the filter `l`. In terms of Big O notation, this means `f'(x)` is O(`(f' x, g' x)`), and the ratio `‖f'‖ / ‖(f' x, g' x)‖` is eventually less than or equal to 1 for large `x`, according to the filter `l`.
More concisely: For any type `α` and semi-normed additive commutative groups `E'` and `F'`, given a filter `l` on `α`, functions `f': α → E'` and `g': α → F'`, `f'` is Big O of the constant function mapping to `(f' x, g' x)` under filter `l`.
|
Asymptotics.isBigOWith_of_le
theorem Asymptotics.isBigOWith_of_le :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
(l : Filter α), (∀ (x : α), ‖f x‖ ≤ ‖g x‖) → Asymptotics.IsBigOWith 1 l f g
This theorem, `Asymptotics.isBigOWith_of_le`, states that for all types `α`, `E`, and `F`, given two functions `f` and `g` from `α` to `E` and `F` respectively, and a filter `l` on `α`, if the norm of `f(x)` is less than or equal to the norm of `g(x)` for all `x` in `α`, then `f` is Big `O` of `g` with a constant of `1` at filter `l`. In other words, in the asymptotic analysis of the two functions `f` and `g`, if the absolute value of `f(x)` is always less than or equal to the absolute value of `g(x)`, then `f` grows no faster than `g`, up to a constant factor of `1`.
More concisely: If for all `x` in `α`, the norm of `f(x)` is less than or equal to the norm of `g(x)`, then `f` is Big O of `g` with a constant of `1` at filter `l`. In other words, `|f(x)| ≤ |g(x)|` implies `f = O(g)` up to a constant factor of `1`.
|
Filter.IsBoundedUnder.isBigO_const
theorem Filter.IsBoundedUnder.isBigO_const :
∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
{l : Filter α},
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f) → ∀ {c : F''}, c ≠ 0 → f =O[l] fun _x => c
This theorem states that for any types `α`, `E`, and `F''`, given a normed space `E`, a normed additive commutative group `F''`, a function `f` from `α` to `E`, and a filter `l` on `α`; if the image of the filter `l` under the norm of `f` is eventually bounded with respect to the less than or equal to relation, then for any non-zero constant `c` from `F''`, `f` is big O of the constant function that always returns `c` with respect to the filter `l`. This is a statement about asymptotic complexity: it says that if `f` is eventually bounded, then its growth rate is at most constant.
More concisely: If a function from a type to a normed space is eventually bounded with respect to a filter, then its growth rate is at most constant with respect to that filter.
|
Asymptotics.isLittleO_of_tendsto
theorem Asymptotics.isLittleO_of_tendsto :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
(∀ (x : α), g x = 0 → f x = 0) → Filter.Tendsto (fun x => f x / g x) l (nhds 0) → f =o[l] g
This theorem, referred to as the alias of the reverse direction of `Asymptotics.isLittleO_iff_tendsto`, states that for any types `α` and `𝕜`, where `𝕜` is a normed division ring, and for any filter `l` and two functions `f` and `g` from `α` to `𝕜`, if for every `x` in `α`, `g` of `x` is zero implies that `f` of `x` is also zero, and if the limit of the function `f/g` as `x` approaches any value in the domain `α` (according to filter `l`) is zero, then `f` is little-o of `g` (denoted by `f =o[l] g`). That is, the function `f` is asymptotically smaller than `g` at all points determined by the filter `l`.
More concisely: If a function `f` from type `α` to a normed division ring `𝕜` satisfies `g(x) = 0 implies f(x) = 0` and `lim (f/g)ₗl = 0`, then `f = o[l] g`. (Here, `lim (f/g)ₗl` denotes the limit of the quotient `f/g` as `x` approaches any value in `α` according to filter `l`.)
|
Asymptotics.IsBigO.exists_eq_mul
theorem Asymptotics.IsBigO.exists_eq_mul :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
u =O[l] v → ∃ φ, Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ φ) ∧ l.EventuallyEq u (φ * v)
The theorem `Asymptotics.IsBigO.exists_eq_mul` is essentially the forward direction of the theorem `Asymptotics.isBigO_iff_exists_eq_mul`. It states that for any types `α` and `𝕜`, where `𝕜` is a normed division ring, and for any filter `l` over `α` and any functions `u` and `v` from `α` to `𝕜`, if `u` is Big-O of `v` at `l` (in other words, if `u` is asymptotically not greater than `v`), then there exists a function `φ` such that the image of `l` under the norm of `φ` is eventually bounded under the less than or equal to relation and `l` eventually equals the product of `φ` and `v`. Essentially, `u` can be expressed as `φ * v` where `φ` is a function that is eventually bounded.
More concisely: If `u` is Big-O of `v` at filter `l` in the normed division ring `𝕜`, then there exists a function `φ` such that `||φ||_𝕜` is eventually bounded under `≤` on `l` and `l` is eventually equal to `φ * v`.
|
Asymptotics.IsBigO.congr_left
theorem Asymptotics.IsBigO.congr_left :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {g : α → F} {l : Filter α}
{f₁ f₂ : α → E}, f₁ =O[l] g → (∀ (x : α), f₁ x = f₂ x) → f₂ =O[l] g
This theorem is about asymptotic notation, specifically Big O notation, in the context of function analysis. It provides a condition under which we can replace one function with another in a Big O statement. Specifically, it states that for any two functions `f₁` and `f₂` mapping from some arbitrary type `α` to another type `E`, and another function `g` mapping from `α` to a third type `F` (with both `E` and `F` being types that have a norm), if `f₁` is Big O of `g` with respect to some filter `l`, and every output of `f₁` is equal to the corresponding output of `f₂`, then `f₂` is also Big O of `g` with respect to the same filter.
More concisely: If `f₁` is Big O of `g` with respect to filter `l` and `f₁(x) = f₂(x)` for all `x`, then `f₂` is Big O of `g` with respect to `l`.
|
Asymptotics.IsBigO.congr
theorem Asymptotics.IsBigO.congr :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
{g₁ g₂ : α → F}, f₁ =O[l] g₁ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → f₂ =O[l] g₂
This theorem states that for any types `α`, `E`, and `F` with norms defined for `E` and `F`, and any function `f₁`, `f₂`, `g₁`, `g₂` mapping `α` to `E` or `F`, if `f₁` is big-O of `g₁` under some arbitrary filter `l`, and `f₁` is identical to `f₂` for all `x : α`, and `g₁` is identical to `g₂` for all `x : α`, then `f₂` is also big-O of `g₂` under the same filter `l`. In simpler terms, this means that if two function pairs are identical and the first pair adheres to big-O notation, then the second pair also adheres to big-O notation.
More concisely: If functions `f₁` and `f₂` are identical and `f₁` is big-O of `g₁`, where `g₁` is identical to `g₂`, then `f₂` is big-O of `g₂`.
|
Asymptotics.IsBigOWith.of_bound
theorem Asymptotics.IsBigOWith.of_bound :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
{l : Filter α}, (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.IsBigOWith.of_bound` states that for any types `α`, `E`, and `F`, any normed spaces `E` and `F`, any real number `c`, any functions `f: α → E` and `g: α → F`, and any filter `l` on `α`, if it is true that, eventually for `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`, then `f` is big-O of `g` with constant `c` at `l`, in the sense of the Landau notation `IsBigOWith`. This means that `‖f‖ / ‖g‖` is eventually bounded by `c`, modulo division by zero issues that are avoided by this definition.
More concisely: If for all x in the filter l, the norm of f(x) is bounded above by c times the norm of g(x), then f is big-O of g with constant c at filter l.
|
Asymptotics.isLittleO_iff_forall_isBigOWith
theorem Asymptotics.isLittleO_iff_forall_isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.isLittleO_iff_forall_isBigOWith` states that, given any types `α`, `E`, and `F` where `E` and `F` have a defined norm, along with functions `f : α → E` and `g : α → F` and a filter `l` on `α`, `f` is little-o of `g` at `l` if and only if for all real numbers `c` greater than 0, `f` is Big-O of `g` at `l` with constant `c`. In mathematical terms, this is saying $f(x) = o(g(x))$ as x approaches `l` if and only if for all positive constants `c`, there exists an `N` such that for all `x > N`, the absolute value of `f(x)/g(x)` is less than `c`. This theorem provides a characterization of little-o notation in terms of Big-O notation.
More concisely: For functions `f : α → E` and `g : α → F` defined on type `α` with norms, `f` is little-o of `g` at filter `l` if and only if for every positive constant `c`, there exists an `N` such that for all `x > N`, `|f(x)/g(x)| < c`.
|
Asymptotics.IsBigO.neg_left
theorem Asymptotics.IsBigO.neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, f' =O[l] g → (fun x => -f' x) =O[l] g
This theorem, named `Asymptotics.IsBigO.neg_left`, is an alias of the reverse direction of `Asymptotics.isBigO_neg_left`. It states that for any types `α`, `F`, and `E'`, with `F` being normed and `E'` being a semi-normed add commutative group, and any functions `g : α → F` and `f' : α → E'`, if `f'` is big-O of `g` at some filter `l` (written as `f' =O[l] g`), then the negation of `f'` is also big-O of `g` at the same filter. In mathematical terms, if `f'` is asymptotically bounded by `g`, then `-f'` is also asymptotically bounded by `g`.
More concisely: If `f'` is big-O of `g` at filter `l`, then `-f'` is also big-O of `g` at filter `l`. In other words, the negative of a big-O function is still big-O of the original function.
|
Asymptotics.isBigO_abs_left
theorem Asymptotics.isBigO_abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
(fun x => |u x|) =O[l] g ↔ u =O[l] g
This theorem states that for any type `α`, any normed type `F`, any function `g : α → F`, any filter `l : Filter α`, and any function `u : α → ℝ`, the absolute value function of `u` is a big-O of `g` with respect to the filter `l` if and only if `u` itself is a big-O of `g` with respect to the same filter. In mathematical terms, we say that |u(x)| = O(g(x)) if and only if u(x) = O(g(x)), where the big-O notation represents the Asymptotic upper bound.
More concisely: For any type `α`, normed type `F`, function `g : α → F`, filter `l : Filter α`, and function `u : α → ℝ`, the absolute value of `u` is a big-O of `g` with respect to `l` if and only if `u` itself is a big-O of `g` with respect to `l`. In other words, |u(x)| = O(g(x)) if and only if u(x) = O(g(x)).
|
PartialHomeomorph.isBigOWith_congr
theorem PartialHomeomorph.isBigOWith_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
[inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : PartialHomeomorph α β) {b : β},
b ∈ e.target →
∀ {f : β → E} {g : β → F} {C : ℝ},
Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
This theorem states that the big-O notation for functions `f` and `g` with respect to a constant `C` and a neighborhood filter at a point `b` in the target of a partial homeomorphism `e` is preserved under the inverse of this homeomorphism. In other words, if `f` is big-O of `g` at `b`, then the composition of `f` and `g` with the inverse of the homeomorphism also maintains this relationship at the point that maps to `b` under the inverse homeomorphism, assuming that the norms on the codomains of `f` and `g` and the topologies on their domains are given. The big-O notation `IsBigOWith C (nhds b) f g` means that the norm of `f` divided by the norm of `g` is eventually (at points close to `b`) bounded by `C`.
More concisely: If `f` is big-O of `g` at `b` under a partial homeomorphism `e`, then `e.symm ∘ f` is big-O of `g ∘ e.symm` at `e.target b`.
|
Asymptotics.isLittleO_abs_left
theorem Asymptotics.isLittleO_abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
(fun x => |u x|) =o[l] g ↔ u =o[l] g
This theorem, `Asymptotics.isLittleO_abs_left`, states that for any type `α`, a type `F` which has a norm, a function `g` from `α` to `F`, a filter `l` on `α`, and a function `u` from `α` to real numbers, the absolute value function applied to `u` is little-o of `g` at the filter `l` if and only if `u` itself is little-o of `g` at the same filter. In more mathematical terms, it says that $|u(x)| = o(g(x))$ as $x$ approaches the limit defined by the filter `l` if and only if $u(x) = o(g(x))$ under the same conditions.
More concisely: For any type `α`, function `g : α → F` with norm, filter `l` on `α`, and function `u : α → ℝ`, the absolute value of `u` is little-o of `g` at `l` if and only if `u` is little-o of `g` at `l`. |`|u|` is `o(g)` at `l` if and only if `u` is `o(g)` at `l`.
|
Asymptotics.IsLittleO.of_bound
theorem Asymptotics.IsLittleO.of_bound :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → f =o[l] g
This theorem, `Asymptotics.IsLittleO.of_bound`, states that for any types `α`, `E`, `F`, with the `Norm` instances for `E` and `F`, and given functions `f : α → E`, `g : α → F`, and a filter `l` on `α`, if for all positive real numbers `c`, eventually (with respect to the filter `l`) the norm of `f x` is less than or equal to `c` times the norm of `g x`, then `f` is little-o of `g` at `l`. In simpler terms, this theorem provides a condition under which we can say that the function `f` grows no faster than `g` in the limit according to the filter `l`.
More concisely: If for all `c > 0`, eventually (with respect to filter `l` on type `α`) the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)` for all `x` in `α`, then `f` is little-o of `g` with respect to the filter `l`.
|
Asymptotics.IsBigO.trans
theorem Asymptotics.IsBigO.trans :
∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
[inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
f =O[l] g → g =O[l] k → f =O[l] k
This theorem states that the big O notation, a notation used to describe the limiting behavior of a function when the argument tends towards a particular value or infinity, is transitive for sequences of functions. More specifically, if we have three functions `f`, `g`, and `k` of any types `E`, `F'`, and `G` respectively, and a filter `l` of type `α`, if `f` is big O of `g`, denoted `f =O[l] g`, and `g` is big O of `k`, denoted `g =O[l] k`, then it follows that `f` is big O of `k`, denoted `f =O[l] k`. The filter `l` can be thought of as a "context" in which these functions are being compared. This theorem is a fundamental property of the big O notation and is important in the analysis of computational complexity in computer science, among other fields.
More concisely: If functions `f`, `g`, and `k` are such that `f =O[l] g` and `g =O[l] k` for some filter `l`, then `f =O[l] k`.
|
Asymptotics.isBigOWith_abs_left
theorem Asymptotics.isBigOWith_abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {c : ℝ} {g : α → F} {l : Filter α} {u : α → ℝ},
Asymptotics.IsBigOWith c l (fun x => |u x|) g ↔ Asymptotics.IsBigOWith c l u g
This theorem, `Asymptotics.isBigOWith_abs_left`, states that for any types `α` and `F` with a norm on `F`, a real number `c`, a function `g` mapping `α` to `F`, a filter `l` on `α` and a function `u` mapping `α` to real numbers, the condition that the absolute value of `u(x)` is big-O of `g` with respect to `c` and `l` (in other words, the norm of `u(x)` is eventually bounded by `c` times the norm of `g`, for `l`), is equivalent to the condition that `u(x)` itself is big-O of `g` with respect to `c` and `l`.
More concisely: If for all x in alpha, the absolute value of u(x) is big-O of g(x) with respect to c and filter l, then u is big-O of g with respect to c and filter l.
|
Asymptotics.IsBigOWith.right_le_sub_of_lt_1
theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_1 :
∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'},
Asymptotics.IsBigOWith c l f₁ f₂ → c < 1 → Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x
The theorem `Asymptotics.IsBigOWith.right_le_sub_of_lt_1` states that for any types `α` and `E'`, where `E'` is a seminormed additive commutative group, given a real number `c`, a filter `l` on `α`, and two functions `f₁` and `f₂` from `α` to `E'`, if the function `f₁` is big O of the function `f₂` with constant `c` under the filter `l` and `c` is less than 1, then the function `f₂ - f₁` is big O of the function `f₂` with constant `1 / (1 - c)` under the same filter `l`. In simpler terms, it's about a particular relationship between the growth rates of `f₁`, `f₂`, and `f₂ - f₁` when `c` is less than 1.
More concisely: If `f₁` is big O of `f₂` with constant `c` (`0 < c < 1`) under filter `l` in the seminormed additive commutative group `E'`, then `f₂ - f₁` is big O of `f₂` with constant `1 / (1 - c)` under the same filter `l`.
|
Asymptotics.IsBigOWith.norm_right
theorem Asymptotics.IsBigOWith.norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
Asymptotics.IsBigOWith c l f g' → Asymptotics.IsBigOWith c l f fun x => ‖g' x‖
The theorem `Asymptotics.IsBigOWith.norm_right` is an alias of the reverse direction of another theorem `Asymptotics.isBigOWith_norm_right`. This theorem states that for any types `α`, `E`, `F'`, any norms on `E` and `F'`, any real number `c`, any functions `f : α → E` and `g' : α → F'`, and any filter `l` on `α`, if `f` is Big-O of `g'` with respect to the filter `l` and constant `c` (i.e., `Asymptotics.IsBigOWith c l f g'`), then `f` is also Big-O of the function that maps `x` to the norm of `g'(x)`, with the same constant `c` and filter `l` (i.e., `Asymptotics.IsBigOWith c l f fun x => ‖g' x‖`). In simpler terms, this theorem allows us to replace `g'` with its norm when analyzing the Big-O behavior of `f` relative to `g'`.
More concisely: If `f` is Big-O of `g'` with respect to filter `l` and constant `c`, then `f` is also Big-O of the function `x => ‖g' x‖` with the same filter `l` and constant `c`.
|
Asymptotics.isBigO_iff''
theorem Asymptotics.isBigO_iff'' :
∀ {α : Type u_1} {E : Type u_3} {E''' : Type u_12} [inst : Norm E] [inst_1 : SeminormedAddGroup E'''] {f : α → E}
{l : Filter α} {g : α → E'''}, f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
This theorem, `Asymptotics.isBigO_iff''`, defines the concept of Big O notation in terms of filters by involving a constant in the lower bound. For every normed vector space `E`, seminormed add group `E'''`, function `f` from `α` to `E`, filter `l` on `α`, and function `g` from `α` to `E'''`, it states that `f` is Big O of `g` at filter `l` if and only if there exists a positive constant `c` such that, eventually for every `x` in `l`, `c` times the norm of `f(x)` is less than or equal to the norm of `g(x)`.
More concisely: For any normed vector space `E`, seminormed add group `E'''`, function `f` from `α` to `E`, filter `l` on `α`, and function `g` from `α` to `E'''`, `f` is Big O of `g` at filter `l` if and only if there exists a constant `c > 0` such that, for all `x` in `l`, `‖f(x)‖ ≤ c * ‖g(x)‖`.
|
Asymptotics.IsBigO.of_neg_right
theorem Asymptotics.IsBigO.of_neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =O[l] fun x => -g' x) → f =O[l] g'
The theorem `Asymptotics.IsBigO.of_neg_right` states that for any types `α`, `E`, `F'`, any function `f : α → E`, any function `g' : α → F'`, and any filter `l` on `α`, if `f` is big O of `-g'` at `l` (denoted as `f =O[l] fun x => -g' x`), then `f` is also big O of `g'` at `l` (denoted as `f =O[l] g'`). Here, `f =O[l] g'` means that there exist constants such that `f(x)` is less than or equal to that constant times `|g'(x)|` for all `x` in a set defined by the filter `l`. This theorem thus states a property about the equivalence of asymptotic bounds on a function `f` when the comparator function `g'` is negated.
More concisely: If `f` is big O of the negation of `g` at a filter `l`, then `f` is also big O of `g` at `l`.
|
Asymptotics.IsBigO.norm_norm
theorem Asymptotics.IsBigO.norm_norm :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α},
f' =O[l] g' → (fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖
This theorem, `Asymptotics.IsBigO.norm_norm`, is an alias for the reverse direction of `Asymptotics.isBigO_norm_norm`. It states that for any types `α`, `E'`, `F'`, and given `f': α → E'` and `g': α → F'`, along with a filter `l` on `α`, and instances of `E'` and `F'` equipped with seminorms forming seminormed commutative additive groups, if `f'` is of the same big O order as `g'` at the filter `l`, then the function mapping `x` to the norm of `f'(x)` is also of the same big O order as the function mapping `x` to the norm of `g'(x)` at the filter `l`. In LaTeX terms, if $f' = O(g')$ at `l`, then $\|f'(x)\| = O(\|g'(x)\|)$ at `l`.
More concisely: If `f': α → E'` and `g': α → F'` are functions with the same big O order at filter `l` on `α`, then the norms of `f'` and `g'` are of the same big O order at filter `l`. In mathematical notation, if $f' = O(g')$ at `l`, then $\|f'\| = O(\|g Situation\|)$ at `l`.
|
Asymptotics.bound_of_isBigO_cofinite
theorem Asymptotics.bound_of_isBigO_cofinite :
∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
{g'' : α → F''}, f =O[Filter.cofinite] g'' → ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
The theorem `Asymptotics.bound_of_isBigO_cofinite` states that if a function `f` is big-O notation of a function `g''` along the cofinite filter (i.e., if `f` is asymptotically bounded above by `g''` for large input values), then there exists a positive constant `C` such that for any input `x` where `g'' x` is not zero, the norm (or "magnitude") of `f x` is less than or equal to `C` times the norm of `g'' x`. This essentially provides a way to bound the size of `f` in terms of another function `g''` and a constant, whenever `g'' x` is not zero.
More concisely: If a function `f` is big-O notation of `g''` along the cofinite filter, then there exists a constant `C` such that |`f x`| ≤ `C` * |`g'' x`| for all `x` where `g'' x` is non-zero.
|
Asymptotics.IsBigO.of_abs_left
theorem Asymptotics.IsBigO.of_abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
(fun x => |u x|) =O[l] g → u =O[l] g
This theorem, `Asymptotics.IsBigO.of_abs_left`, is an alias for the forward direction of `Asymptotics.isBigO_abs_left`. It states that for any types `α` and `F`, a norm instance on `F`, functions `g : α → F` and `u : α → ℝ`, and a filter `l` on `α`, if the function taking `x` to the absolute value of `u(x)` is Big O of `g` at `l` (i.e., the former function is asymptotically bounded above by a constant multiple of the latter), then `u` itself is also Big O of `g` at `l`. In other words, if the absolute value of `u` is asymptotically bounded by `g`, then `u` is also asymptotically bounded by `g`.
More concisely: If the absolute value of a function `u : α → ℝ` is Big O of another function `g : α → F` at a filter `l` on `α`, then `u` is also Big O of `g` at `l`.
|
Asymptotics.isBigO_zero
theorem Asymptotics.isBigO_zero :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] (g : α → F)
(l : Filter α), (fun _x => 0) =O[l] g
This theorem, `Asymptotics.isBigO_zero`, states that for any types `α`, `F`, and `E'`, if a function `g : α → F` is considered, and `l` is a filter on `α`, then the zero function (i.e., a function that returns zero for all inputs) is "Big O" of `g` at `l`. In Big O notation, this is expressed as `0 =O[l] g`. This implies that the zero function grows no faster than `g` in the limit as we approach the points specified by the filter `l`. The types `F` and `E'` are required to have a norm and a seminormed add commutative group structure, respectively, to ensure that the concept of "Big O" is well-defined.
More concisely: For any type `α`, filter `l` on `α`, and functions `g : α → F` where `F` has a norm and `E'` has a seminormed add commutative group structure, the zero function is Big O of `g` at `l`, i.e., `0 =O[l] g`.
|
Asymptotics.isBigOWith_abs_right
theorem Asymptotics.isBigOWith_abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {c : ℝ} {f : α → E} {l : Filter α} {u : α → ℝ},
(Asymptotics.IsBigOWith c l f fun x => |u x|) ↔ Asymptotics.IsBigOWith c l f u
This theorem, `Asymptotics.isBigOWith_abs_right`, states that for any types `α` and `E`, with `E` possessing a norm, any real constant `c`, any function `f` from `α` to `E`, any filter `l` on `α`, and any function `u` from `α` to real numbers, the property that `f` is big O with respect to the absolute value of `u` (i.e., the function value `|u(x)|`) under the filter `l` with constant `c` (denoted as `Asymptotics.IsBigOWith c l f (λ x => |u x|)`) is equivalent to the property that `f` is big O with respect to `u itself` under the same filter with the same constant (denoted as `Asymptotics.IsBigOWith c l f u`). In other words, the Landau notation `IsBigOWith` is invariant under taking the absolute value of the function on the right-hand side.
More concisely: The theorem `Asymptotics.isBigOWith_abs_right` in Lean 4 states that for any type `α`, real constant `c`, function `f` from `α` to a normed type `E`, filter `l` on `α`, and function `u` from `α` to real numbers, `Asymptotics.IsBigOWith c l f (λ x => |u x|)` is equivalent to `Asymptotics.IsBigOWith c l f u`. In other words, the Landau notation `IsBigOWith` is invariant under taking the absolute value of the right-hand side function.
|
Asymptotics.IsBigOWith.bound
theorem Asymptotics.IsBigOWith.bound :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
{l : Filter α}, Asymptotics.IsBigOWith c l f g → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
The theorem `Asymptotics.IsBigOWith.bound` states that for any real number `c`, any functions `f` and `g` from a type `α` to normed types `E` and `F` respectively, and any filter `l` on `α`, if `Asymptotics.IsBigOWith c l f g` holds true (indicating that the norm of `f` is eventually bounded by `c` times the norm of `g` under the filter `l`), then there exists an eventuality (a set of elements in `α` for which a certain condition holds, represented by `∀ᶠ (x : α) in l`) where the norm of `f` at any such element `x` is less than or equal to `c` times the norm of `g` at `x`. In mathematical terms, this states that if `f` is Big-O of `g` with constant `c` and filter `l`, then eventually (with respect to `l`), the inequality `‖f(x)‖ ≤ c * ‖g(x)‖` holds for all `x`.
More concisely: If `f` is Big-O of `g` with constant `c` and filter `l`, then there exists an eventuality `x ∈ l` such that `‖f(x)‖ ≤ c * ‖g(x)‖` for all `x`.
|
Filter.IsBoundedUnder.isBigO_one
theorem Filter.IsBoundedUnder.isBigO_one :
∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
[inst_2 : One F] [inst_3 : NormOneClass F],
(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f x‖) → f =O[l] fun _x => 1
This theorem, named "Filter.IsBoundedUnder.isBigO_one", states that for any types `α`, `E`, and `F`, given that `E` and `F` have a notion of norm, `f` is a function from `α` to `E`, `l` is a filter on `α`, and `F` has an instance of the `One` typeclass and `NormOneClass`, if the image of the filter `l` under the map that sends `x` to the norm of `f(x)` (`‖f x‖`) is eventually bounded with respect to the less than or equal to (`≤`) relation, then `f` is Big O of the constant function 1 at `l` (`f =O[l] fun _x => 1`). Here, "Big O" is a notation used in asymptotic analysis indicating that `f` is bounded above by some constant times the function `fun _x => 1`, for all `x` in a subset defined by `l`.
More concisely: If a filter on a type with a normed additive abelian group structure is eventually bounded under the norm of a function from that type to another normed additive abelian group, then the function is Big O of the constant function 1 with respect to the filter.
|
Asymptotics.isBigO_iff'
theorem Asymptotics.isBigO_iff' :
∀ {α : Type u_1} {E : Type u_3} {E''' : Type u_12} [inst : Norm E] [inst_1 : SeminormedAddGroup E'''] {f : α → E}
{l : Filter α} {g : α → E'''}, f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
This theorem states that a function `f` is Big O of another function `g` with respect to a given filter `l` if and only if there exists a positive constant `c` such that, eventually for all `x` in the filter `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`. Here, `f` and `g` are functions from some type `α` to normed types `E` and `E'''` respectively, and `l` is a filter on the type `α`. The 'eventually' qualifier implies that this condition need not hold for all `x`, but must hold for all `x` beyond a certain point in the filter `l`.
More concisely: A function `f : α → E` is Big O of another function `g : α → E'''` with respect to a filter `l` on `α` if and only if there exists a constant `c > 0` such that, for all `x ∈ l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`.
|
Asymptotics.isBigOWith_neg_left
theorem Asymptotics.isBigOWith_neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ}
{g : α → F} {f' : α → E'} {l : Filter α},
Asymptotics.IsBigOWith c l (fun x => -f' x) g ↔ Asymptotics.IsBigOWith c l f' g
The theorem `Asymptotics.isBigOWith_neg_left` asserts that for any types `α`, `F`, and `E'`, with `F` having a norm structure and `E'` having a seminormed additive commutative group structure, for any real number `c`, any function `g : α → F`, any function `f' : α → E'`, and any filter `l` on `α`, the statement that `f'` is 'big O' of `g` (in the sense of the `Asymptotics.IsBigOWith` definition) with constant `c` and filter `l` is equivalent to the statement that the negation of `f'` is 'big O' of `g` with the same constant and filter. In other words, the 'big O' relationship is preserved when taking the negation of the function.
More concisely: The negation of a function being big O of another function, with a constant and filter, is equivalent to the original function being big O of the negation of the other function with the same constant and filter.
|
Asymptotics.isBigOWith_of_le'
theorem Asymptotics.isBigOWith_of_le' :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
(l : Filter α), (∀ (x : α), ‖f x‖ ≤ c * ‖g x‖) → Asymptotics.IsBigOWith c l f g
This theorem states that for all types `α`, `E`, and `F` where `E` and `F` have a norm, given a real number `c` and two functions `f` and `g` from `α` to `E` and `F` respectively, and a filter `l` on `α`. If it is the case that for all `x` in `α`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`, then `f` is big O of `g` with constant `c` at filter `l`. In other words, the output of function `f` is asymptotically bounded by `c` times the output of function `g` modulo division by zero issues.
More concisely: Given types `α`, `E`, and `F` with norms, and functions `f : α → E` and `g : α → F`, if for all `x` in `α`, `||f x|| ≤ c * ||g x||`, then `f` is big O of `g` with constant `c` in the filter topology.
|
Asymptotics.IsBigOWith.norm_left
theorem Asymptotics.IsBigOWith.norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ}
{g : α → F} {f' : α → E'} {l : Filter α},
Asymptotics.IsBigOWith c l f' g → Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g
The theorem `Asymptotics.IsBigOWith.norm_left` is an alias for the reverse direction of `Asymptotics.isBigOWith_norm_left`. It states that for any types `α`, `F`, and `E'`, where `F` and `E'` have norms, any real number `c`, any functions `g : α → F` and `f' : α → E'`, and any filter `l` on `α`, if the function `f'` is of Big O order with respect to `g` at the filter `l` with constant `c`, then the function that sends `x` to the norm of `f' x` is also of Big O order with respect to `g` at the filter `l` with the same constant `c`. In other words, if `f'` is eventually bounded by `c * g` with respect to `l`, then the norm of `f'` is also eventually bounded by `c * g` with respect to `l`.
More concisely: If `f': α → E'` is Big O of `g: α → F` at filter `l` with constant `c`, then the function `x ↦ ||f' x||` is also Big O of `g` at filter `l` with constant `c`.
|
Asymptotics.IsBigO.of_abs_abs
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
This theorem, `Asymptotics.IsBigO.of_abs_abs`, is an alias for the forward direction of the `Asymptotics.isBigO_abs_abs` theorem. It states that for any type `α`, filter `l`, and real-valued functions `u` and `v` defined on `α`, if the absolute value of `u` is Big O of the absolute value of `v` (denoted as `|u(x)| = O(|v(x)|)`), then `u` is Big O of `v` (denoted as `u(x) = O(v(x))`). That is, if the growth rate of the absolute values of `u` and `v` are comparable, then the growth rates of `u` and `v` themselves are also comparable.
More concisely: If the absolute value of function `u` is Big O of the absolute value of function `v`, then `u` is Big O of `v`.
|
Asymptotics.IsBigOWith.right_le_sub_of_lt_one
theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one :
∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'},
Asymptotics.IsBigOWith c l f₁ f₂ → c < 1 → Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x
The theorem `Asymptotics.IsBigOWith.right_le_sub_of_lt_one` states that for any types `α` and `E'`, where `E'` is a semi-normed additive commutative group, and any real number `c`, filter `l` on `α`, and functions `f₁` and `f₂` from `α` to `E'`, if `f₁` is Big-O of `f₂` with constant `c` at filter `l` (i.e., `f₁` is eventually bounded by `c * f₂` at `l`), and `c` is less than 1, then `f₂` is Big-O of `f₂ - f₁` with constant `1 / (1 - c)` at filter `l`. In other words, `f₂` is eventually bounded by `1 / (1 - c)` times `f₂ - f₁` at `l`. This theorem governs the interaction of Big-O notation with subtraction under certain conditions.
More concisely: If `f₁` is Big-O of `f₂` with constant `c` at filter `l` and `0 < c < 1`, then `f₂` is Big-O of `f₂ - f₁` with constant `1 / (1 - c)` at filter `l`.
|
Asymptotics.IsBigOWith.of_norm_right
theorem Asymptotics.IsBigOWith.of_norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
(Asymptotics.IsBigOWith c l f fun x => ‖g' x‖) → Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.IsBigOWith.of_norm_right` is an alias for the forward direction of `Asymptotics.isBigOWith_norm_right`. It states that for any types `α`, `E`, and `F'`, with `E` having a defined norm, and `F'` being a seminormed add commutative group, given a real number `c`, a function `f` from `α` to `E`, a function `g'` from `α` to `F'`, and a filter `l` on `α`, if the function `f` is in BigO with respect to the norm of `g'` (denoted as `‖g' x‖`) at the filter `l` with a constant `c`, then `f` is also in BigO with respect to `g'` itself at the filter `l` with the same constant `c`. In simpler terms, if the growth rate of `f` is eventually no greater than `c` times the norm of `g'`, then the growth rate of `f` is also eventually no greater than `c` times `g'`.
More concisely: If a function `f` is Big O of `g'` with respect to the norm `‖.‖` at filter `l` with constant `c`, then `f` is also Big O of `g'` at filter `l` with the same constant `c`.
|
Asymptotics.IsLittleO.eventually_mul_div_cancel
theorem Asymptotics.IsLittleO.eventually_mul_div_cancel :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
u =o[l] v → l.EventuallyEq (u / v * v) u
This theorem states that for any normed division ring `𝕜` and filter `l`, and any functions `u` and `v` from `α` to `𝕜`, if `u` is little-o of `v` along `l`, then almost everywhere (with respect to `l`), the expression `(u / v) * v` is equal to `u`. In mathematical terms, if `u = o(v)` as `l` approaches some value, then we can cancel the division and multiplication by `v` in the expression `(u / v) * v` to get `u` eventually.
More concisely: For any normed division ring `𝕜`, if function `u` is little-o of `v` along filter `l`, then `(u / v) * v` equals `u` almost everywhere with respect to `l`.
|
Asymptotics.IsLittleO.mono
theorem Asymptotics.IsLittleO.mono :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l l' : Filter α}, f =o[l'] g → l ≤ l' → f =o[l] g
This theorem, `Asymptotics.IsLittleO.mono`, states that given any two types `α`, `E`, and `F`, where `E` and `F` have a norm, and functions `f : α → E`, `g : α → F`, along with two filters `l` and `l'` over `α`, if `f` is little-o of `g` at filter `l'` (`f =o[l'] g`) and `l` is less than or equal to `l'` (`l ≤ l'`), then `f` is also little-o of `g` at filter `l` (`f =o[l] g`). In big-O notation, if `f(x)` is asymptotically smaller than `g(x)` as `x` approaches a limit under a certain condition (defined by filter `l'`), and if this condition is at least as restrictive as another condition (defined by filter `l`), then `f(x)` is also asymptotically smaller than `g(x)` as `x` approaches the limit under this less restrictive condition.
More concisely: If `f =o[l'] g` and `l ≤ l'`, then `f =o[l] g`.
In other words, if `f(x)` is little-o of `g(x)` under filter `l'`, and `l` is less or equal to `l'`, then `f(x)` is also little-o of `g(x)` under filter `l`.
|
Asymptotics.IsBigOWith.abs_right
theorem Asymptotics.IsBigOWith.abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {c : ℝ} {f : α → E} {l : Filter α} {u : α → ℝ},
Asymptotics.IsBigOWith c l f u → Asymptotics.IsBigOWith c l f fun x => |u x|
The theorem `Asymptotics.IsBigOWith.abs_right` is an alias for the reverse direction of `Asymptotics.isBigOWith_abs_right`. It states that for any types `α` and `E`, given a norm on `E`, a real number `c`, a function `f` from `α` to `E`, a filter `l` on `α`, and a function `u` from `α` to `ℝ`, if `f` is Big O of `u` as per the `IsBigOWith` definition, then `f` is also Big O of the absolute value function of `u` (`|u(x)|`). In other words, if `‖f‖` is eventually bounded by `c * ‖u‖` near the points dictated by the filter `l`, then `‖f‖` is also eventually bounded by `c * ‖|u(x)|‖` near those same points.
More concisely: If `f` is Big O of `u` with respect to a norm on `E`, then `f` is also Big O of the absolute value function of `u` with respect to the same norm.
|
Asymptotics.IsBigO.comp_tendsto
theorem Asymptotics.IsBigO.comp_tendsto :
∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E}
{g : α → F} {l : Filter α},
f =O[l] g → ∀ {k : β → α} {l' : Filter β}, Filter.Tendsto k l' l → (f ∘ k) =O[l'] (g ∘ k)
The theorem `Asymptotics.IsBigO.comp_tendsto` states that for any types `α`, `β`, `E`, and `F`, given the normed spaces `E` and `F`, and two functions `f : α → E` and `g : α → F` with a filter `l` on `α`; if `f` is Big O of `g` at `l` (denoted as `f =O[l] g`), then for any function `k : β → α` and any filter `l'` on `β`, if `k` tends towards `l` under filter `l'` (denoted as `Filter.Tendsto k l' l`), then the composition of `f` and `k` is Big O of the composition of `g` and `k` at `l'` (denoted as `(f ∘ k) =O[l'] (g ∘ k)`).
In other words, if `f` is asymptotically bounded by `g` as `α` tends to `l`, then this asymptotic dominance is preserved under composition with a function `k` that tends towards `l` as `β` tends towards `l'`.
More concisely: If `f =O[l] g` and `Filter.Tendsto k l' l`, then `(f ∘ k) =O[l'] (g ∘ k)` for functions `f : α → E`, `g : α → F`, and `k : β → α` in the context of normed spaces `E` and `F` and filters `l` on `α` and `l'` on `β`.
|
Asymptotics.IsBigO.add
theorem Asymptotics.IsBigO.add :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → f₂ =O[l] g → (fun x => f₁ x + f₂ x) =O[l] g
This theorem, `Asymptotics.IsBigO.add`, states that for any given alpha type `α`, filter type `F`, and seminormed add commutative group `E'`, along with any given function `g : α → F` and filter `l`, if the functions `f₁ : α → E'` and `f₂ : α → E'` are both Big O of `g` with respect to `l` (expressed as `f₁ =O[l] g` and `f₂ =O[l] g`), then the function that maps `x` to `f₁ x + f₂ x` is also Big O of `g` with respect to `l`. In other words, the sum of two functions, each of which is Big O of a certain function, is itself Big O of the same function.
More concisely: If `f₁` and `f₂` are both Big O of `g` with respect to filter `l`, then `f₁ + f₂` is also Big O of `g` with respect to `l`.
|
Asymptotics.IsBigO.of_abs_right
theorem Asymptotics.IsBigO.of_abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
(f =O[l] fun x => |u x|) → f =O[l] u
This theorem, `Asymptotics.IsBigO.of_abs_right`, is an alias for the forward direction of `Asymptotics.isBigO_abs_right`. Given any types `α` and `E`, a norm over `E`, a function `f` from `α` to `E`, a filter `l` over `α`, and a function `u` from `α` to `ℝ`, it states that if `f` is bounded above by a constant multiple of the absolute value function `|u|` as observed through the filter `l` (denoted as `f =O[l] |u|`), then `f` is also bounded above by a constant multiple of the function `u` itself, observed through the same filter `l` (denoted as `f =O[l] u`).
More concisely: If a function `f` is bounded above by the absolute value of another function `u` up to a constant factor in the filter `l`, then `f` is also bounded above by `u` up to a constant factor in the same filter.
|
Asymptotics.IsLittleO.of_norm_left
theorem Asymptotics.IsLittleO.of_norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =o[l] g → f' =o[l] g
This is an alias for the forward direction of `Asymptotics.isLittleO_norm_left`. The theorem states that for any types `α`, `F`, and `E'`, given the normed type `F`, the seminormed additive commutative group `E'`, a function `g` mapping `α` to `F`, a function `f'` mapping `α` to `E'`, and a filter `l` on `α`, if the norm of `f'` is little-o of `g` at `l` (meaning that `f'` grows no faster than `g` in the limit towards `l`), then `f'` itself is also little-o of `g` at `l`.
More concisely: If `f'` is little-o of `g` in norm at filter `l`, then `f'` is also little-o of `g` at filter `l`.
|
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|
This theorem, an alias for the reverse direction of `Asymptotics.isBigO_abs_abs`, states that for all types `α`, filters `l` on `α`, and functions `u` and `v` from `α` to the real numbers `ℝ`, if `u` is big O of `v` with respect to filter `l`, then the absolute value of `u` is also big O of the absolute value of `v` with respect to the same filter `l`. In mathematical terms, if $u = O(v)$, then $|u| = O(|v|)$.
More concisely: For all types `α`, filters `l` on `α`, and functions `u` and `v` from `α` to `ℝ`, if `u` is big O of `v` with respect to `l`, then the absolute value of `u` is big O of the absolute value of `v` with respect to `l`. In mathematical notation, `|u| = O(|v|)` when `u = O(v)`.
|
Asymptotics.IsBigOWith.prod_left_same
theorem Asymptotics.IsBigOWith.prod_left_same :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'}
{k' : α → G'} {l : Filter α},
Asymptotics.IsBigOWith c l f' k' →
Asymptotics.IsBigOWith c l g' k' → Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k'
The theorem `Asymptotics.IsBigOWith.prod_left_same` states that for any type `α`, normed additive commutative groups `E'`, `F'`, and `G'`, a real number `c`, functions `f'`, `g'`, and `k'` from `α` to `E'`, `F'`, and `G'` respectively, and a filter `l` on `α`, if `f'` and `g'` are both "big O" of `k'` with constant `c` at filter `l`, then the function that takes `x` in `α` and returns the pair `(f' x, g' x)` is also "big O" of `k'` with the same constant `c` at the same filter `l`. Here, "big O" is a notation for asymptotic upper bounds, meaning that the norms of `f'` and `g'` are eventually at most `c` times the norm of `k'` for `l`.
More concisely: If functions `f'` and `g'` are both big O of `k'` with constant `c` at filter `l` on type `α`, then the function `x ↦ (f' x, g' x)` is also big O of `k'` with constant `c` at filter `l`.
|
Asymptotics.isBigOWith_self_const_mul'
theorem Asymptotics.isBigOWith_self_const_mul' :
∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] (u : Rˣ) (f : α → R) (l : Filter α),
Asymptotics.IsBigOWith ‖↑u⁻¹‖ l f fun x => ↑u * f x
This theorem states that for any non-zero scalar `u` in a seminormed ring `R`, any function `f` from type `α` to `R`, and any filter `l` on `α`, the function `f` is Big-O of the function `g(x) = u * f(x)` with respect to `l`, where the constant of the Big-O notation is the norm of the inverse of `u`. In other words, the norm of `f` is eventually bounded by the norm of the inverse of `u` times the norm of `g(x) = u * f(x)` for values in the filter `l`.
More concisely: For any non-zero scalar `u` in a seminormed ring `R`, and for any function `f : α → R` and filter `l` on `α`, the norm of `f` is eventually dominated by the constant `(|u|⁻¹ * |u| * |f|)` as `x` approaches elements in the filter `l`.
|
Asymptotics.IsBigO.abs_left
theorem Asymptotics.IsBigO.abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
u =O[l] g → (fun x => |u x|) =O[l] g
This theorem, `Asymptotics.IsBigO.abs_left`, is an alias for the reverse direction of `Asymptotics.isBigO_abs_left`. It states that, given any two functions `u` and `g` from a type `α` to a normed field `F` and `Real numbers` respectively, and a filter `l` on `α`, if `u` is Big O of `g` at `l` , then the function which takes each `x` in `α` to the absolute value of `u(x)`, is also Big O of `g` at `l`. This theorem allows us to infer asymptotic tight bounds on the absolute value of a function based on its Big O relation to another function.
More concisely: If `u` is Big O of `g` at filter `l`, then the absolute value function of `u` is also Big O of `g` at `l`.
|
Asymptotics.IsLittleO.abs_right
theorem Asymptotics.IsLittleO.abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
f =o[l] u → f =o[l] fun x => |u x|
This theorem, `Asymptotics.IsLittleO.abs_right`, states that for any type `α` and a normed type `E`, given a function `f` from `α` to `E`, a filter `l` on `α`, and a function `u` from `α` to the real numbers ℝ, if `f` is little-o of `u` at the filter `l` (meaning that `f` grows no faster than `u` in the limit as `l`), then `f` is also little-o of the absolute value of `u` at the same filter. This theorem provides an alias of the reverse direction of `Asymptotics.isLittleO_abs_right`.
More concisely: If `f : α → E` is little-o of `u : α → ℝ` at filter `l` on `α`, then `f` is also little-o of the absolute value of `u` at `l`.
|
Asymptotics.IsLittleO.tendsto_div_nhds_zero
theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
f =o[l] g → Filter.Tendsto (fun x => f x / g x) l (nhds 0)
The theorem `Asymptotics.IsLittleO.tendsto_div_nhds_zero` states that for any type `α`, a normed division ring `𝕜`, a filter `l` on `α`, and functions `f` and `g` from `α` to `𝕜`, if `f` is little-o of `g` at filter `l` (which means the ratio of `f` to `g` tends to zero when values are taken close to the points specified by the filter `l`), then the function that takes `x` to `f(x)/g(x)` tends to zero in the neighborhood filter at zero. This theorem essentially says that if `f` is much smaller than `g` near the points defined by `l`, then the ratio `f/g` tends to zero in the neighborhood of zero.
More concisely: If a function `f` is little-o of `g` at filter `l` on type `α`, then the quotient function `x ⟩‐⟩ 0 => f x / g x` tends to zero in the neighborhood filter at zero in a normed division ring `𝕜`.
|
Asymptotics.IsLittleO.forall_isBigOWith
theorem Asymptotics.IsLittleO.forall_isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g
This theorem states that for two functions `f` and `g` on a type `α` with a filter `l` and for every real number `c` greater than zero, if `f` is little-o of `g` at `l` (denoted `f =o[l] g`), then `f` is also Big-O of `g` at `l` with constant `c` (denoted `Asymptotics.IsBigOWith c l f g`). In simpler terms, this means that if the function `f` eventually grows no faster than `g` for the filter `l`, then we can find a constant `c` such that `f` is bounded by `c * g` under the same conditions.
More concisely: If `f =o[l] g` (little-o) then there exists a constant `c` such that `Asymptotics.IsBigOWith c l f g` (Big-O).
|
Asymptotics.IsBigOWith.of_norm_left
theorem Asymptotics.IsBigOWith.of_norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ}
{g : α → F} {f' : α → E'} {l : Filter α},
Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g → Asymptotics.IsBigOWith c l f' g
The theorem `Asymptotics.IsBigOWith.of_norm_left` states that for any real number `c`, any type `α`, any functions `f'` and `g` from `α` to a normed space `F` and a seminormed add commutative group `E'` respectively, and any filter `l` on `α`, if the norm of `f'` is Big-O of `g` with respect to `c` and `l` (i.e., the norm of `f'` is eventually bounded by `c` times the norm of `g`), then `f'` itself is also Big-O of `g` with respect to `c` and `l`. In other words, if `‖f'‖ / ‖g‖` is eventually bounded by `c` (modulo division by zero), then `f' / g` is also eventually bounded by `c`, again modulo division by zero issues.
More concisely: If the norm of a function `f'` is Big-O of another function `g` with respect to a constant `c` and a filter `l`, then `f'` is also Big-O of `g` with respect to `c` and `l`.
|
Asymptotics.isLittleO_iff_tendsto'
theorem Asymptotics.isLittleO_iff_tendsto' :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
(∀ᶠ (x : α) in l, g x = 0 → f x = 0) → (f =o[l] g ↔ Filter.Tendsto (fun x => f x / g x) l (nhds 0))
The theorem `Asymptotics.isLittleO_iff_tendsto'` states that for any types `α` and `𝕜`, where `𝕜` is a normed division ring, along with a filter `l` on `α` and two functions `f`, `g` from `α` to `𝕜`, given that whenever `g(x)` is zero for some `x` in the neighborhood defined by filter `l`, `f(x)` is also zero, then `f` is little-o of `g` at the filter `l` if and only if the function that sends `x` to `f(x)/g(x)` tends to 0 at the filter `l`.
In other words, `f` is dominated by `g` at the filter `l` (i.e., `f` is little-o of `g`) if and only if the ratio `f(x)/g(x)` approaches 0 as `x` approaches a point in the neighborhood defined by filter `l`, under the condition that `f(x)` is zero whenever `g(x)` is zero.
More concisely: For functions `f` and `g` from a type `α` to a normed division ring `𝕜`, `f` is little-o of `g` at filter `l` if and only if the quotient `f(x)/g(x)` converges to 0 at filter `l`, provided `f(x) = 0` whenever `g(x) = 0`.
|
Asymptotics.isBigOWith_const_mul_self
theorem Asymptotics.isBigOWith_const_mul_self :
∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] (c : R) (f : α → R) (l : Filter α),
Asymptotics.IsBigOWith ‖c‖ l (fun x => c * f x) f
The theorem `Asymptotics.isBigOWith_const_mul_self` states that for any seminormed ring `R`, a constant `c` in `R`, a function `f` from a generic type `α` to `R`, and a filter `l` on `α`, the function `c * f` is big-O of `f` with respect to the filter `l` and the constant factor `‖c‖`. In other words, the values of `c * f` are eventually bounded by `‖c‖ * ‖f‖` for the filter `l`. This means that the growth rate of the function `c * f` is at most as fast as the function `f`, up to a constant factor of `‖c‖`.
More concisely: For any seminormed ring `R`, constant `c` in `R`, function `f` from a type `α` to `R`, and filter `l` on `α`, `c * f` is big-O of `f` with constant factor `‖c‖` with respect to the filter `l`.
|
Asymptotics.IsLittleO.of_isBigOWith
theorem Asymptotics.IsLittleO.of_isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, (∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g) → f =o[l] g
The theorem `Asymptotics.IsLittleO.of_isBigOWith` states that for any types `α`, `E`, and `F` with the latter two possessing a norm, and for any functions `f : α → E` and `g : α → F` with a given filter `l` on `α`, if for all real numbers `c` greater than 0, `f` is big-O of `g` within `c` and `l` (i.e., the norm of `f` is eventually bounded by `c` times the norm of `g`), then `f` is little-o of `g` at `l`. In other words, `f` grows no faster than `g` at `l`.
More concisely: If for all `c > 0`, the norm of `f(x)` is eventually bounded by `c` times the norm of `g(x)` for all `x` in a filter `l` on `α`, then `f` is little-o of `g` at `l`.
|
Asymptotics.IsLittleO_def
theorem Asymptotics.IsLittleO_def :
∀ {α : Type u_17} {E : Type u_18} {F : Type u_19} [inst : Norm E] [inst_1 : Norm F] (l : Filter α) (f : α → E)
(g : α → F), f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.IsLittleO_def` states that for any types `α`, `E`, and `F`, with `E` and `F` having a norm, and any filter `l` on `α`, and any functions `f : α → E` and `g : α → F`, the function `f` is little o of `g` with respect to the filter `l` (notated as `f =o[l] g`) if and only if for any positive real number `c`, `f` is Big O of `g` with respect to the filter `l` and constant `c` (notated as `Asymptotics.IsBigOWith c l f g`). In other words, `f` is little o of `g` if `f` is eventually bounded by `c * g` for every positive `c`, modulo issues of division by zero.
More concisely: For types `α`, `E`, and `F` with normed functions `f : α → E` and `g : α → F`, `f` is little o of `g` with respect to filter `l` if and only if for every `c > 0`, `f` is Big O of `cg` with respect to `l`.
|
Asymptotics.IsBigO.pow
theorem Asymptotics.IsBigO.pow :
∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
{l : Filter α} {f : α → R} {g : α → 𝕜}, f =O[l] g → ∀ (n : ℕ), (fun x => f x ^ n) =O[l] fun x => g x ^ n
This theorem, `Asymptotics.IsBigO.pow`, states that for any types `α`, `R`, `𝕜`, with `R` being a seminormed ring and `𝕜` a normed division ring, and any filter `l` and functions `f : α → R` and `g : α → 𝕜`, if `f` is Big O of `g` at filter `l` (meaning the absolute value of `f` is eventually less than or equal to some constant multiple of `g`), then for any natural number `n`, the function that maps `x` to `f(x)^n` is also Big O of the function that maps `x` to `g(x)^n` at the same filter `l`. This essentially says that the Big O property is preserved under exponentiation.
More concisely: For functions `f : α → R` and `g : α → 𝕜`, if `f` is Big O of `g` at filter `l` in the seminormed ring `R` and normed division ring `𝕜`, then `f^n` is Big O of `g^n` at `l` for any natural number `n`.
|
Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.26
theorem Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.26 :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =O[l] g = f' =O[l] g
This theorem states that for any types `α`, `F`, and `E'`, with `F` having a norm and `E'` being a seminormed addititive commutative group, and given a function `g` from `α` to `F` and another function `f'` from `α` to `E'`, and a filter `l` on `α`, the big O notation of the norm of `f'` with respect to `g` at the filter `l` is equal to the big O notation of `f'` with respect to `g` at the same filter `l`. In other words, when considering asymptotic behavior, taking the norm of the function `f'` does not change the order of growth when compared to `g`.
More concisely: For functions `g : α → F` with `F` having a norm, `f' : α → E'` with `(E', ±)|.|)` a seminormed additive commutative group, and filter `l` on `α`, the big O notation of `|f'|` with respect to `g` at `l` equals the big O notation of `f'` with respect to `g` at `l`.
|
Asymptotics.IsBigOWith.of_norm_norm
theorem Asymptotics.IsBigOWith.of_norm_norm :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : 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'
The theorem `Asymptotics.IsBigOWith.of_norm_norm` is an alias of the forward direction of `Asymptotics.isBigOWith_norm_norm`. This theorem states that for any types `α`, `E'`, and `F'`, with `α` being a filter, and `E'` and `F'` being seminormed add commutative groups, and any real number `c`, if the function `|f'(x)|` is big O of `|g'(x)|` in the sense of Landau notation `IsBigOWith` (that is, if the absolute value of `f'` is eventually bounded by `c` times the absolute value of `g'`), then the function `f'(x)` itself is also big O of `g'(x)` in the same sense. In other words, if `f'` behaves similarly to `g'` when considering their absolute values, then `f'` behaves similarly to `g'` without the need to consider absolute values.
More concisely: If `|f'(x)|` is big O of `|g'(x)|` in the sense of Landau notation, then `f'(x)` is also big O of `g'(x)` in the same sense.
|
Asymptotics.isLittleO_zero
theorem Asymptotics.isLittleO_zero :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] (g' : α → F') (l : Filter α), (fun _x => 0) =o[l] g'
This theorem states that for any types `α`, `E'`, and `F'`, where `E'` and `F'` are seminormed additive commutative groups, and any function `g'` from `α` to `F'`, and any filter `l` on `α`, the function that is constantly zero is little-o of `g'` at `l`. In simpler terms, as we get closer to the limit `l`, the values of the function `g'` grow much faster than the constant function that always equals zero. This is a fundamental concept in asymptotic analysis.
More concisely: For any seminormed additive commutative groups `E'` and `F'`, function `g': α → F'`, and filter `l` on `α`, if for all `ε > 0`, there exists a `δ > 0` such that `∀x, y ∈ α`, `x ∈ l`, `d(x, y) < δ` implies `∥g'(x) - g'(y)∥ < ε`, then `0` is little-o of `g'` at `l`.
|
Asymptotics.IsBigO.mul_isLittleO
theorem Asymptotics.IsBigO.mul_isLittleO :
∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
{l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜},
f₁ =O[l] g₁ → f₂ =o[l] g₂ → (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
This theorem states that for any types `α`, `R`, and `𝕜` (with `R` being a seminormed ring and `𝕜` a normed division ring), and for any filter `l`, if function `f₁` is big-O of `g₁` under filter `l` and `f₂` is little-o of `g₂` under the same filter, then the function that maps `x` to the product of `f₁(x)` and `f₂(x)` is also little-o of the function that maps `x` to the product of `g₁(x)` and `g₂(x)`. This theorem is a statement about asymptotic behavior of function multiplication under certain norms.
More concisely: If $f\_1$ is big-O of $g\_1$ and $f\_2$ is little-o of $g\_2$ under filter $l$ in the seminormed ring $(R, ||\_.||)$ and normed division ring $(𝕜, ||\_.||)$, then $f\_1 \cdot f\_2$ is little-o of $g\_1 \cdot g\_2$ under filter $l$.
|
Asymptotics.IsLittleO.const_mul_left
theorem Asymptotics.IsLittleO.const_mul_left :
∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {g : α → F}
{l : Filter α} {f : α → R}, f =o[l] g → ∀ (c : R), (fun x => c * f x) =o[l] g
This theorem states that for any types `α`, `F`, and `R`, with `F` being a normed type and `R` a semi-normed ring, and for any functions `f : α → R` and `g : α → F` that are asymptotically equivalent at a filter `l`, the asymptotic equivalence remains when `f` is multiplied by a constant `c` from `R`. In simpler words, if `f` and `g` grow at the same rate, then scaling `f` by a constant does not change its growth rate relative to `g`.
More concisely: If `f : α → R`, `g : α → F`, `α` is any type, `F` is a normed type, `R` is a semi-normed ring, `l` is a filter, and `f` and `g` are asymptotically equivalent at `l`, then `cf` and `g` are asymptotically equivalent at `l` for any constant `c` from `R`.
|
Asymptotics.IsBigO.sub
theorem Asymptotics.IsBigO.sub :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → f₂ =O[l] g → (fun x => f₁ x - f₂ x) =O[l] g
This theorem, `Asymptotics.IsBigO.sub`, is stating a property about Big O notation in the context of limits in functional analysis. Specifically, it states that for any types `α`, `F`, and `E'` where `F` is a normed space and `E'` is a semi-normed additive commutative group, and for any function `g : α → F` and filter `l : Filter α` and functions `f₁, f₂ : α → E'`, if `f₁ =O[l] g` and `f₂ =O[l] g` (that is, `f₁` and `f₂` are Big O of `g` with respect to the filter `l`), then the function `(fun x => f₁ x - f₂ x)` (which represents the pointwise difference of `f₁` and `f₂`) is also Big O of `g` with respect to the filter `l`. That is, if two functions are both bounded by the same function in the limit, then their difference is also bounded by that same function in the limit.
More concisely: If functions `f₁` and `f₂` are both Big O of `g` with respect to filter `l` in the context of functional analysis, then their pointwise difference `(x mapsto f₁ x - f₂ x)` is also Big O of `g` with respect to `l`.
|
Asymptotics.IsLittleO.of_norm_norm
theorem Asymptotics.IsLittleO.of_norm_norm :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α},
((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) → f' =o[l] g'
This theorem, `Asymptotics.IsLittleO.of_norm_norm`, is an alias for the forward direction of the theorem `Asymptotics.isLittleO_norm_norm`. In simple terms, it states that if, for all `α` of some type, and for all `E'` and `F'` of certain seminormed add commutative group types, and given functions `f'` and `g'` from `α` to `E'` and `F'` respectively, and a filter `l` on `α`, if the norm of `f'` is little-o of the norm of `g'` at filter `l` (i.e., the norm of `f'` tends to zero faster than the norm of `g'` as `l` goes to infinity), then the function `f'` itself is little-o of `g'` at filter `l`.
More concisely: If the norm of a function is little-o of the norm of another function with respect to a filter, then the first function is little-o of the second function with respect to that filter.
|
Asymptotics.IsLittleO.right_isBigO_add
theorem Asymptotics.IsLittleO.right_isBigO_add :
∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'},
f₁ =o[l] f₂ → f₂ =O[l] fun x => f₁ x + f₂ x
This theorem states that for all types `α` and `E'`, with `E'` being a seminormed additive commutative group, and for all filters `l` and functions `f₁` and `f₂` from `α` to `E'`, if `f₁` is little-o of `f₂` at filter `l` (meaning that `f₁` grows asymptotically slower than `f₂` as they approach the limit points of the filter), then `f₂` is Big-O of `f₁ + f₂` at filter `l` (meaning that the growth rate of `f₂` is bounded above by the growth rate of `f₁ + f₂`). In short, it expresses a certain relative growth rate condition between two functions in the context of asymptotic analysis.
More concisely: If `f₁` is little-o of `f₂` at filter `l` in the seminormed additive commutative group `E'` over type `α`, then `f₂` is Big-O of `f₁ + f₂` at filter `l`.
|
Asymptotics.isBigO_iff
theorem Asymptotics.isBigO_iff :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
The theorem `Asymptotics.isBigO_iff` states that for any types `α`, `E`, and `F`, and for any functions `f : α → E` and `g : α → F`, given a filter `l` on `α`, the statement "function `f` is Big O of function `g` at filter `l`" is equivalent to the existence of a constant `c` such that, eventually for every `x` in filter `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`. This is a formal description of the concept of Big O notation in terms of filters and norms in the context of Asymptotic analysis.
More concisely: For functions `f : α → E` and `g : α → F` over type `α`, and filter `l` on `α`, the functions `f` is Big O of `g` at `l` if and only if there exists a constant `c` such that, for all `x` in `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`.
|
Asymptotics.isBigO_iff_eventually
theorem Asymptotics.isBigO_iff_eventually :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =O[l] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖
The theorem `Asymptotics.isBigO_iff_eventually` states that, for a given pair of functions `f` and `g'` mapping from an arbitrary type `α` to normed type `E` and semi-normed additive commutative group `F'` respectively, and for a given filter `l` over `α`, `f` is Big O of `g'` at `l` if and only if for all real numbers `c` that are sufficiently large, eventually for all `x` in `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g'(x)`. In other words, `f` is bounded above by a multiple of `g'` for all `c` large enough and for all `x` in `l` eventually. The term "eventually" here refers to the condition being true for all `x` beyond a certain point in `l`, and "sufficiently large" means that the condition holds for all `c` beyond some threshold.
More concisely: For functions `f : α → E` and `g' : α → F'` mapping from type `α` to a normed type `E` and semi-normed additive commutative group `F'` respectively, `f` is Big O of `g'` at filter `l` if and only if for all sufficiently large `c`, there exists a point `x` in `l` such that the norm of `f(x)` is less than or equal to `c` times the norm of `g'(x)`.
|
Asymptotics.IsBigOWith.neg_right
theorem Asymptotics.IsBigOWith.neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
Asymptotics.IsBigOWith c l f g' → Asymptotics.IsBigOWith c l f fun x => -g' x
This theorem, `Asymptotics.IsBigOWith.neg_right`, states that for given types `α`, `E`, and `F'` where `α` is the domain upon which the functions `f` and `g'` operate, `E` is the codomain of `f`, and `F'` is a seminormed additive commutative group representing the codomain of `g'`, along with a real number `c`, a filter `l` on `α`, if the function `f` is big O of `g'` with constant `c` at filter `l` (denoted as `Asymptotics.IsBigOWith c l f g'`), then `f` is also big O of the negation of `g'` (i.e., `-g'`) with the same constant `c` at the same filter `l`. In simpler terms, if `f` grows no faster than `g'` up to a constant factor, then `f` also grows no faster than `-g'` up to the same constant factor.
More concisely: If `f` is big O of `g'` with constant `c` at filter `l`, then `f` is also big O of `-g'` with constant `c` at filter `l`.
|
Asymptotics.IsLittleO.norm_right
theorem Asymptotics.IsLittleO.norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =o[l] g' → f =o[l] fun x => ‖g' x‖
The theorem `Asymptotics.IsLittleO.norm_right` is an alias of the reverse direction of `Asymptotics.isLittleO_norm_right`. In terms of mathematics, it states that for any types `α`, `E`, and `F'`, given a norm on `E` and a seminormed additive commutative group on `F'`, for any functions `f : α → E` and `g' : α → F'`, and any filter `l` on `α`, if `f` is little-o of `g'` at `l` (that is, `f` grows slower than `g'` when approaching the limit `l`), then `f` is also little-o of `||g'||` at `l` (that is, `f` grows slower than the norm of `g'` when approaching the limit `l`).
More concisely: Given functions `f : α → E` and `g' : α → F'`, a norm on `E`, a seminormed additive commutative group on `F'`, and a filter `l` on `α`, if `f` is little-o of `g'` at `l`, then `f` is also little-o of `||g'||` at `l`.
|
Asymptotics.IsBigO.of_neg_left
theorem Asymptotics.IsBigO.of_neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => -f' x) =O[l] g → f' =O[l] g
This theorem, `Asymptotics.IsBigO.of_neg_left`, states that for all types `α`, `F`, and `E'`, given any normed field `F`, any semi-normed addition commutative group `E'`, any functions `g` and `f'` from `α` to `F` and `E'` respectively, and any filter `l` on `α`, if the function that negates every output of `f'` is a big-O of `g` at filter `l`, then `f'` itself is a big-O of `g` at filter `l`. In terms of Asymptotic notation, this means that if `-f'(x)` is O(g) as x approaches `l`, then `f'(x)` is also O(g).
More concisely: If the negation of a function `f'` is big-O of `g` as `x` approaches filter `l`, then `f'` is also big-O of `g` as `x` approaches `l`. (In the context of asymptotic notation, this means that `f'(x)` is O(`g(x)`) as `x` goes to `l` if and only if `-f'(x)` is O(`g(x)`).)
|
Asymptotics.IsBigO.of_bound
theorem Asymptotics.IsBigO.of_bound :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α} (c : ℝ), (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → f =O[l] g
The theorem `Asymptotics.IsBigO.of_bound` states that for every function `f` from a type `α` to a normed space `E`, and every function `g` from `α` to another normed space `F`, if for almost all `x` in a certain filter `l`, the norm of `f(x)` is less than or equal to a real constant `c` times the norm of `g(x)`, then `f` is Big O of `g` at this filter. In other words, `f` grows no faster than `g` up to a constant factor, for values `x` from the filter `l`. This is a formal, rigorous way to describe asymptotic upper bounds in the language of mathematical analysis.
More concisely: If for almost all x in a filter l, the norm of f(x) is bounded above by a constant c times the norm of g(x), then f is Big O of g at filter l.
|
Asymptotics.IsBigOWith.neg_left
theorem Asymptotics.IsBigOWith.neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ}
{g : α → F} {f' : α → E'} {l : Filter α},
Asymptotics.IsBigOWith c l f' g → Asymptotics.IsBigOWith c l (fun x => -f' x) g
The theorem `Asymptotics.IsBigOWith.neg_left` is an alias for the reverse direction of `Asymptotics.isBigOWith_neg_left` and states the following: Given the types `α`, `F`, `E'`, a filter `l` on `α`, two functions `f'` and `g` from `α` to `E'` and `F` respectively, and a real number `c`, if `f'` is "big O" of `g` with respect to `l` and the factor `c` (i.e., the norm of `f'` is eventually bounded by `c` times the norm of `g` as per the definition of `Asymptotics.IsBigOWith`), then the negation of the function `f'` (i.e., the function that to each `x` assigns `-f'(x)`) is also "big O" of `g` with the same respect to `l` and the factor `c`. This theorem essentially states that the "big O" relation is preserved under taking the negation of the function.
More concisely: If `f` is big O of `g` with respect to filter `l` and constant `c`, then the negation of `f` is big O of `g` with respect to `l` and `c`.
|
Asymptotics.isBigOWith_norm_left
theorem Asymptotics.isBigOWith_norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ}
{g : α → F} {f' : α → E'} {l : Filter α},
Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g ↔ Asymptotics.IsBigOWith c l f' g
The theorem `Asymptotics.isBigOWith_norm_left` states that for any type `α`, any normed type `F`, any semi-normed add commutative group `E'`, any real number `c`, any function `g` mapping from `α` to `F`, any function `f'` mapping from `α` to `E'`, and any filter `l` on `α`, the assertion that `f'` is `O(g)` with constant `c` with respect to the filter `l` when we take the norm of `f'`, is equivalent to the assertion that `f'` is `O(g)` with constant `c` with respect to the filter `l` without taking the norm. In mathematical terms, it means that $\|f'\| = O(g)$ if and only if $f' = O(g)$, where $O$ denotes the Big O notation, which describes an upper bound of one function in terms of another.
More concisely: For any type `α`, normed type `F`, semi-normed add commutative group `E'`, real number `c`, functions `g : α → F` and `f' : α → E'`, and filter `l` on `α`, the condition `\|f'\| = O(g)` with constant `c` with respect to `l` is equivalent to `f' = O(g)` with constant `c` with respect to `l`.
|
Asymptotics.IsBigOWith.congr
theorem Asymptotics.IsBigOWith.congr :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {l : Filter α}
{f₁ f₂ : α → E} {g₁ g₂ : α → F},
Asymptotics.IsBigOWith c₁ l f₁ g₁ →
c₁ = c₂ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → Asymptotics.IsBigOWith c₂ l f₂ g₂
The theorem `Asymptotics.IsBigOWith.congr` states that for any two real numbers `c₁` and `c₂`, any two functions `f₁` and `f₂` from a type `α` to a normed type `E`, and any two functions `g₁` and `g₂` from `α` to another normed type `F`, if `f₁` is Big-O of `g₁` with respect to the filter `l` and the constant `c₁`, and if `c₁` equals `c₂`, `f₁` equals `f₂` for all `x` in `α`, and `g₁` equals `g₂` for all `x` in `α`, then `f₂` is also Big-O of `g₂` with respect to the filter `l` and the constant `c₂`. In other words, Big-O notation is congruent with respect to the constants and the functions involved.
More concisely: If `f₁` is Big-O of `g₁` with respect to filter `l` and constant `c₁`, `c₁ = c₂`, `f₁ = f₂`, and `g₁ = g₂` hold for all `x` in `α`, then `f₂` is Big-O of `g₂` with respect to filter `l` and constant `c₂`.
|
Asymptotics.IsLittleO.trans
theorem Asymptotics.IsLittleO.trans :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
{l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =o[l] g → g =o[l] k → f =o[l] k
This theorem states that given three functions `f`, `g`, and `k` that map from some type `α` to types `E`, `F`, and `G` respectively (all of which are equipped with a norm), and given a filter `l` on `α`, if `f` is little-o of `g` at filter `l` and `g` is little-o of `k` at filter `l`, then `f` is also little-o of `k` at filter `l`. In terms of asymptotic notation, if f = o(g) and g = o(k) under the filter `l`, then f = o(k) under the same filter. This establishes the transitivity property of the little-o notation.
More concisely: If `f = o(g)` and `g = o(k)` for functions `f: α -> E`, `g: α -> F`, and `k: α -> G` under filter `l` on type `α`, then `f = o(k)` under the same filter.
|
Asymptotics.IsBigOWith.congr_left
theorem Asymptotics.IsBigOWith.congr_left :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {g : α → F} {l : Filter α}
{f₁ f₂ : α → E}, Asymptotics.IsBigOWith c l f₁ g → (∀ (x : α), f₁ x = f₂ x) → Asymptotics.IsBigOWith c l f₂ g
The theorem `Asymptotics.IsBigOWith.congr_left` states that for any types `α`, `E`, and `F`, where `E` and `F` are equipped with a norm, a real number `c`, a function `g` from `α` to `F`, a filter `l` on `α`, and two functions `f₁` and `f₂` from `α` to `E`, if `f₁` is Big-O of `g` with constant `c` with respect to filter `l` (i.e., `Asymptotics.IsBigOWith c l f₁ g` holds), and every element of `α` is mapped to the same value by `f₁` and `f₂`, then `f₂` is also Big-O of `g` with the same constant `c` with respect to the same filter `l`. In other words, the Big-O relation is preserved under pointwise equality of the functions involved.
More concisely: If `f₁` is Big-O of `g` with constant `c` with respect to filter `l` and `f₁` and `f₂` agree pointwise, then `f₂` is also Big-O of `g` with constant `c` with respect to `l`.
|
Asymptotics.isLittleO_abs_right
theorem Asymptotics.isLittleO_abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
(f =o[l] fun x => |u x|) ↔ f =o[l] u
The theorem `Asymptotics.isLittleO_abs_right` states that for any types `α` and `E`, where `E` has a norm, and for any functions `f : α → E`, `u : α → ℝ`, and a filter `l` on `α`, `f` is little o of `|u x|` with respect to `l` if and only if `f` is little o of `u` with respect to `l`. In mathematical notation, this is saying $f(x) = o(|u(x)|)$ if and only if $f(x) = o(u(x))$.
More concisely: For functions `f : α → E` and `u : α → ℝ` on type `α`, where `E` has a norm, `f` is little o of `|u x|` with respect to a filter `l` if and only if `f` is little o of `u` with respect to `l`, i.e., $f(x) = o(|u(x)|)_l$ if and only if $f(x) = o(u(x))_l$.
|
Asymptotics.IsBigO.congr'
theorem Asymptotics.IsBigO.congr' :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
{g₁ g₂ : α → F}, f₁ =O[l] g₁ → l.EventuallyEq f₁ f₂ → l.EventuallyEq g₁ g₂ → f₂ =O[l] g₂
The theorem `Asymptotics.IsBigO.congr'` states that for any types `α`, `E`, and `F`, given the norms on `E` and `F`, a filter `l` on `α`, and functions `f₁`, `f₂` from `α` to `E`, and `g₁`, `g₂` from `α` to `F`, if `f₁` is Big O of `g₁` at filter `l` (`f₁ =O[l] g₁`), `f₁` is eventually equal to `f₂` at filter `l` (`f₁ =ᶠ[l] f₂`), and `g₁` is eventually equal to `g₂` at filter `l` (`g₁ =ᶠ[l] g₂`), then `f₂` is Big O of `g₂` at filter `l` (`f₂ =O[l] g₂`). In simpler terms, it means that if two pairs of functions are asymptotically equivalent and the functions within each pair are eventually equal, then the resulting pairs of functions are also asymptotically equivalent.
More concisely: If functions `f₁` and `g₁`, as well as `f₂` and `g₂`, are related by `f₁ =O[l] g₁`, `f₁ =ᶠ[l] f₂`, and `g₁ =ᶠ[l] g₂` for a filter `l` and types `α`, `E`, and `F`, then `f₂ =O[l] g₂`.
|
Asymptotics.IsLittleO.norm_left
theorem Asymptotics.IsLittleO.norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, f' =o[l] g → (fun x => ‖f' x‖) =o[l] g
This is an alias for the reverse direction of the `Asymptotics.isLittleO_norm_left` theorem. For all types `α`, `F`, and `E'`, where `F` has a norm and `E'` is a semi normed additive commutative group, and given functions `g : α → F` and `f' : α → E'`, and a filter `l` on `α`, if `f'` is little 'o' of `g` at `l` (i.e., `f'` is asymptotically smaller than `g` as we approach the limit `l`), then the function `x => ‖f' x‖` (which takes `x` to the norm of `f'(x)`) is also little 'o' of `g` at `l`.
More concisely: If `f'` is little-o of `g` at filter `l`, then the function `x => ||f'(x)||` is also little-o of `g` at `l`, for all types `α`, `F` with norm, and `E'` a semi-normed additive commutative group.
|
Asymptotics.isBigO_zero_right_iff
theorem Asymptotics.isBigO_zero_right_iff :
∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F']
[inst_1 : NormedAddCommGroup E''] {f'' : α → E''} {l : Filter α},
(f'' =O[l] fun _x => 0) ↔ l.EventuallyEq f'' 0
The theorem `Asymptotics.isBigO_zero_right_iff` states that for any types `α`, `F'`, and `E''`, where `F'` is a seminormed commutative additive group and `E''` is a normed commutative additive group, and for any function `f''` from `α` to `E''` and any filter `l` on `α`, it is the case that `f''` is Big O of zero with respect to `l` if and only if `f''` equals zero almost everywhere with respect to `l`. In mathematical terms, it means that a function is asymptotically negligible (i.e., it becomes arbitrarily small as its argument approaches some limit) if and only if it is essentially zero around that limit.
More concisely: A function from a type to a normed commutative additive group is Big O of zero with respect to a filter on the domain if and only if it equals zero almost everywhere with respect to that filter.
|
Asymptotics.isBigO_fst_prod
theorem Asymptotics.isBigO_fst_prod :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α}, f' =O[l] fun x => (f' x, g' x)
The theorem `Asymptotics.isBigO_fst_prod` in Lean 4 states that for any types `α`, `E'`, and `F'`, where `E'` and `F'` are both seminormed add commutative groups, and given any functions `f': α → E'` and `g': α → F'`, and a filter `l` on `α`, the function `f'` is Big-O of the function that maps `x` to the pair `(f'(x), g'(x))` when evaluated on the filter `l`. In terms of asymptotics, this means that `f'` grows no faster than the function mapping `x` to `(f'(x), g'(x))`.
More concisely: For functions `f:` α -> E' and `g:` α -> F' on a type α with seminormed add commutative groups E' and F', and a filter l on α, the function f is Big-O of the function x mapsto (f x, g x) when evaluated on filter l.
|
Asymptotics.IsBigO.eq_zero_imp
theorem Asymptotics.IsBigO.eq_zero_imp :
∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E'']
[inst_1 : NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α},
f'' =O[l] g'' → ∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0
This theorem states that for any types `α`, `E''`, and `F''`, with `E''` and `F''` being normed additively commutative groups, and any functions `f''` from `α` to `E''` and `g''` from `α` to `F''`, and any filter `l` on `α`, if `f''` is big O of `g''` at the points approaching through the filter `l`, then whenever `g''` equals zero at a point in the filter `l`, `f''` will also equal zero at that point. In other words, if function `f''` grows no faster than `g''` near the points determined by the filter `l`, and if `g''` is zero at some of those points, then `f''` must be zero at those points too.
More concisely: If `f: α -> E` and `g: α -> F` are functions from a type `α` to normed additively commutative groups `E` and `F`, respectively, and `f` is big O of `g` at the points approaching through filter `l`, then for any point `x in α` where `g(x) = 0`, it follows that `f(x) = 0`.
|
Asymptotics.isBigO_norm_right
theorem Asymptotics.isBigO_norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'
This theorem, `Asymptotics.isBigO_norm_right`, states that for any types `α`, `E`, and `F'`, where `E` has a norm structure and `F'` has a seminormed additive commutative group structure, and given any functions `f : α → E` and `g' : α → F'`, and a filter `l` on `α`, the function `f` is big-O of the norm of `g'` at filter `l` if and only if `f` is big-O of `g'` at filter `l`. In other words, the big-O notation holds the same for a function and its normed version with respect to a specific filter.
More concisely: For functions `f : α → E` and `g' : α → F'` between normed spaces `E` and seminormed additive commutative groups `F'`, and filter `l` on `α`, `f` is big-O of the norm of `g'` at filter `l` if and only if `f` is big-O of `g'` at filter `l`.
|
Asymptotics.IsBigOWith.congr_const
theorem Asymptotics.IsBigOWith.congr_const :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {f : α → E} {g : α → F}
{l : Filter α}, Asymptotics.IsBigOWith c₁ l f g → c₁ = c₂ → Asymptotics.IsBigOWith c₂ l f g
The theorem `Asymptotics.IsBigOWith.congr_const` states that for any two real constants `c₁` and `c₂`, two functions `f` and `g` on a type `α`, and a filter `l` on `α`, if `f` is Big-O of `g` with constant `c₁` at the filter `l` (i.e., `Asymptotics.IsBigOWith c₁ l f g` holds), and if `c₁` equals `c₂`, then `f` is also Big-O of `g` with constant `c₂` at the filter `l`. In other words, the Big-O notation's constant can be replaced by an equal constant without changing the validity of the Big-O relationship. This theorem essentially reflects the principle that the Big-O notation is insensitive to the exact value of the constant as long as it remains the same.
More concisely: If `f` is Big-O of `g` with constant `c₁` at filter `l` in Lean, and `c₁` equals `c₂`, then `f` is also Big-O of `g` with constant `c₂` at filter `l`.
|
Asymptotics.IsLittleO.trans_isBigOWith
theorem Asymptotics.IsLittleO.trans_isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
{c : ℝ} {f : α → E} {g : α → F} {k : α → G} {l : Filter α},
f =o[l] g → Asymptotics.IsBigOWith c l g k → 0 < c → f =o[l] k
The theorem `Asymptotics.IsLittleO.trans_isBigOWith` states that for any types `α`, `E`, `F`, and `G` with instances of norms on `E`, `F`, and `G`, a real number `c`, functions `f : α → E`, `g : α → F`, and `k : α → G`, and a filter `l` on `α`, if `f` is little-o of `g` at `l` (meaning that `f` grows slower than `g` at `l`), and if `g` is Big-O of `k` at `l` with a constant factor `c` (meaning that `g` grows no faster than `c * k` at `l`), and if `c` is greater than zero, then `f` is little-o of `k` at `l`. In other words, it states that the little-o relation is transitive through the Big-O relation, under certain conditions. This conclusion allows us to compare the growth rates of functions at a specific point or sequence.
More concisely: If `f` is little-o of `g` at filter `l` and `g` is Big-O of `k` at `l` with constant factor `c > 0`, then `f` is little-o of `k` at `l`.
|
Asymptotics.isLittleO_one_iff
theorem Asymptotics.isLittleO_one_iff :
∀ {α : Type u_1} (F : Type u_4) {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {f' : α → E'}
{l : Filter α} [inst_2 : One F] [inst_3 : NormOneClass F],
(f' =o[l] fun _x => 1) ↔ Filter.Tendsto f' l (nhds 0)
This theorem, "Asymptotics.isLittleO_one_iff", states that for any type `α`, a type `F` with a norm, a type `E'` that forms a seminormed additive commutative group, a function `f'` from `α` to `E'`, and a filter `l` on `α`, with `F` having an element 'one' and a 'norm one' class, the function `f'` is little-o of one at the limit `l` (i.e., `f'` is dominated by the function returning one as `l` tends to infinity) if and only if the limit of `f'` as `l` tends to infinity is zero in the neighborhood filter at zero. In simpler terms, `f'` grows slower than the constant function 1 at `l` if and only if `f'` tends toward 0 as `l` tends toward infinity.
More concisely: For any type `α`, normed type `F`, seminormed additive commutative group `E'`, function `f': α → E'`, and filter `l` on `α`, the function `f'` is little-o of one at the limit `l` if and only if the limit of `f'` as `l` approaches infinity is zero in the neighborhood filter at zero.
|
Asymptotics.IsBigOWith.mul
theorem Asymptotics.IsBigOWith.mul :
∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
{l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c₂ : ℝ},
Asymptotics.IsBigOWith c₁ l f₁ g₁ →
Asymptotics.IsBigOWith c₂ l f₂ g₂ →
Asymptotics.IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
The theorem `Asymptotics.IsBigOWith.mul` states that for any two pairs of functions `(f₁, g₁)` and `(f₂, g₂)` over a type `α`, if `f₁` is "big O with constant `c₁`" of `g₁` with respect to a filter `l`, and `f₂` is "big O with constant `c₂`" of `g₂` with respect to the same filter `l`, then the function that maps `x` to the product `f₁(x) * f₂(x)` is "big O with constant `c₁ * c₂`" of the function that maps `x` to the product `g₁(x) * g₂(x)`, again with respect to the filter `l`. In other words, if each of the functions `f₁` and `f₂` grows no faster than their corresponding `g₁` and `g₂`, respectively, then the same is true for their products, with the new constant being the product of the original constants.
More concisely: If functions `f₁(x)` is big O of `g₁(x)` with constant `c₁` and `f₂(x)` is big O of `g₂(x)` with constant `c₂` with respect to filter `l`, then `f₁(x) * f₂(x)` is big O of `g₁(x) * g₂(x)` with constant `c₁ * c₂` with respect to `l`.
|
Asymptotics.IsBigO.mono
theorem Asymptotics.IsBigO.mono :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l l' : Filter α}, f =O[l'] g → l ≤ l' → f =O[l] g
This theorem, `Asymptotics.IsBigO.mono`, states that for all types `α`, `E`, and `F`, with `E` and `F` being normed, and for any functions `f : α → E` and `g : α → F`, along with two filters `l` and `l'` on `α`, if `f` is Big O of `g` at filter `l'` and `l` is less than or equal to `l'`, then `f` is also Big O of `g` at filter `l`. In layman's terms, this theorem is about the transitivity property in asymptotic notation: if a function `f` grows no faster than a function `g` at a certain rate (or filter), it will also grow no faster than `g` at any slower rate (or smaller filter).
More concisely: If `f` is Big O of `g` at filter `l'` and `l` ≤ `l'`, then `f` is also Big O of `g` at filter `l` in the normed types `α`, `E`, and `F`.
|
Asymptotics.IsBigO.congr_of_sub
theorem Asymptotics.IsBigO.congr_of_sub :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =O[l] g → (f₁ =O[l] g ↔ f₂ =O[l] g)
This theorem states that for any types `α`, `F`, and `E'`, given a norm on `F` and a seminormed add commutative group on `E'`, and given functions `g : α → F` and `f₁, f₂ : α → E'`, if `(f₁ - f₂)` is big-O of `g` (denoted as `(f₁ - f₂) =O[l] g`) with respect to a filter `l`, then `f₁` is big-O of `g` if and only if `f₂` is big-O of `g`. In other words, the big-O status of `f₁` and `f₂` relative to `g` is equivalent if `(f₁ - f₂)` is also big-O of `g` under the filter `l`. This concept is from asymptotic analysis, where a function f is Big-O of g if it grows no faster than g in the limit.
More concisely: If `(f₁ - f₂) =O[l] g` in Lean 4 with types `α`, `F`, and `E'`, normed group `F`, seminormed add commutative group `E'`, and functions `g : α → F`, `f₁, f₂ : α → E'`, then `f₁ =O[l] g` if and only if `f₂ =O[l] g`.
|
Asymptotics.IsBigO.eventually_mul_div_cancel
theorem Asymptotics.IsBigO.eventually_mul_div_cancel :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
u =O[l] v → l.EventuallyEq (u / v * v) u
This theorem states that for any Normed Division Ring `𝕜`, any Filter `l`, and any two functions `u` and `v` from `α` to `𝕜`, if `u` is Big O of `v` along `l` (written as `u =O[l] v`), then `(u / v) * v` is eventually equal to `u` at `l`. In other words, if `u` grows at the same rate as `v` or slower as we approach `l`, then we can cancel out `v` from the fraction `(u / v) * v` to get `u` after some point close to `l`.
More concisely: For any Normed Division Ring `𝕜`, if `u =O[l] v` for functions `u : α -> 𝕜` and `v : α -> 𝕜`, then `(u / v) * v` converges to `u` as `l` is approached.
|
Filter.Tendsto.isBigO_one
theorem Filter.Tendsto.isBigO_one :
∀ {α : Type u_1} (F : Type u_4) {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {f' : α → E'}
{l : Filter α} [inst_2 : One F] [inst_3 : NormOneClass F] {c : E'},
Filter.Tendsto f' l (nhds c) → f' =O[l] fun _x => 1
This theorem states that for any types `α`, `F`, `E'` with `F` being a normed space and `E'` being a semi-normed add commutative group, a function `f'` mapping from `α` to `E'`, a filter `l` on `α`, a `1` element in `F` that is a norm one class, and an element `c` in `E'`, if the function `f'` tends towards the neighborhood filter of `c` when `l` is mapped through `f'`, then `f'` is big O of the constant function `1` at filter `l`. In more mathematical terms, if the limit of `f'` as `l` goes to `c` exists, then `f'` is bounded by a constant times the function that is always `1` near `c`.
More concisely: If a function from a type to a semi-normed add commutative group tends towards a constant in a normed space as a filter on the domain converges, then the function is big O of the constant function 1 with respect to that filter.
|
Asymptotics.IsBigO.of_norm_right
theorem Asymptotics.IsBigO.of_norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =O[l] fun x => ‖g' x‖) → f =O[l] g'
This theorem is an alias for the forward direction of `Asymptotics.isBigO_norm_right`. It states that for any types `α`, `E`, and `F'`, if you have a normed space over `E`, a seminormed add commutative group over `F'`, and functions `f : α → E` and `g' : α → F'` with a filter `l` over `α`, if `f` is Big O of the norm of `g'` at filter `l` (written as `f =O[l] fun x => ‖g' x‖`), then `f` is also Big O of `g'` at the same filter (written as `f =O[l] g'`).
In simpler terms, it's saying if a function `f` grows at a rate no faster than the norm of another function `g'`, then `f` also grows at a rate no faster than `g'` itself.
More concisely: If a function `f : α → E` is Big O of the norm of another function `g' : α → F'` at filter `l` over `α`, then `f` is also Big O of `g'` at filter `l`.
|
Asymptotics.isBigO_iff_isBigOWith
theorem Asymptotics.isBigO_iff_isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =O[l] g ↔ ∃ c, Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.isBigO_iff_isBigOWith` states that, given two functions `f` and `g` mapping from a type `α` to normed types `E` and `F` respectively, and a filter `l` on `α`, `f` is of the same order of magnitude as `g` with respect to the filter `l` (denoted as `f =O[l] g`) if and only if there exists a real number `c` such that `f` is big O of `g` with a constant `c` concerning the filter `l`. In other words, the norm of `f` is eventually (at points in the filter `l`) bounded by `c` times the norm of `g`.
More concisely: For functions `f : α -> E` and `g : α -> F` mapping from a type `α` to normed types `E` and `F` respectively, and a filter `l` on `α`, `f` is of the same order of magnitude as `g` with respect to `l` if and only if there exists a constant `c` such that the norm of `f` is bounded by `c` times the norm of `g` at points in the filter `l`.
|
Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.59
theorem Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.59 :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {P : β → Prop},
(∀ᶠ (b : β) in Filter.map m f, P b) = ∀ᶠ (a : α) in f, P (m a)
This theorem, `Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.59`, states that for every type `α` and `β`, every filter `f` over `α`, every function `m` from `α` to `β`, and every predicate `P` over `β`, the property that for almost every `b` in the filter obtained by mapping `f` through `m`, `P` holds, is equivalent to the property that for almost every `a` in the filter `f`, `P` holds after applying `m` to `a`. In other words, the event of `P` happening "almost everywhere" in the mapped filter is identical to the event of `P` happening "almost everywhere" in the original filter, after the values are mapped.
More concisely: For every filter `f` over type `α`, function `m` from `α` to `β`, and predicate `P` over `β`, the property that for almost every `b` in `f.map m`, `P(b)` holds if and only if for almost every `a` in `f`, `P(m a)` holds.
|
Asymptotics.isBigO_self_const_mul'
theorem Asymptotics.isBigO_self_const_mul' :
∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {c : R},
IsUnit c → ∀ (f : α → R) (l : Filter α), f =O[l] fun x => c * f x
This theorem states that for any type `α`, any seminormed ring `R`, any element `c` of `R` that is a unit (i.e., has a multiplicative inverse), any function `f` from `α` to `R`, and for any filter `l` on `α`, `f` is "big O" of `c * f` at the filter `l`. In terms of asymptotic analysis, this means that `f` grows no faster than `c * f` under the filter `l`, considering `c` as a constant factor.
More concisely: For any type `α`, any seminormed ring `R` with unit `c`, and any function `f` from `α` to `R`, if `l` is a filter on `α`, then `f` is big O of `c * f` at `l`.
|
Asymptotics.IsLittleO.trans_isBigO
theorem Asymptotics.IsLittleO.trans_isBigO :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [inst : Norm E] [inst_1 : Norm F]
[inst_2 : SeminormedAddCommGroup G'] {l : Filter α} {f : α → E} {g : α → F} {k : α → G'},
f =o[l] g → g =O[l] k → f =o[l] k
This theorem, `Asymptotics.IsLittleO.trans_isBigO`, states that for any types `α`, `E`, `F`, and `G'`, where `E` and `F` have a norm and `G'` is a semi-normed additive commutative group, and given a filter `l` and functions `f`, `g`, `k` from `α` to `E`, `F`, `G'` respectively, if `f` is little-o of `g` at `l` and `g` is big-O of `k` at `l`, then `f` is little-o of `k` at `l`. In terms of asymptotic notation, if $f(x)$ is $o(g(x))$ and $g(x)$ is $O(k(x))$ as $x$ approaches a point in the limit `l`, then $f(x)$ is $o(k(x))$.
More concisely: If $f(x) = o(g(x))$ and $g(x) = O(k(x))$ as $x$ approaches $l$, then $f(x) = o(k(x))$.
|
Asymptotics.isLittleO_const_iff
theorem Asymptotics.isLittleO_const_iff :
∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E'']
[inst_1 : NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {c : F''},
c ≠ 0 → ((f'' =o[l] fun _x => c) ↔ Filter.Tendsto f'' l (nhds 0))
The theorem `Asymptotics.isLittleO_const_iff` states that for any type `α`, any normed additive commutative group `E''`, another normed additive commutative group `F''`, a function `f''` from `α` to `E''`, a filter `l` on `α`, and a non-zero constant `c` of type `F''`, the function `f''` is little o of the constant function `c` (under the filter `l`) if and only if the function `f''` tends to the neighborhood of 0 under the filter `l`. In mathematical terms, we could write this as: for a non-zero constant `c`, `f'' = o(c)` as `x` approaches `l` if and only if `f''` tends to 0 as `x` approaches `l`. Here, `f'' = o(c)` means that `f''(x)` is significantly smaller than `c` when `x` is close to the limit `l`.
More concisely: For any normed additive commutative groups E and F, type α, function f from α to E, filter l on α, and non-zero constant c of type F, the function f is little o of the constant function c under filter l if and only if f tends to 0 under filter l.
|
Asymptotics.IsBigOWith.add
theorem Asymptotics.IsBigOWith.add :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ}
{g : α → F} {l : Filter α} {f₁ f₂ : α → E'},
Asymptotics.IsBigOWith c₁ l f₁ g →
Asymptotics.IsBigOWith c₂ l f₂ g → Asymptotics.IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g
The theorem `Asymptotics.IsBigOWith.add` states that for any two functions `f₁` and `f₂` from a type `α` to a semi-normed add commutative group `E'`, and a function `g` from `α` into a normed type `F`, if `f₁` is "Big O" of `g` with constant `c₁` and `f₂` is "Big O" of `g` with constant `c₂` at a filter `l` on `α`, then the function `f₁ + f₂` is "Big O" of `g` at the same filter `l` with constant `c₁ + c₂`. Here, "Big O" is defined in the sense of Landau's notation, that is, `f` is "Big O" of `g` if the norm of `f` is eventually (for `l`) bounded by the product of a constant and the norm of `g`.
More concisely: If functions `f₁` and `f₂` are Big O of a function `g` with constants `c₁` and `c₂`, respectively, at a filter `l` on `α` over a semi-normed add commutative group `E'`, then their sum `f₁ + f₂` is Big O of `g` with constant `c₁ + c₂` at the same filter `l`.
|
Asymptotics.IsBigOWith.abs_left
theorem Asymptotics.IsBigOWith.abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {c : ℝ} {g : α → F} {l : Filter α} {u : α → ℝ},
Asymptotics.IsBigOWith c l u g → Asymptotics.IsBigOWith c l (fun x => |u x|) g
This theorem, referred to as `Asymptotics.IsBigOWith.abs_left`, establishes a relationship for Big-O notation in the context of asymptotic analysis. Specifically, if a function `u` is Big-O of another function `g` with respect to a filter `l` and a constant `c` (denoted as `Asymptotics.IsBigOWith c l u g`), then the absolute value of function `u` (denoted as `|u x|`) is also Big-O of the function `g` with the same constant and filter. In other words, if the norm of `u` is eventually bounded by `c` times the norm of `g` for `l`, then the same holds true when we take the absolute value of `u`. It essentially states that taking the absolute value of a function does not change its Big-O order.
More concisely: If `u` is Big-O of `g` with respect to filter `l` and constant `c`, then `|u|` is also Big-O of `g` with the same constant and filter.
|
Asymptotics.IsBigOWith.abs_abs
theorem Asymptotics.IsBigOWith.abs_abs :
∀ {α : Type u_1} {c : ℝ} {l : Filter α} {u v : α → ℝ},
Asymptotics.IsBigOWith c l u v → Asymptotics.IsBigOWith c l (fun x => |u x|) fun x => |v x|
This theorem states that if a function `u` is "big O" of another function `v` with respect to a filter `l` and constant `c`, which is denoted as `Asymptotics.IsBigOWith c l u v`, then the absolute values of the functions also maintain this relationship. In other words, if `u` is bounded by `c` times `v` in the limit towards the filter `l`, then `|u|` is also bounded by `c` times `|v|` in the same limit. Here, `|u|` and `|v|` represent the functions that send `x` to the absolute value of `u(x)` and `v(x)`, respectively.
More concisely: If `u` is big O of `v` with respect to filter `l` and constant `c` in Lean 4, then `|u|` is also big O of `|v|` with respect to `l` and constant `c`.
|
Asymptotics.IsBigO.abs_right
theorem Asymptotics.IsBigO.abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
f =O[l] u → f =O[l] fun x => |u x|
This theorem, `Asymptotics.IsBigO.abs_right`, is an alias of the reverse direction of `Asymptotics.isBigO_abs_right`. It states that for all types `α` and `E`, where `E` has a norm, and given a function `f` from `α` to `E`, a filter `l` on `α`, and a real-valued function `u` on `α`, if `f` is big-O of `u` at `l` (i.e., `f` grows no faster than `u` as the input approaches the limit `l`), then `f` is also big-O of the absolute value of `u` at `l`. In mathematical terms, if $f(x) = O(u(x))$ as $x$ approaches `l`, then $f(x) = O(|u(x)|)$ as $x$ approaches `l`.
More concisely: If a function `f` from type `α` to a type `E` with a norm, is big-O of a real-valued function `u` at a filter `l`, then `f` is also big-O of the absolute value of `u` at `l`. In other words, `|u|(x) ∣ x ∈ l ∧ f(x) = O(u(x)) ∧ ∀ x, ∃ ε > 0. ∀ δ > 0. ∀ x' ∈ l. abs(u(x')) < ε → abs(f(x')) < δ` implies `|u|(x) ∣ x ∈ l ∧ f(x) = O(|u|(x))`.
|
Asymptotics.IsBigOWith.of_abs_right
theorem Asymptotics.IsBigOWith.of_abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {c : ℝ} {f : α → E} {l : Filter α} {u : α → ℝ},
(Asymptotics.IsBigOWith c l f fun x => |u x|) → Asymptotics.IsBigOWith c l f u
The theorem `Asymptotics.IsBigOWith.of_abs_right` is an alias for the forward direction of `Asymptotics.isBigOWith_abs_right` in Lean 4. It states that for all types `α` and `E`, norm `E`, real number `c`, function `f` from `α` to `E`, filter `l` on `α`, and function `u` from `α` to real numbers, if the Landau notation `IsBigOWith c l f |u x|` holds (where `|u x|` denotes the absolute value of `u x`, and this notation means that eventually for `l`, the norm of `f` is bounded by `c` times the absolute value of `u`), then `IsBigOWith c l f u` also holds (meaning that eventually for `l`, the norm of `f` is bounded by `c` times `u` itself). This theorem essentially says that if the norm of a function `f` is eventually bounded by `c` times the absolute value of another function `u`, it is also eventually bounded by `c` times the function `u` itself.
More concisely: If for all x in the domain of a function f and filter l, the absolute value of f(x) is eventually bounded by a constant c times the absolute value of another function u, then f is eventually bounded by c times u itself.
|
Asymptotics.IsBigOWith.comp_tendsto
theorem Asymptotics.IsBigOWith.comp_tendsto :
∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E}
{g : α → F} {l : Filter α},
Asymptotics.IsBigOWith c l f g →
∀ {k : β → α} {l' : Filter β}, Filter.Tendsto k l' l → Asymptotics.IsBigOWith c l' (f ∘ k) (g ∘ k)
The theorem `Asymptotics.IsBigOWith.comp_tendsto` states that for any two functions `f` and `g` from a type `α` to normed spaces `E` and `F` respectively, if at some filter `l` on `α`, `f` is big O of `g` with constant `c` (i.e., `f` is eventually at most `c` times `g`), then for any function `k` from a type `β` to `α` and any filter `l'` on `β`, if `k` tends to `l` at `l'`, then `(f ∘ k)` is also big O of `(g ∘ k)` with the same constant `c` at `l'`. In other words, the big O order of growth is preserved under composition with a function that tends to the original filter.
More concisely: If function `f` is big O of `g` at filter `l` on type `α` with constant `c`, then `(f ∘ k)` is big O of `(g ∘ k)` at filter `l'` on type `β` with constant `c`, given that `k` tends to `l` at `l'`.
|
Asymptotics.IsBigOWith.weaken
theorem Asymptotics.IsBigOWith.weaken :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c c' : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
Asymptotics.IsBigOWith c l f g' → c ≤ c' → Asymptotics.IsBigOWith c' l f g'
The theorem `Asymptotics.IsBigOWith.weaken` states that for any types `α`, `E`, `F'`, any norm on `E`, any semi-normed add commutative group `F'`, any real numbers `c` and `c'`, any functions `f : α → E` and `g' : α → F'`, and any filter `l` on `α`, if the function `f` is Big O of the function `g'` with respect to the filter `l` and the constant `c`, and `c` is less than or equal to `c'`, then `f` is also Big O of `g'` with respect to the filter `l` and the constant `c'`. In other words, we can increase the Big O constant without affecting the Big O relation.
More concisely: If `f` is Big O of `g'` with respect to filter `l` and constant `c`, and `c <= c'`, then `f` is still Big O of `g'` with respect to filter `l` and constant `c'`.
|
Asymptotics.isBigOWith_norm_right
theorem Asymptotics.isBigOWith_norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
(Asymptotics.IsBigOWith c l f fun x => ‖g' x‖) ↔ Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.isBigOWith_norm_right` states that for any types `α`, `E`, and `F'`, if `E` has a norm and `F'` is a semi-normed add commutative group, then for any real number `c`, any filter `l` on `α`, and any functions `f : α → E` and `g' : α → F'`, the property that `f` is big O of the norm of `g'` (under `l`, with constant `c`) is equivalent to the property that `f` is big O of `g'` (under `l`, with constant `c`). In other words, the norm of function `g'` can be dropped without affecting the big O notation.
More concisely: For types `α`, `E` (a normed vector space), and `F'` (a semi-normed add commutative group), the function `f : α → E` is big O of `g' : α → F'` (under filter `l` and constant `c`) if and only if it is big O of the norm of `g'` (under `l` and constant `c`).
|
Asymptotics.IsLittleO.inv_rev
theorem Asymptotics.IsLittleO.inv_rev :
∀ {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜']
{l : Filter α} {f : α → 𝕜} {g : α → 𝕜'},
f =o[l] g → (∀ᶠ (x : α) in l, f x = 0 → g x = 0) → (fun x => (g x)⁻¹) =o[l] fun x => (f x)⁻¹
This theorem, `Asymptotics.IsLittleO.inv_rev`, states that for any normed division rings `𝕜` and `𝕜'`, and any functions `f : α → 𝕜` and `g : α → 𝕜'` that are asymptotically equal almost everywhere on a filter `l` (i.e., `f =o[l] g`), if `f(x) = 0` implies that `g(x) = 0` almost everywhere on `l`, then the function `g` inverted (1/g(x)) is asymptotically equal to the function `f` inverted (1/f(x)) almost everywhere on `l`. In other words, if `f` and `g` are asymptotically equivalent and their zeros coincide almost everywhere, then their inverses are also asymptotically equivalent.
More concisely: If functions `f : α → 𝕜` and `g : α → 𝕜'` are asymptotically equal almost everywhere on a filter `l` and `f(x) = 0` if and only if `g(x) = 0` almost everywhere on `l`, then `1/f` is asymptotically equal to `1/g` almost everywhere on `l`.
|
Asymptotics.IsLittleO.neg_right
theorem Asymptotics.IsLittleO.neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =o[l] g' → f =o[l] fun x => -g' x
This theorem, named `Asymptotics.IsLittleO.neg_right`, states that for any given types `α`, `E`, and `F'`, where `E` has a norm and `F'` has a semi-normed additive commutative group, and given functions `f : α → E` and `g' : α → F'`, with a filter `l` over `α`, if `f` is little o of `g'` at `l` (denoted as `f =o[l] g'`), then `f` is also little o of the negation of `g'` (denoted as `f =o[l] fun x => -g' x`).
In simpler terms, if the function `f` grows at a slower rate than `g'` at filter `l`, then `f` also grows slower than the negation of `g'` at the same filter.
More concisely: If `f : α → E` is little o of `g' : α → F'` at filter `l` over `α`, then `f` is also little o of the negation of `g'` at `l`.
|
Asymptotics.isBigO_refl
theorem Asymptotics.isBigO_refl :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] (f : α → E) (l : Filter α), f =O[l] f
This theorem, `Asymptotics.isBigO_refl`, states that for any type `α`, any normed type `E`, any function `f` from `α` to `E`, and any filter `l` on `α`, the function `f` is asymptotically bounded by itself, i.e., `f` is Big O of `f` (`f =O[l] f`) at the filter `l`. In the language of theoretical computer science or mathematics, this means that the growth rate of the function `f` is at most as fast as the growth rate of the function `f`, which is always true.
More concisely: For any type `α`, normed type `E`, function `f` from `α` to `E`, and filter `l` on `α`, `f` is in Big O notation with respect to `l`, i.e., `f = O(f)` at the filter `l`.
|
Asymptotics.isBigOWith_snd_prod
theorem Asymptotics.isBigOWith_snd_prod :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α},
Asymptotics.IsBigOWith 1 l g' fun x => (f' x, g' x)
The theorem `Asymptotics.isBigOWith_snd_prod` states that for any type `α`, any two types `E'` and `F'` that form semi-normed additive commutative groups, any two functions `f'` and `g'` from `α` to `E'` and `F'` respectively, and any filter `l` on `α`, the function `g'` is Big O of the function that takes `x` from `α` and returns the pair `(f' x, g' x)`. Here, the Big O notation is being used with a constant factor of 1. In other words, for values that are eventually reached when applying the filter `l`, the norm of `g'(x)` does not exceed the norm of the pair `(f'(x), g'(x))`.
More concisely: For any type `α`, given semi-normed additive commutative groups `E'` and `F'`, functions `f': α -> E'` and `g': α -> F'`, and a filter `l` on `α`, the function `g'` is Big O of the function that maps `x` in `α` to the pair `(f' x, g' x)` with respect to the norm.
|
Asymptotics.IsBigO.const_mul_left
theorem Asymptotics.IsBigO.const_mul_left :
∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {g : α → F}
{l : Filter α} {f : α → R}, f =O[l] g → ∀ (c' : R), (fun x => c' * f x) =O[l] g
This theorem, `Asymptotics.IsBigO.const_mul_left`, states that for any given types `α`, `F`, and `R` along with an instance of Norm over `F`, an instance of SeminormedRing over `R`, a function `g` mapping from `α` to `F`, a filter `l` over `α`, and a function `f` mapping from `α` to `R`, if `f` is `Big O` of `g` at filter `l`, then, for any constant `c'` of type `R`, the function that maps `x` to `c' * f(x)` is also `Big O` of `g` at filter `l`. In simpler terms, if a function `f` grows no faster than a function `g`, then the function `c' * f`, where `c'` is a constant, also grows no faster than `g`.
More concisely: If `f` is Big O of `g` at filter `l` in Lean, then `c * f` is also Big O of `g` at filter `l` for any constant `c` of type `R`.
|
Asymptotics.IsBigO.of_norm_norm
theorem Asymptotics.IsBigO.of_norm_norm :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α},
((fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖) → f' =O[l] g'
This theorem, `Asymptotics.IsBigO.of_norm_norm`, is an alias for the forward direction of `Asymptotics.isBigO_norm_norm`. It states that for any types `α`, `E'`, and `F'`, along with any seminormed additive commutative groups over `E'` and `F'`, any functions `f'` and `g'` from `α` to `E'` and `F'` respectively, and any filter `l` on `α`, if the norm of `f'` is big O of the norm of `g'` at filter `l`, then `f'` itself is also big O of `g'` at the same filter. In other words, if the magnitudes of `f'` and `g'` grow comparably for large inputs, then `f'` and `g'` themselves also grow comparably.
More concisely: If the norm of function `f'` is big O of the norm of function `g'` at filter `l`, then function `f'` is big O of `g'` at filter `l`.
|
Asymptotics.isBigOWith_congr
theorem Asymptotics.isBigOWith_congr :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {l : Filter α}
{f₁ f₂ : α → E} {g₁ g₂ : α → F},
c₁ = c₂ →
l.EventuallyEq f₁ f₂ →
l.EventuallyEq g₁ g₂ → (Asymptotics.IsBigOWith c₁ l f₁ g₁ ↔ Asymptotics.IsBigOWith c₂ l f₂ g₂)
The theorem `Asymptotics.isBigOWith_congr` states that for any two types `α`, `E`, and `F` with norms, given two real numbers `c₁` and `c₂`, a filter `l` on `α`, and four functions `f₁`, `f₂` from `α` to `E` and `g₁`, `g₂` from `α` to `F`, if `c₁` equals `c₂`, `f₁` equals `f₂` almost surely with respect to the filter `l`, and `g₁` equals `g₂` almost surely with respect to the filter `l`, then `f₁` is "big O" to `g₁` with constant `c₁` if and only if `f₂` is "big O" to `g₂` with constant `c₂`. Here, being "big O" means that the norm of `f` is eventually (for `l`) bounded by `c` times the norm of `g`.
More concisely: If functions `f₁` and `f₂` are almost surely equal and `g₁` is almost surely equal to `g₂`, then `f₁` is big O of `g₁` with constant `c₁` if and only if `f₂` is big O of `g₂` with constant `c₂`.
|
Asymptotics.isBigOWith_of_eq_mul
theorem Asymptotics.isBigOWith_of_eq_mul :
∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {c : ℝ} {l : Filter α} {u v : α → R} (φ : α → R),
(∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) → l.EventuallyEq u (φ * v) → Asymptotics.IsBigOWith c l u v
The theorem `Asymptotics.isBigOWith_of_eq_mul` states that if the norm of a function `φ` is eventually bounded by a constant `c`, and another function `u` is equal to the product of `φ` and `v` almost everywhere with respect to a filter `l`, then `u` is big-O of `v` with constant `c` and filter `l`. This signifies that the magnitude of `u` is eventually, for `l`, at most `c` times the magnitude of `v`. This theorem does not require any conditions on `c`, which differentiates it from `IsBigOWith_iff_exists_eq_mul`.
More concisely: If a function `φ` is eventually bounded by a constant `c` and equals the product of functions `φ` and `v` almost everywhere with respect to a filter `l`, then `φ` is big-O of `v` with constant `c` and filter `l`.
|
Asymptotics.IsLittleO.congr
theorem Asymptotics.IsLittleO.congr :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
{g₁ g₂ : α → F}, f₁ =o[l] g₁ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → f₂ =o[l] g₂
This theorem states that for any types `α`, `E`, and `F` with `E` and `F` being normed, any filter `l` on `α`, and any four functions `f₁`, `f₂` from `α` to `E`, `g₁`, `g₂` from `α` to `F`, if `f₁` is little-o of `g₁` at `l` and `f₁` equals `f₂` and `g₁` equals `g₂` for all `x` in `α`, then `f₂` is also little-o of `g₂` at `l`. In mathematical terms, we can write this as: if \(f_1(x) = O(g_1(x))\) as \(x \to l\), \(f_1(x) = f_2(x)\) and \(g_1(x) = g_2(x)\) for all \(x\), then \(f_2(x) = O(g_2(x))\) as \(x \to l\).
More concisely: If `f₁(x) = O(g₁(x))` and `f₁(x) = f₂(x)` and `g₁(x) = g₂(x)` for all `x`, then `f₂(x) = O(g₂(x))`. In other words, if `f₁` is little-o of `g₁` and `f₁` equals `f₂` and `g₁` equals `g₂`, then `f₂` is also little-o of `g₂`.
|
Asymptotics.IsLittleO.exists_eq_mul
theorem Asymptotics.IsLittleO.exists_eq_mul :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {u v : α → 𝕜},
u =o[l] v → ∃ φ, Filter.Tendsto φ l (nhds 0) ∧ l.EventuallyEq u (φ * v)
This theorem, named `Asymptotics.IsLittleO.exists_eq_mul`, represents a variant of `Asymptotics.isLittleO_iff_exists_eq_mul` in the forward direction. It states that for any types `α` and `𝕜`, where `𝕜` is a normed division ring, and given a filter `l` and functions `u` and `v` from `α` to `𝕜`, if `u` is little-o of `v` at filter `l` (denoted as `u =o[l] v`), then there exists a function `φ` such that `φ` tends towards 0 at the neighborhood filter of 0 (`nhds 0`) along `l`, and `u` equals `φ * v` almost everywhere with respect to filter `l`. The latter means that `u` and `φ * v` take the same values at all points of `α` except possibly a set of elements that `l` ignores. In other words, `u` can be expressed as a function `φ` multiplied by `v`, where `φ` tends to 0 as it approaches the limit under the filter `l`.
More concisely: If `u` is little-o of `v` at filter `l` in a normed division ring `𝕜` over type `α`, then there exists a function `φ` tending to 0 at `nhds 0` along `l`, such that `u` equals `φ * v` almost everywhere with respect to `l`.
|
Asymptotics.IsLittleO.congr_left
theorem Asymptotics.IsLittleO.congr_left :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {g : α → F} {l : Filter α}
{f₁ f₂ : α → E}, f₁ =o[l] g → (∀ (x : α), f₁ x = f₂ x) → f₂ =o[l] g
This theorem states that in the context of asymptotic notation, if a function `f₁` is little-o of another function `g` (which is represented as `f₁ =o[l] g`), and every output of `f₁` is equal to the corresponding output of another function `f₂` (expressed as `∀ (x : α), f₁ x = f₂ x`), then `f₂` is also little-o of `g` (expressed as `f₂ =o[l] g`). Essentially, it shows that the little-o property is preserved under pointwise equality.
More concisely: If `f₁ =o[l] g` and `∀ (x : α), f₁ x = f₂ x`, then `f₂ =o[l] g`.
|
Asymptotics.isLittleO_iff
theorem Asymptotics.isLittleO_iff :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
This theorem, `Asymptotics.isLittleO_iff`, states the definition of "little-o" notation in the context of asymptotic analysis with filters. Specifically, it asserts that for any functions `f : α → E` and `g : α → F`, where `E` and `F` are normed spaces over some type `α`, and a given filter `l` on `α`, `f` is "little-o" of `g` at `l` if and only if for any positive real number `c`, eventually (as defined by the filter `l`), the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`. This encapsulates the notion that `f` grows no faster than `g` near the limit points defined by the filter `l`.
More concisely: For functions `f : α → E` and `g : α → F` over a filter `l` on `α` in normed spaces `E` and `F`, `f` is little-o of `g` at `l` if and only if for every `c > 0`, eventually, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`.
|
Asymptotics.IsLittleO.mul_isBigO
theorem Asymptotics.IsLittleO.mul_isBigO :
∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
{l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜},
f₁ =o[l] g₁ → f₂ =O[l] g₂ → (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
The theorem `Asymptotics.IsLittleO.mul_isBigO` states that for any types `α`, `R`, and `𝕜`, along with a `SeminormedRing R` and a `NormedDivisionRing 𝕜`, given a filter `l` and functions `f₁`, `f₂`, `g₁`, and `g₂` from `α` to `R` or `𝕜`, if `f₁` is little-o of `g₁` at `l` and `f₂` is big-O of `g₂` at `l`, then the function defined by the product of `f₁` and `f₂` is little-o of the function defined by the product of `g₁` and `g₂` at `l`. This theorem is about the multiplication of little-o and big-O functions and their relationships in asymptotic analysis.
More concisely: If `f₁` is little-o of `g₁` and `f₂` is big-O of `g₂` at a filter `l`, then `f₁ * f₂` is little-o of `g₁ * g₂` at `l`.
|
Asymptotics.IsLittleO.neg_left
theorem Asymptotics.IsLittleO.neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, f' =o[l] g → (fun x => -f' x) =o[l] g
The theorem `Asymptotics.IsLittleO.neg_left` is an alias of the reverse direction of `Asymptotics.isLittleO_neg_left`. This theorem states that, for any types α, F, and E', where F has a norm and E' is a seminormed add commutative group, and for any functions g: α → F and f': α → E', and a filter l on α, if f' is little-o of g according to filter l, then the negation of f' is also little-o of g according to the same filter. This is expressed in Lean as `f' =o[l] g → (fun x => -f' x) =o[l] g`. Here, `=o[l]` denotes the little-o notation at filter l. Little-o notation is used in analysis to describe limiting behavior of functions.
More concisely: If a function f' is little-o of another function g with respect to a filter l, then the negative of f' is also little-o of g with respect to the same filter.
|
Asymptotics.IsBigOWith.trans
theorem Asymptotics.IsBigOWith.trans :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
{c c' : ℝ} {f : α → E} {g : α → F} {k : α → G} {l : Filter α},
Asymptotics.IsBigOWith c l f g →
Asymptotics.IsBigOWith c' l g k → 0 ≤ c → Asymptotics.IsBigOWith (c * c') l f k
The theorem `Asymptotics.IsBigOWith.trans` states that, for any normed types `E`, `F`, `G` and any functions `f : α → E`, `g : α → F`, and `k : α → G`, if `f` is big-O of `g` with constant `c` at a filter `l` and `g` is big-O of `k` with constant `c'` at the same filter, then `f` is big-O of `k` with constant `c*c'` at `l`, provided that `c` is non-negative. In other words, the big-O notation's transitivity property is upheld: if `f` is eventually bounded by `c * ‖g‖` and `g` is eventually bounded by `c' * ‖k‖`, then `f` is eventually bounded by `(c * c') * ‖k‖`.
More concisely: Given normed types E, F, G and functions f, g, and k with non-negative constant c and c', if f is big-O of g with constant c and g is big-O of k with constant c' at filter l, then f is big-O of k with constant c * c' at filter l.
|
Asymptotics.IsLittleO.of_neg_left
theorem Asymptotics.IsLittleO.of_neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => -f' x) =o[l] g → f' =o[l] g
This theorem is an alias of the forward direction of `Asymptotics.isLittleO_neg_left` in asymptotic analysis. Given types `α`, `F`, `E'` and a filter `l` on `α`, and functions `f' : α → E'` and `g : α → F` such that the negative of `f'` is little-o of `g` with respect to the filter `l` (written as `(-f' x) =o[l] g`), it asserts that `f'` is also little-o of `g` with respect to the same filter (written as `f' =o[l] g`). The `Norm F` and `SeminormedAddCommGroup E'` contexts imply that `F` has a norm and `E'` is a seminormed additive commutative group.
More concisely: If `f'` is little-o of `g` with respect to filter `l` and `-f'` is also little-o of `g` with respect to `l`, then `f'` is little-o of `g` with respect to `l`.
|
Asymptotics.isBigO_snd_prod
theorem Asymptotics.isBigO_snd_prod :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α}, g' =O[l] fun x => (f' x, g' x)
The theorem `Asymptotics.isBigO_snd_prod` states that for any types `α`, `E'`, and `F'`, with `E'` and `F'` being seminormed add commutative groups, and any functions `f' : α → E'` and `g' : α → F'`, as well as a filter `l` on `α`, the function `g'` is Big O of the function that maps `x` to the tuple `(f' x, g' x)` at the filter `l`. In mathematical terms, this means that `g'` grows at most as fast as the tuple function `(f' x, g' x)` near the points determined by the filter `l`.
More concisely: For any types `α`, `E'`, and `F'` (with `E'` and `F'` seminormed add commutative groups), and functions `f': α -> E'` and `g': α -> F'`, if `l` is a filter on `α`, then `g'` is Big O of the function `x => (f' x, g' x)` at the filter `l`.
|
Asymptotics.IsBigOWith.norm_norm
theorem Asymptotics.IsBigOWith.norm_norm :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : 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‖
The theorem `Asymptotics.IsBigOWith.norm_norm` is an alias of the reverse direction of `Asymptotics.isBigOWith_norm_norm`. It states that for any types `α`, `E'`, `F'`, seminormed add commutative groups `E'` and `F'`, a real number `c`, functions `f'` and `g'` from `α` to `E'` and `F'` respectively, and a filter `l` on `α`, if the function `f'` is big O of `g'` with respect to `c` and `l` (meaning, the norm of `f'` is eventually bounded by `c` times the norm of `g'`), then the same is true when we consider the norms of `f'` and `g'` as functions themselves. That is, the norm of `f'` is big O of the norm of `g'` under the same conditions.
More concisely: If `f'` is big O of `g'` with respect to `c` and `l` in the sense of norms on `E'` and `F'`, then the norm of `f'` is big O of the norm of `g'` under the same conditions.
|
PartialHomeomorph.isLittleO_congr
theorem PartialHomeomorph.isLittleO_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
[inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : PartialHomeomorph α β) {b : β},
b ∈ e.target → ∀ {f : β → E} {g : β → F}, f =o[nhds b] g ↔ (f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)
This theorem states that the asymptotic behavior of two functions `f` and `g` at a point `b` in the context of a `PartialHomeomorph` `e` is maintained under the homeomorphism. More formally, given a `PartialHomeomorph` `e` from a topological space `α` to another topological space `β`, and two functions `f` and `g` from `β` to normed spaces `E` and `F` respectively, if `f` is little-o of `g` at `b` in the filter of neighborhoods of `b` (denoted `f =o[nhds b] g`), then this is equivalent to `(f ∘ ↑e)` being little-o of `(g ∘ ↑e)` at the image of `b` under the inverse of `e` in the filter of neighborhoods of the inverse image of `b` (denoted `(f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)`). Here, `little-o` notation indicates that `f` grows slower than `g` as we approach the point `b`.
More concisely: Given a `PartialHomeomorph` `e` from a topological space `α` to `β`, and functions `f: β -> NormedSpace E` and `g: β -> NormedSpace F` with `f =o[nhds b] g`, then `(f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)`.
|
Asymptotics.IsBigO.norm_right
theorem Asymptotics.IsBigO.norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =O[l] g' → f =O[l] fun x => ‖g' x‖
This theorem, "Asymptotics.IsBigO.norm_right", is an alias of the reverse direction of `Asymptotics.isBigO_norm_right`. It applies to functions `f` and `g'` mapping from a type `α` to types `E` and `F'` respectively, where `E` has a norm structure, `F'` is a semi-normed additive commutative group, and `l` is a filter on `α`. The theorem states that if `f` is Big O of `g'` at filter `l`, i.e., `f` grows no faster than `g'` in the limit as defined by `l`, then `f` is also Big O of the norm of `g'` at the same filter.
More concisely: If `f` is Big O of `g'` at filter `l`, then `f` is Big O of the norm of `g'` at filter `l`, for functions `f` from type `α` to a normed type `E` and `g'` to a semi-normed additive commutative group `F'`, where `l` is a filter on `α`.
|
Asymptotics.isLittleO_iff_nat_mul_le_aux
theorem Asymptotics.isLittleO_iff_nat_mul_le_aux :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α},
((∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖) → (f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖)
This theorem states that for all types `α`, `E`, and `F`, given a norm instance for `E` and `F`, and functions `f : α → E` and `g : α → F` with a specific filter `l`, either every `x` in `α` satisfies that the norm of `f(x)` is greater than or equal to 0 or every `x` in `α` satisfies that the norm of `g(x)` is greater than or equal to 0. If this is the case, then `f` is little-o of `g` with respect to filter `l` if and only if for every natural number `n`, eventually for every `x` in `α` in filter `l`, `n` times the norm of `f(x)` is less than or equal to the norm of `g(x)`. In the context of asymptotics, this theorem provides a characterization of the little-o notation in terms of the inequality involving the norms of functions `f` and `g`.
More concisely: For types `α`, `E`, and `F` with norm instances, given functions `f : α → E` and `g : α → F`, and filter `l`, if for all `x` in `α` in `l`, either the norm of `f(x)` ≥ 0 or the norm of `g(x)` ≥ 0, then `f` is little-o of `g` with respect to `l` if and only if for all natural `n`, eventually for all `x` in `α` in `l`, `n·‖f(x)‖≤‖g(x)‖`.
|
Asymptotics.IsBigOWith.of_abs_left
theorem Asymptotics.IsBigOWith.of_abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {c : ℝ} {g : α → F} {l : Filter α} {u : α → ℝ},
Asymptotics.IsBigOWith c l (fun x => |u x|) g → Asymptotics.IsBigOWith c l u g
The theorem `Asymptotics.IsBigOWith.of_abs_left` is an alias of the forward direction of `Asymptotics.isBigOWith_abs_left`. It states that for any types `α` and `F`, where `F` is a normed type, along with a real number `c`, a function `g` from `α` to `F`, a filter `l` on `α`, and a real-valued function `u` on `α`, if `Asymptotics.IsBigOWith`holds with `c`, `l`, the absolute value of `u` and `g`, then `Asymptotics.IsBigOWith` also holds with the same `c`, `l`, `u` and `g`. This means that if the absolute value of `u(x)` is eventually bounded by `c * ‖g‖` for the filter `l`, then the same holds true for `u(x)` itself, ignoring the absolute value.
More concisely: If `g(x)` is big-O of `u(x)` up to a constant factor for absolute values, then `g(x)` is also big-O of `u(x)` without the absolute value constraint.
|
Asymptotics.IsLittleO.isBigO
theorem Asymptotics.IsLittleO.isBigO :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =o[l] g → f =O[l] g
This theorem states that for any types `α`, `E`, and `F`, given that `E` and `F` have a norm defined on them, and given any two functions `f : α → E` and `g : α → F` and a filter `l` on `α`, if `f` is little-o of `g` at the filter `l` (written as `f =o[l] g`), then `f` is also Big-O of `g` at the filter `l` (written as `f =O[l] g`). In mathematical terms, this is saying that if `f(x)` is dominated by `g(x)` as `x` approaches a certain limit (in the sense of little-o), then `f(x)` is also bounded above by `g(x)` times some constant near that limit (in the sense of Big-O).
More concisely: If `f : α → E` and `g : α → F` are functions on a type `α` with norms, and `l` is a filter on `α` such that `f =o[l] g`, then `f =O[l] g`. In other words, little-o implies Big-O for functions `f` and `g` at filter `l`.
|
Asymptotics.IsBigOWith.of_neg_right
theorem Asymptotics.IsBigOWith.of_neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ}
{f : α → E} {g' : α → F'} {l : Filter α},
(Asymptotics.IsBigOWith c l f fun x => -g' x) → Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.IsBigOWith.of_neg_right` states that for any real constant `c`, filter `l` on a type `α`, and functions `f` from `α` to `E` and `g'` from `α` to `F'`, if `f` is `O(c * -g')`, then `f` is also `O(c * g')`. Here, `O` is the Big O notation which states that `f` is asymptotically less than or equal to `c * g'` in magnitude. This theorem is about the symmetry of the Big O relation with respect to negation of the function `g'`. Essentially, if `f` is bounded by `c` times the negative of `g'` at the limit defined by the filter `l`, then `f` is also bounded by `c` times `g'` at that limit.
More concisely: If `f` is Big O of `-c * g'` with respect to filter `l`, then `f` is also Big O of `c * g'` with respect to `l`.
|
Asymptotics.IsBigOWith.right_le_add_of_lt_1
theorem Asymptotics.IsBigOWith.right_le_add_of_lt_1 :
∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'},
Asymptotics.IsBigOWith c l f₁ f₂ → c < 1 → Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x
This theorem, which is an alias of `Asymptotics.IsBigOWith.right_le_add_of_lt_one`, states that for any type `α`, any seminormed additive commutative group `E'`, any real number `c` that is less than 1, any filter `l` on `α`, and any two functions `f₁` and `f₂` from `α` to `E'`, if `f₁` is big O of `f₂` with constant `c` with respect to filter `l` (that is, the norm of `f₁` is eventually bounded by `c` times the norm of `f₂`), then `f₂` is big O of the function `f₁ + f₂` with constant `1 / (1 - c)`. Here, the function `f₁ + f₂` is defined pointwise, i.e., for all `x` in `α`, `(f₁ + f₂)(x)` equals `f₁(x) + f₂(x)`. In other words, the theorem states that if `f₁` grows no faster than `c` times `f₂` for some `c < 1`, then `f₂` grows no faster than `1 / (1 - c)` times the function `f₁ + f₂`.
More concisely: For any type `α`, seminormed additive commutative group `E'`, real number `c` < 1, filter `l` on `α`, and functions `f₁, f₂` from `α` to `E'`, if `f₁` is big O of `f₂` with constant `c` with respect to `l`, then `f₂` is big O of `f₁ + f₂` with constant `1 / (1 - c)`.
|
Asymptotics.IsBigOWith.of_neg_left
theorem Asymptotics.IsBigOWith.of_neg_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ}
{g : α → F} {f' : α → E'} {l : Filter α},
Asymptotics.IsBigOWith c l (fun x => -f' x) g → Asymptotics.IsBigOWith c l f' g
The theorem `Asymptotics.IsBigOWith.of_neg_left` states that for any types `α`, `F`, and `E'`, where `F` is a normed type and `E'` is a semi-normed add commutative group, given a real number `c`, functions `g : α → F` and `f' : α → E'`, and a filter `l` on `α`, if the function `-f'` is `BigOWith` with respect to function `g` and constant `c` at filter `l` (i.e., it can be bounded by `c` times `g` eventually at filter `l`), then the function `f'` also satisfies this property. In other words, if the normed value of the function `-f'` is eventually bounded by `c` times the normed value of the function `g` at the filter `l`, then the same holds true for the function `f'`.
More concisely: If `-f'` is BigOWith(`g`, `c`) at filter `l` in Lean, then `f'` is also BigOWith(`g`, `c`) at filter `l`.
|
Asymptotics.IsBigOWith.isBigO
theorem Asymptotics.IsBigOWith.isBigO :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
{l : Filter α}, Asymptotics.IsBigOWith c l f g → f =O[l] g
The theorem `Asymptotics.IsBigOWith.isBigO` states that for any types `α`, `E`, `F` and any normed spaces `E` and `F`, for any real number `c`, and for any functions `f: α → E` and `g: α → F`, and for any filter `l` on `α`, if it is true that the function `f` is Big-O of `g` with respect to the filter `l` and constant `c` (in the sense of the definition `Asymptotics.IsBigOWith`), then `f` is Big-O of `g` with respect to the filter `l` (in the sense of the relation `=O[l]`). In simpler terms, if the norms of `f` are eventually bounded by `c` times the norms of `g` for `l`, then `f` is Big-O of `g` for `l`.
More concisely: If `f` is Big-O of `g` with respect to filter `l` and constant `c` according to the definition `Asymptotics.IsBigOWith`, then `f = O(g)` with respect to filter `l`.
|
Asymptotics.IsLittleO.of_neg_right
theorem Asymptotics.IsLittleO.of_neg_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =o[l] fun x => -g' x) → f =o[l] g'
This theorem, `Asymptotics.IsLittleO.of_neg_right`, is an alias for the forward direction of `Asymptotics.isLittleO_neg_right`. The theorem states that for any types `α`, `E`, and `F'`, a normed space over type `E`, a semi-normed add commutative group over type `F'`, a function `f` mapping from type `α` to `E`, another function `g'` mapping from type `α` to `F'`, and a filter `l` on `α`, if `f` is little o of `-g'` at `l`, then `f` is also little o of `g'` at `l`. In mathematical terms, this theorem is saying that if $f(x) = O(-g'(x))$ as $x$ approaches a certain value (according to the filter `l`), then it must also be true that $f(x) = O(g'(x))$.
More concisely: If a function `f` is little o of the negative of another function `g'` at a filter `l`, then `f` is also little o of `g'` at `l`.
|
Asymptotics.IsLittleO.of_abs_left
theorem Asymptotics.IsLittleO.of_abs_left :
∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
(fun x => |u x|) =o[l] g → u =o[l] g
This theorem, `Asymptotics.IsLittleO.of_abs_left`, is an alias for the forward direction of `Asymptotics.isLittleO_abs_left`. It states that for any types `α` and `F` (where `F` has a norm instance), given functions `g : α → F`, `u : α → ℝ`, and a filter `l` on `α`, if the absolute value function of `u`, denoted by `(fun x => |u x|)`, is little-o of `g` with respect to filter `l` (i.e., `(fun x => |u x|) =o[l] g`), then `u` itself is also little-o of `g` with respect to the same filter (i.e., `u =o[l] g`). In simple terms, if the absolute value of a real-valued function `u` grows no faster than another function `g` when approaching certain points, then `u` itself also grows no faster than `g` at those points.
More concisely: If the absolute value of a function `u : α → ℝ` is little-o of another function `g : α → F` (where `F` has a norm instance) with respect to a filter `l` on `α`, then `u` is also little-o of `g` with respect to `l`.
|
Asymptotics.isBigO_abs_right
theorem Asymptotics.isBigO_abs_right :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
(f =O[l] fun x => |u x|) ↔ f =O[l] u
This theorem, `Asymptotics.isBigO_abs_right`, states that for any types α and E, with E being a normed space, and any functions `f : α → E` and `u : α → ℝ`, and a filter `l` on α, `f` is Big O of the absolute value function of `u` with respect to the filter `l` if and only if `f` is Big O of `u` with respect to the same filter. In simpler terms, it means that the big O notation is not affected by taking the absolute value of the second function.
More concisely: For functions `f : α → E` and `u : α → ℝ` on type `α` with `E` a normed space, and filter `l` on `α`, `f` is Big O of the absolute value of `u` with respect to `l` if and only if `f` is Big O of `u` with respect to `l`.
|
Asymptotics.isBigO_iff_eventually_isBigOWith
theorem Asymptotics.isBigO_iff_eventually_isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =O[l] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.isBigO_iff_eventually_isBigOWith` states that for any types `α`, `E`, and `F'`, where `E` is a normed space and `F'` is a seminormed add commutative group, and for any functions `f: α → E` and `g': α → F'`, and a filter `l` on `α`, `f` is big-O of `g'` at filter `l` if and only if for all real numbers `c` that are sufficiently large, `f` is big-O with respect to `g'` with constant `c` at filter `l`.
In other words, `f` is asymptotically bounded above by `g'` multiplied by a constant `c` for all `c` beyond a certain threshold. This is equivalent to saying that the ratio of the norms of `f` and `g'` is eventually bounded by `c`, with the understanding that issues related to division by zero are avoided by the definition.
More concisely: For functions `f: α → E` and `g': α → F'` with `E` a normed space, `F'` a seminormed add commutative group, and filter `l` on `α`, `f` is big-O of `g'` at filter `l` if and only if there exists a constant `c` such that for all `x ∈ l`, the norm of `f x` is eventually less than or equal to `c` times the seminorm of `g' x`.
|
Asymptotics.IsLittleO.norm_norm
theorem Asymptotics.IsLittleO.norm_norm :
∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E']
[inst_1 : SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α},
f' =o[l] g' → (fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖
This theorem, `Asymptotics.IsLittleO.norm_norm`, states that for any types `α`, `E'`, and `F'`, where `E'` and `F'` form seminormed additively commutative groups, and for any functions `f'` and `g'` from `α` to `E'` and `F'` respectively, and a filter `l` on `α`, if `f'` is little o of `g'` at `l`, then the norm of `f'` is also little o of the norm of `g'` at `l`. This is simply an alias of the reverse direction of `Asymptotics.isLittleO_norm_norm`.
In simpler terms, if a function `f'` grows no faster than a function `g'` as they both approach a particular point according to a certain filter, then the "size" (determined by the norm) of `f'` also grows no faster than the "size" of `g'`.
More concisely: If `f': α → E'` is little o of `g': α → F'` at a filter `l` on `α`, then the norm of `f'` is little o of the norm of `g'` at filter `l` in the seminormed additively commutative groups `E'` and `F'`.
|
Asymptotics.IsBigO.exists_pos
theorem Asymptotics.IsBigO.exists_pos :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, f =O[l] g' → ∃ c > 0, Asymptotics.IsBigOWith c l f g'
The theorem `Asymptotics.IsBigO.exists_pos` states that for any types `α`, `E`, `F'`, where `E` has a norm and `F'` is a semi-normed add commutative group, and for any functions `f : α → E` and `g' : α → F'`, and any filter `l` on `α`, if `f` is of the same order of magnitude as `g'` at `l` (denoted as `f =O[l] g'`), then there exists a positive real number `c` such that `f` is 'big O' of `g'` with constant `c` at `l`. In other words, `f` is asymptotically bounded by `c * g'` near the filter `l`.
More concisely: If a function `f` is of the same order of magnitude as `g'` at a filter `l` on type `α`, then there exists a constant `c` such that `f(x) ≤ c * g'(x)` for all `x` in `α` near `l`.
|
Asymptotics.isLittleO_norm_right
theorem Asymptotics.isLittleO_norm_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
{g' : α → F'} {l : Filter α}, (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'
The theorem `Asymptotics.isLittleO_norm_right` states that for any types `α`, `E`, and `F'`, with `E` being a normed space, and `F'` being a seminormed add commutative group, and for any functions `f : α → E` and `g' : α → F'`, and for any filter `l` on `α`, `f` is little-o of the norm of `g'` at `l` if and only if `f` is little-o of `g'` at `l`. In terms of asymptotic notation, this theorem is saying that `f(x)` is asymptotically smaller than `‖g' x‖` if and only if `f(x)` is asymptotically smaller than `g' x`.
More concisely: For functions `f : α → E` from type `α` to a normed space `E` and `g' : α → F'` from type `α` to a seminormed additive commutative group `F'`, `f` is little-o of the norm of `g'` at a filter `l` on `α` if and only if `f` is little-o of `g'` at `l`. In other words, `f(x)` is asymptotically smaller than `‖g' x‖` and `g' x` as `x` approaches limits in `l`.
|
Asymptotics.IsBigOWith.of_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
The theorem `Asymptotics.IsBigOWith.of_abs_abs` states that for any given type `α`, scalar `c`, filter `l` on `α`, and functions `u` and `v` from `α` to real numbers, if the absolute value of `u(x)` is bounded by `c` times the absolute value of `v(x)` eventually for the filter `l`, then `u(x)` is also bounded by `c` times `v(x)` eventually for the same filter. This is essentially saying that if `|u(x)|` is big O of `|v(x)|`, then `u(x)` is also big O of `v(x)`, using the definition of big O notation in asymptotic analysis.
More concisely: If for all x in the filter l, |u(x)| ≤ c * |v(x)| implies u(x) ≤ c * v(x) eventually for the same filter l.
|
Asymptotics.IsBigO.norm_left
theorem Asymptotics.IsBigO.norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, f' =O[l] g → (fun x => ‖f' x‖) =O[l] g
This theorem, `Asymptotics.IsBigO.norm_left`, is an alias for the reverse direction of the theorem `Asymptotics.isBigO_norm_left`. It states that for any types `α`, `F`, and `E'`, where `F` has a norm and `E'` is a seminormed additive commutative group, and any functions `g : α → F` and `f' : α → E'`, if `f'` is Big O of `g` at a filter `l` (denoted as `f' =O[l] g`), then the function that takes `x` to the norm of `f'(x)` is also Big O of `g` at the same filter (denoted as `(fun x => ‖f' x‖) =O[l] g`). In simpler terms, if `f'` grows no faster than `g` in terms of order of magnitude, then the same is true for the norm of `f'`.
More concisely: If `f'` is Big O of `g` at filter `l`, then the function `x ↔> ‖f' x‖` is Big O of `g` at filter `l` in the normed additive commutative group `E'`.
|
Homeomorph.isBigO_congr
theorem Homeomorph.isBigO_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
[inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F},
f =O[nhds b] g ↔ (f ∘ ⇑e) =O[nhds (e.symm b)] (g ∘ ⇑e)
This theorem states that the `IsBigO` property, a concept from asymptotic analysis indicating that a function's growth is bounded by another, is invariant under a `Homeomorph`, a continuous, bijective transformation between two topological spaces with a continuous inverse. Specifically, for any homeomorphism `e` from a topological space `α` to another topological space `β`, and for any two functions `f` and `g` from `β` to normed spaces `E` and `F` respectively, `f` is `IsBigO` of `g` at a neighborhood of point `b` in `β` if and only if the composite functions `f ∘ ⇑e` and `g ∘ ⇑e` exhibit the `IsBigO` property at the neighborhood of the point `e.symm b` in `α`.
More concisely: For any homeomorphism between topological spaces and any functions from the image space to normed spaces, if one function is big O of another at a point in the image space, then the composite functions exhibit the same big O relation at the preimage point in the domain space.
|
Asymptotics.IsBigO.trans_tendsto
theorem Asymptotics.IsBigO.trans_tendsto :
∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E'']
[inst_1 : NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α},
f'' =O[l] g'' → Filter.Tendsto g'' l (nhds 0) → Filter.Tendsto f'' l (nhds 0)
The theorem `Asymptotics.IsBigO.trans_tendsto` states that for any types `α`, `E''`, and `F''`, where `E''` and `F''` are normed additively commutative groups, if a function `f''` from `α` to `E''` is dominated by another function `g''` from `α` to `F''` (i.e., `f''` is Big-O of `g''`) at a filter `l`, and if the function `g''` tends to 0 at `l` (i.e., for every neighborhood of 0, the preimage of that neighborhood under `g''` is a neighborhood at `l`), then the function `f''` also tends to 0 at `l`. In other words, if `f''` is asymptotically smaller than `g''` and `g''` tends to zero, then `f''` must also tend to zero.
More concisely: If a function `f''` is Big-O of another function `g''` at a filter `l` and `g''` tends to 0 at `l`, then `f''` tends to 0 at `l` (in the context of normed additively commutative groups).
|
Asymptotics.IsLittleO.congr'
theorem Asymptotics.IsLittleO.congr' :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
{g₁ g₂ : α → F}, f₁ =o[l] g₁ → l.EventuallyEq f₁ f₂ → l.EventuallyEq g₁ g₂ → f₂ =o[l] g₂
This theorem states that for any types `α`, `E`, and `F` with `E` and `F` being normed, given a filter `l` and four functions `f₁`, `f₂` from `α` to `E` and `g₁`, `g₂` from `α` to `F`, if `f₁` is little o of `g₁` with respect to `l`, and `f₁` is eventually equal to `f₂` and `g₁` is eventually equal to `g₂` with respect to the same filter `l`, then `f₂` is little o of `g₂` with respect to `l`. In mathematical terms, this means that the asymptotic behavior of `f₁` and `f₂` is the same, and the same holds for `g₁` and `g₂`, then the asymptotic behavior of `f₂` and `g₂` will also be the same.
More concisely: If `f₁` is little o of `g₁` and equal to `f₂` eventually, and `g₁` is equal to `g₂` eventually with respect to filter `l`, then `f₂` is little o of `g₂` with respect to `l`.
|
Asymptotics.isBigO_of_le
theorem Asymptotics.isBigO_of_le :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
(l : Filter α), (∀ (x : α), ‖f x‖ ≤ ‖g x‖) → f =O[l] g
This theorem, `Asymptotics.isBigO_of_le`, states that for all types `α`, `E`, and `F`, where `E` and `F` are types with a norm (a function that assigns a strictly positive length or size to each vector in a vector space), and given any function `f` from `α` to `E`, and `g` from `α` to `F`, along with a filter `l` on `α`, if the norm of `f(x)` is always less than or equal to the norm of `g(x)` for every `x` in `α`, then `f` is Big O of `g` at the filter `l`. In Big O notation, this is saying that `f` grows no faster than `g`, considering the limits as `x` approaches the elements determined by the filter `l`.
More concisely: Given types `α`, `E` with a norm, functions `f: α → E` and `g: α → F` from `α` to normed types `E` and `F`, and a filter `l` on `α`, if `||f(x)|| ≤ ||g(x)||` for all `x` in `α`, then `f` is Big O of `g` at filter `l`.
|
Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.46
theorem Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.46 :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =O[l] g = ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
This theorem, `Mathlib.Analysis.Asymptotics.Asymptotics._auxLemma.46`, states that for any types `α`, `E`, and `F`, where `E` and `F` are normed, given two functions `f : α → E` and `g : α → F` and a filter `l` on `α`, the function `f` is big O of `g` at the filter `l` if and only if there exists a constant `c` such that, eventually for every `x` in the filter `l`, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`. This is a notion of limit used in analysis to describe the asymptotic behavior of functions.
More concisely: For types `α`, `E`, and `F` where `E` and `F` are normed, and for functions `f : α → E` and `g : α → F` on filter `l` on `α`, `f` is big O of `g` at `l` if and only if there exists a constant `c` such that, for all `x` in `l`, ||`f(x)`|| ≤ c * ||`g(x)`||.
|
Asymptotics.isLittleO_of_tendsto'
theorem Asymptotics.isLittleO_of_tendsto' :
∀ {α : Type u_1} {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {l : Filter α} {f g : α → 𝕜},
(∀ᶠ (x : α) in l, g x = 0 → f x = 0) → Filter.Tendsto (fun x => f x / g x) l (nhds 0) → f =o[l] g
The theorem `Asymptotics.isLittleO_of_tendsto'` states that for any types `α` and `𝕜`, where `𝕜` is a normed division ring, and for any filter `l` on `α`, along with two functions `f` and `g` both mapping from `α` to `𝕜`, if for almost all `x` in the filter `l`, the function `g` when applied to `x` gives zero implies that `f` applied to `x` is also zero, and the function mapping `x` to `f x / g x` converges to zero in the neighbourhood of zero under the filter `l`, then `f` is little o of `g` at filter `l`, represented as `f =o[l] g`.
In mathematical terms, this theorem states that if `f(x)` tends to zero whenever `g(x)` does, and the ratio `f(x) / g(x)` converges to zero, then `f(x)` is asymptotically smaller than `g(x)` as `x` approaches a certain point according to the filter `l`.
More concisely: If a function `f` tends to zero whenever another function `g` does and the quotient `f / g` converges to zero under a filter `l`, then `f` is little o of `g` at filter `l`.
|
Asymptotics.isBigO_norm_left
theorem Asymptotics.isBigO_norm_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
{f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g
This theorem, `Asymptotics.isBigO_norm_left`, states that for any types `α`, `F`, and `E'`, given a norm on `F` and `E'` being a semi-normed add commutative group, for any functions `f': α → E'` and `g: α → F`, and any filter `l` on `α`, the norm of `f'` is Big-O of `g` with respect to `l` if and only if `f'` is Big-O of `g` with respect to `l`.
In simpler terms, this theorem is about asymptotic behavior of functions. It says that a function `f'` is dominated by another function `g` (in terms of growth rates for large inputs, according to the Big-O notation) if and only if the norm of `f'` is also dominated by `g`.
More concisely: For functions `f': α → E'` and `g: α → F` between types `α`, `E'`, and `F` with `E'` being a semi-normed add commutative group, and given a norm on `F` and filter `l` on `α`, `f'` is Big-O of `g` with respect to `l` if and only if the norm of `f'` is Big-O of `g` with respect to `l`.
|
Asymptotics.IsLittleO.def'
theorem Asymptotics.IsLittleO.def' :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
{l : Filter α}, f =o[l] g → 0 < c → Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.IsLittleO.def'` states that for any positive real number `c`, if a function `f` is little-o of another function `g` at a filter `l` (written as `f =o[l] g`), then `f` is also big-O of `g` at the same filter with constant `c` (expressed as `Asymptotics.IsBigOWith c l f g`). In other words, if `f` grows no faster than `g` at `l` in the limit (ignoring a constant factor), then there exists some positive constant `c` such that `f` is bounded by `c` times `g` at `l` eventually. This theorem provides a connection between the little-o and big-O notations in asymptotic analysis. Note that the types `E` and `F` are normed spaces and `α` is the domain of the functions `f` and `g`.
More concisely: If `f = o[l] g` (little-o) holds for functions `f` and `g` in the normed spaces `E` and `F` over the domain `α` at filter `l`, then `Asymptotics.IsBigOWith c l f g` (big-O) holds for some constant `c > 0`.
|
Asymptotics.IsBigO.isBigOWith
theorem Asymptotics.IsBigO.isBigOWith :
∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
{l : Filter α}, f =O[l] g → ∃ c, Asymptotics.IsBigOWith c l f g
The theorem `Asymptotics.IsBigO.isBigOWith` states that for any two functions `f` and `g` on a type `α` with norms (`Norm E` and `Norm F` respectively) and a filter `l` on `α`, if `f` is Big O of `g` at the filter `l` (notated as `f =O[l] g`), then there exists a real number `c` such that `f` is eventually bounded by `c * ‖g‖` at the filter `l`. In other words, the ratio `‖f‖ / ‖g‖` is eventually bounded by `c`, ignoring division by zero issues. This establishes a connection between `IsBigO` and `IsBigOWith` relations in the context of asymptotic notation.
More concisely: If `f =O[l] g` for functions `f` and `g` on type `α` with norms and filter `l`, then there exists a constant `c` such that `|f(x)| ≤ c * |g(x)|` for all `x` in the filter `l`.
|
Asymptotics.IsLittleO.of_abs_abs
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
This theorem, `Asymptotics.IsLittleO.of_abs_abs`, is an alias of the forward direction of `Asymptotics.isLittleO_abs_abs`. It states that for any type `α`, any filter `l` on `α`, and any two functions `u` and `v` from `α` to the real numbers `ℝ`, if the absolute value of `u` is little-o of the absolute value of `v` (i.e., `u` grows no faster than `v` in the limit), then `u` itself is little-o of `v`. In mathematical terms, if $|u(x)| = o(|v(x)|)$ as `x` approaches a limit, then $u(x) = o(v(x))$ as `x` approaches that same limit.
More concisely: If $|u(x)| = o(|v(x)|)$ as $x$ approaches a limit, then $u(x) = o(v(x))$ as $x$ approaches that same limit.
|