Asymptotics.IsTheta.symm
theorem Asymptotics.IsTheta.symm :
∀ {α : 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 =Θ[l] g → g =Θ[l] f
This theorem states that for any given types `α`, `E`, and `F`, if `f` (a function from `α` to `E`) is theta (`=Θ`) of `g` (a function from `α` to `F`) at a certain filter `l`, then `g` is also theta of `f` at the same filter. In other words, the 'theta notation', which in this context represents asymptotic equivalence, is symmetric. This means if `f` grows at the same rate as `g` under some conditions defined by `l`, then `g` also grows at the same rate as `f` under those conditions.
More concisely: If `f` is theta equal to `g` at filter `l` in types `α`, `E`, and `F`, then `g` is theta equal to `f` at the same filter `l`.
|
Asymptotics.isTheta_const_smul_right
theorem Asymptotics.isTheta_const_smul_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
[inst_2 : NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : NormedSpace 𝕜 F'] {c : 𝕜},
c ≠ 0 → ((f =Θ[l] fun x => c • g' x) ↔ f =Θ[l] g')
This theorem states that for any types `α`, `E`, `F'`, `𝕜` and any functions `f : α → E` and `g' : α → F'`, if `𝕜` is a normed field, `E` is a normed space, `F'` is a seminormed additive commutative group, and `c` is a non-zero scalar in `𝕜`, then `f` is asymptotically equivalent to `c` times `g'` with respect to a filter `l` if and only if `f` is asymptotically equivalent to `g'` with respect to the same filter `l`. Here, "asymptotically equivalent" means that the ratio of `f` and `g'` (or `f` and `c • g'`) tends towards 1 as we follow the filter `l`.
More concisely: For types `α`, `E`, `F'`, `𝕜`, functions `f : α → E`, `g' : α → F'`, and a non-zero scalar `c` in a normed field `𝕜`, `f` is asymptotically equivalent to `c` times `g'` with respect to a filter `l` if and only if `f` is asymptotically equivalent to `g'` with respect to `l`. (Here, "asymptotically equivalent" refers to the ratio of `f` and `g'` or `f` and `c` times `g'` approaching 1 as the filter `l` is followed.)
|
Asymptotics.IsTheta.const_mul_right
theorem Asymptotics.IsTheta.const_mul_right :
∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : NormedField 𝕜] {f : α → E} {l : Filter α}
{c : 𝕜} {g : α → 𝕜}, c ≠ 0 → f =Θ[l] g → f =Θ[l] fun x => c * g x
The theorem `Asymptotics.IsTheta.const_mul_right` states that, for any types `α` (input to the functions), `E` (output of the function `f`), `𝕜` (output of function `g` and type of the constant `c`), a norm on `E`, a normed field on `𝕜`, any function `f : α → E`, a filter `l` on `α`, a non-zero constant `c : 𝕜`, and a function `g : α → 𝕜`, if `f` is asymptotically equivalent to `g` at the filter `l`, then `f` is also asymptotically equivalent to the function `(x => c * g x)` at the same filter `l`. Asymptotically equivalent here means that the functions grow at the same rate as the input approaches some limit (denoted by the filter `l`).
More concisely: If `f` is asymptotically equivalent to `g` at filter `l`, then `f` is also asymptotically equivalent to `(x => c * g x)` at filter `l`, for any constant `c` and normed field `𝕜`.
|
Asymptotics.IsTheta.of_const_smul_left
theorem Asymptotics.IsTheta.of_const_smul_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
[inst_2 : NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : NormedSpace 𝕜 E'] {c : 𝕜},
c ≠ 0 → (fun x => c • f' x) =Θ[l] g → f' =Θ[l] g
This theorem, which is an alias for the forward direction of `Asymptotics.isTheta_const_smul_left`, states that for any types `α`, `F`, `E'`, `𝕜` and any functions `f'` and `g` from `α` to `F` and `E'` respectively, along with a filter `l` on `α`, and a constant `c` from the normed field `𝕜`; if `c` is not zero and the function that maps `x` to `c` times `f'(x)` is "big Theta" of `g` at `l` (i.e., the two functions are asymptotically equivalent), then `f'` is also "big Theta" of `g` at `l`. In other words, if `c • f'(x)` and `g(x)` grow at the same rate for large `x` (within the filter `l`), then `f'(x)` and `g(x)` also grow at the same rate, regardless of the non-zero constant factor `c`.
More concisely: If a constant times a function is big Theta of another function at a filter, then the function is also big Theta of the other function at that filter (up to a constant factor).
|
Asymptotics.IsTheta.of_const_mul_right
theorem Asymptotics.IsTheta.of_const_mul_right :
∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : NormedField 𝕜] {f : α → E} {l : Filter α}
{c : 𝕜} {g : α → 𝕜}, c ≠ 0 → (f =Θ[l] fun x => c * g x) → f =Θ[l] g
This theorem, `Asymptotics.IsTheta.of_const_mul_right`, is an alias of the forward direction of `Asymptotics.isTheta_const_mul_right`. It states that for any types `α`, `E`, and `𝕜`, with `E` being a normed space, `𝕜` a normed field, a filter `l` on `α`, functions `f` from `α` to `E` and `g` from `α` to `𝕜`, and a non-zero constant `c` in `𝕜`, if `f` is asymptotically equivalent to `c * g` under filter `l`, then `f` is also asymptotically equivalent to `g` under the same filter. In simpler terms, if `f` grows at the same rate as `c * g` as `x` approaches a limit, then `f` also grows at the same rate as `g`, regardless of the non-zero constant `c`.
More concisely: If a function `f` is asymptotically equivalent to the product of a constant `c` and another function `g` as `x` approaches a limit, then `f` is asymptotically equivalent to `g`.
|
Asymptotics.isTheta_const_smul_left
theorem Asymptotics.isTheta_const_smul_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
[inst_2 : NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : NormedSpace 𝕜 E'] {c : 𝕜},
c ≠ 0 → ((fun x => c • f' x) =Θ[l] g ↔ f' =Θ[l] g)
This theorem states that, for all types `α`, `F`, `E'`, and `𝕜`, given a norm on `F`, a seminorm on `E'`, a normed field `𝕜`, functions `g : α → F` and `f' : α → E'`, a filter `l` on `α`, and a normed space `𝕜` over `E'`, and a constant `c : 𝕜` such that `c` is not equal to zero, then the function that maps `x` to `c` multiplies `f'(x)` is Big Theta (`=Θ`) of `g` with respect to the filter `l` if and only if `f'` is Big Theta of `g` with respect to `l`. In simpler terms, if you have a function `f'` and you scale it by a non-zero constant `c`, it has the same order of growth as `g` if and only if the original function `f'` has the same order of growth as `g`.
More concisely: For all types `α`, `F`, `E'`, and normed fields `𝕜`, if `c` is a non-zero constant, `g : α → F`, `f' : α → E'`, and `f' ∝ g` (Big Theta relation) with respect to a filter `l` on `α` holds, then `cf' ∝ g` (Big Theta relation) also holds.
|
Asymptotics.IsTheta.of_norm_left
theorem Asymptotics.IsTheta.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‖) =Θ[l] g → f' =Θ[l] g
This theorem, **Alias of the forward direction of `Asymptotics.isTheta_norm_left`**, states that for all types `α`, `F`, `E'` and for all functions `f' : α → E'` and `g : α → F`, and for any filter `l : Filter α`, if the norm of `f'` (denoted as `‖f' x‖` for all `x` in `α`) is asymptotically equivalent to `g` (denoted as `(fun x => ‖f' x‖) =Θ[l] g`), then `f'` itself is also asymptotically equivalent to `g` (denoted as `f' =Θ[l] g`). Asymptotic equivalence, denoted as `=Θ`, means that the two functions behave similarly for large input values, according to the provided filter `l`. The theorem is a part of the asymptotics theory, which is used in mathematical analysis and number theory.
More concisely: If the norm of a function `f'` is asymptotically equivalent to another function `g` with respect to a filter `l`, then `f'` itself is asymptotically equivalent to `g` with respect to the same filter.
|
Asymptotics.IsTheta.of_norm_right
theorem Asymptotics.IsTheta.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 =Θ[l] fun x => ‖g' x‖) → f =Θ[l] g'
This theorem, `Asymptotics.IsTheta.of_norm_right`, is an alias for the forward direction of `Asymptotics.isTheta_norm_right`. It states that for any types `α`, `E`, and `F'`, the norm of `E`, a seminormed addition commutative group `F'`, a function `f` from `α` to `E`, another function `g'` from `α` to `F'`, and a filter `l` on `α`, if `f` is asymptotically equivalent to the norm of `g'` (denoted as `f =Θ[l] fun x => ‖g' x‖`), then `f` is also asymptotically equivalent to `g'` (denoted as `f =Θ[l] g'`). Asymptotic equivalence is a concept in mathematics that describes the limiting behavior of functions.
More concisely: If a function `f` is asymptotically equivalent to the norm of another function `g'` with respect to a filter `l`, then `f` is also asymptotically equivalent to `g'` in the same sense.
|
Asymptotics.IsTheta.const_smul_right
theorem Asymptotics.IsTheta.const_smul_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
[inst_2 : NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : NormedSpace 𝕜 F'] {c : 𝕜},
c ≠ 0 → f =Θ[l] g' → f =Θ[l] fun x => c • g' x
This theorem, `Asymptotics.IsTheta.const_smul_right`, is an alias for the reverse direction of `Asymptotics.isTheta_const_smul_right`. It states that for any types `α`, `E`, `F'`, and `𝕜`, given a norm on `E`, a semi-normed additive commutative group structure on `F'`, a normed field structure on `𝕜`, a function `f : α → E`, a function `g' : α → F'`, a filter `l` on `α`, a normed space structure over `F'` with scalar field `𝕜`, and a non-zero constant `c` of type `𝕜`, if `f` is theta equivalent to `g'` under the filter `l`, then `f` is also theta equivalent to `c • g'(x)` under the same filter, where `c • g'(x)` is the scalar multiplication of `c` and `g'(x)`. The theta equivalence, denoted as `=Θ[l]`, typically expresses that two functions have the same big Theta order of growth.
More concisely: If `f` is Theta equivalent to `g'` under filter `l` in Lean 4, then `f` is also Theta equivalent to `c * g'` under the same filter for any non-zero constant `c`.
|
Asymptotics.IsTheta.of_const_mul_left
theorem Asymptotics.IsTheta.of_const_mul_left :
∀ {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : NormedField 𝕜] {g : α → F} {l : Filter α}
{c : 𝕜} {f : α → 𝕜}, c ≠ 0 → (fun x => c * f x) =Θ[l] g → f =Θ[l] g
This theorem, `Asymptotics.IsTheta.of_const_mul_left`, states that for any types `α`, `F`, and `𝕜`, given that `𝕜` forms a normed field, `F` has a norm, and `g` and `f` are functions of type `α → F` and `α → 𝕜` respectively, if `c` is a non-zero constant in `𝕜` and the function `c * f(x)` is asymptotically equivalent to `g(x)` with respect to a certain filter `l`, then `f(x)` itself is also asymptotically equivalent to `g(x)` with respect to the same filter. Essentially, it says that if a function is asymptotically equivalent to a scaled version of another function, then the two functions are also asymptotically equivalent themselves when the scaling constant is non-zero.
More concisely: If `c` is a non-zero constant in a normed field `𝕜`, and `c * f(x)` is asymptotically equivalent to `g(x)` as `x` approaches some limit with respect to a filter `l`, then `f(x)` is also asymptotically equivalent to `g(x)` with respect to `l`.
|
Asymptotics.IsLittleO.trans_isTheta
theorem Asymptotics.IsLittleO.trans_isTheta :
∀ {α : 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 =Θ[l] k → f =o[l] k
This theorem states that for any types `α`, `E`, `F`, `G'` and any functions `f : α → E`, `g : α → F`, `k : α → G'` with respect to a filter `l`, if `f` is little-o of `g` and `g` is Theta of `k`, then `f` is little-o of `k`. Here, little-o (`f =o[l] g`) means `f` grows no quicker than `g` and Theta (`g =Θ[l] k`) means `g` grows at the same rate as `k`, in an asymptotic sense. The necessary conditions are that `E` and `F` are normed and `G'` is a seminormed additive commutative group.
More concisely: If `f : α → E`, `g : α → F`, and `k : α → G'` are functions, `α` is any type, `E` and `F` are normed types, `G'` is a seminormed additive commutative group, `l` is a filter, `f =o[l] g` (`f` is little-o of `g`), and `g =Θ[l] k` (`g` is Theta of `k`), then `f =o[l] k` (`f` is little-o of `k`).
|
Asymptotics.IsTheta.norm_right
theorem Asymptotics.IsTheta.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 =Θ[l] g' → f =Θ[l] fun x => ‖g' x‖
This theorem, `Asymptotics.IsTheta.norm_right`, is an alias of the reverse direction of `Asymptotics.isTheta_norm_right`. It states that for all types `α`, `E`, and `F'`, where `E` has a norm and `F'` is a semi-normed add commutative group, if a function `f` from `α` to `E` is asymptotically equal (`=Θ`) to another function `g'` from `α` to `F'` under a filter `l`, then `f` is also asymptotically equal to the function that maps each `x` in `α` to the norm of `g'(x)`. In mathematical terms, if $f(x) = Θ(g'(x))$ as $x$ approaches a point (defined by the filter `l`), then $f(x) = Θ(‖g'(x)‖)$.
More concisely: If a function `f` from type `α` to normed type `E` is asymptotically equal to a function `g'` from `α` to semi-normed add commutative group `F'` under filter `l`, then `f` is asymptotically equal to the function mapping `x` to the norm of `g'(x)`. In symbols, `f =ᵢᵃᵇ g' ∘ norm_on ∣ₕ l` implies `f =ᵢᵃᵇ (λ x => ‖g'(x)‖)`.
|
Asymptotics.IsTheta.isBigO_congr_left
theorem Asymptotics.IsTheta.isBigO_congr_left :
∀ {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [inst : Norm G] [inst_1 : SeminormedAddCommGroup E']
[inst_2 : SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α},
f' =Θ[l] g' → (f' =O[l] k ↔ g' =O[l] k)
This theorem states that for any types `α`, `G`, `E'`, and `F'`, with `G` being a normed space and `E'` and `F'` being seminormed additive commutative groups, and given a filter `l` on `α`, and functions `k : α → G`, `f' : α → E'`, and `g' : α → F'`, if `f'` and `g'` are asymptotically equivalent, then `f'` is big O of `k` under the filter `l` if and only if `g'` is big O of `k` under the same filter.
In simpler terms, if two functions are asymptotically equivalent (they have the same growth rate), then any function that bounds one in the big O notation also bounds the other.
More concisely: For types `α`, `G` (a normed space), `E'`, and `F'` (seminormed additive commutative groups), if `f'` and `g'` are asymptotically equivalent functions from `α` to `E'` and `F'` respectively, then `f'` is big O of `k` under filter `l` if and only if `g'` is big O of `k` under the same filter.
|
Asymptotics.IsTheta.inv
theorem Asymptotics.IsTheta.inv :
∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
{f : α → 𝕜} {g : α → 𝕜'}, f =Θ[l] g → (fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹
This theorem states that for any types `α`, `𝕜`, and `𝕜'`, and given that `𝕜` and `𝕜'` are normed fields, for any filter `l` of type `α`, and functions `f : α → 𝕜` and `g : α → 𝕜'`, if `f` and `g` are asymptotically equivalent at `l` (i.e., `f =Θ[l] g`), then the functions defined by the reciprocals of `f` and `g` (i.e., `(fun x => (f x)⁻¹)` and `(fun x => (g x)⁻¹)`) are also asymptotically equivalent at `l`. In other words, the asymptotic equivalence relationship is preserved under taking reciprocals of the functions.
More concisely: If `f` and `g` are asymptotically equivalent functions from type `α` to normed fields `𝕜` and `𝕜'`, respectively, then the reciprocal functions `(fun x => (f x)⁻¹)` and `(fun x => (g x)⁻¹)` are asymptotically equivalent at any filter `l` on `α`.
|
Asymptotics.IsTheta.const_mul_left
theorem Asymptotics.IsTheta.const_mul_left :
∀ {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : NormedField 𝕜] {g : α → F} {l : Filter α}
{c : 𝕜} {f : α → 𝕜}, c ≠ 0 → f =Θ[l] g → (fun x => c * f x) =Θ[l] g
This theorem, `Asymptotics.IsTheta.const_mul_left`, is an alias of the reverse direction of `Asymptotics.isTheta_const_mul_left`. It states that for any types `α`, `F`, and `𝕜`, in which `F` is a norm and `𝕜` is a normed field, along with a function `g` from `α` to `F`, a filter `l` on `α`, a constant `c` of type `𝕜`, and a function `f` from `α` to `𝕜` such that `c` is not zero and `f` is Theta-equivalent to `g` with respect to filter `l`, the function that maps each `x` in `α` to `c * f(x)` is also Theta-equivalent to `g` with respect to the same filter `l`. In other words, if `f` and `g` grow at the same rate, then scaling `f` by a nonzero constant `c` does not change its growth rate relative to `g`.
More concisely: If `f : α -> 𝕜` is Theta-equivalent to `g : α -> F` with respect to filter `l` on `α`, then `c * f` is Theta-equivalent to `g` with respect to `l` for any constant `c` in the normed field `𝕜` not equal to zero.
|
Asymptotics.IsTheta.const_smul_left
theorem Asymptotics.IsTheta.const_smul_left :
∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
[inst_2 : NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : NormedSpace 𝕜 E'] {c : 𝕜},
c ≠ 0 → f' =Θ[l] g → (fun x => c • f' x) =Θ[l] g
This is an alias for the reverse direction of the theorem `Asymptotics.isTheta_const_smul_left`. It states that for any types `α`, `F`, `E'`, and `𝕜`, given that `F` is a normed space, `E'` is a seminormed additive commutative group, `𝕜` is a normed field, `g` is a function from `α` to `F`, `f'` is a function from `α` to `E'`, `l` is a filter on `α`, `E'` is a normed space over `𝕜`, and `c` is a constant in `𝕜` that is not zero, if `f'` is asymptotically equivalent to `g` as `x` approaches `l`, then the function obtained by scaling `f'` by `c`, i.e., the function `(fun x => c • f' x)`, is also asymptotically equivalent to `g` as `x` approaches `l`.
More concisely: If `f': α -> E'` is asymptotically equivalent to `g: α -> F` as `x` approaches `l`, then the scaled function `c • f': α -> E'` is also asymptotically equivalent to `g` as `x` approaches `l`, where `α` is a type, `F` and `E'` are normed spaces, `𝕜` is a normed field, `g` and `f'` are functions from `α` to `F` and `E'` respectively, `l` is a filter on `α`, and `c` is a non-zero constant in `𝕜`.
|
Asymptotics.isTheta_refl
theorem Asymptotics.isTheta_refl :
∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] (f : α → E) (l : Filter α), f =Θ[l] f
This theorem, `Asymptotics.isTheta_refl`, states that for any function `f` from a type `α` to a normed space `E`, and for any filter `l` on `α`, the function `f` is asymptotically equivalent to itself. In more mathematical terms, this means that the function `f` has the same asymptotic behavior as itself when we approach the points determined by the filter `l`. This is a reflexivity property in the context of asymptotic equivalence.
More concisely: For any function `f : α → E` and filter `l` on `α`, `f` is asymptotically equivalent to itself, i.e., `Asymptotics.isTheta f l f`.
|
Asymptotics.IsTheta.trans
theorem Asymptotics.IsTheta.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 =Θ[l] g → g =Θ[l] k → f =Θ[l] k
The theorem `Asymptotics.IsTheta.trans` states that, given certain types `α`, `E`, `G`, and `F'` with `E`, `G` and `F'` having norms and `F'` also being a seminormed additive commutative group, and given a filter `l` and functions `f : α → E`, `g : α → F'`, and `k : α → G`, if `f` is asymptotically equivalent to `g` with respect to filter `l` and `g` is asymptotically equivalent to `k` also with respect to filter `l`, then `f` is also asymptotically equivalent to `k` with respect to filter `l`. This is essentially a statement of the transitivity of the asymptotic equivalence relation.
More concisely: If `f` is asymptotically equivalent to `g` and `g` is asymptotically equivalent to `k` with respect to filter `l`, then `f` is asymptotically equivalent to `k` with respect to filter `l`.
|
Asymptotics.IsTheta.norm_left
theorem Asymptotics.IsTheta.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' =Θ[l] g → (fun x => ‖f' x‖) =Θ[l] g
The theorem `Asymptotics.IsTheta.norm_left` is an alias of the reverse direction of the theorem `Asymptotics.isTheta_norm_left`. It states that for any types `α`, `F`, and `E'`, with `F` having a norm structure and `E'` having a seminormed add commutative group structure, and for any functions `f' : α → E'` and `g : α → F`, and any filter `l` on `α`, if function `f'` is asymptotically equivalent to function `g` with respect to filter `l`, then the function that maps `x` in `α` to the norm of `f' x` is also asymptotically equivalent to function `g` with respect to the same filter `l`.
More concisely: If a function `f'` is asymptotically equivalent to function `g` with respect to filter `l`, then the function mapping `x` to the norm of `f' x` in `E'` is asymptotically equivalent to `g` with respect to `l` in `F`.
|
Asymptotics.IsTheta.of_const_smul_right
theorem Asymptotics.IsTheta.of_const_smul_right :
∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
[inst_2 : NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : NormedSpace 𝕜 F'] {c : 𝕜},
c ≠ 0 → (f =Θ[l] fun x => c • g' x) → f =Θ[l] g'
This theorem, `Asymptotics.IsTheta.of_const_smul_right`, is an alias of the forward direction of `Asymptotics.isTheta_const_smul_right`. It states that for all types `α`, `E`, `F'`, and `𝕜`, and for all functions `f : α → E` and `g' : α → F'` on a given filter `l`, if `f` is asymptotically equivalent to the function `x → c • g'(x)` (where `c` is a non-zero element of type `𝕜` and `•` denotes scalar multiplication), then `f` is also asymptotically equivalent to `g'`. The types `E` and `𝕜` are endowed with a norm, `F'` is a seminormed additive commutative group, and `𝕜` is a normed field. Furthermore, `F'` is a normed space over `𝕜`.
More concisely: If a function `f : α → E` is asymptotically equivalent to `c • g' : α → F'` (for some non-zero `c : 𝕜` and `g' : α → F'`), where `E` and `𝕜` are normed fields, `F'` is a normed semigroup, and `F'` is a normed space over `𝕜`, then `f` is asymptotically equivalent to `g'`.
|