Asymptotics.SuperpolynomialDecay.param_mul
theorem Asymptotics.SuperpolynomialDecay.param_mul :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
Asymptotics.SuperpolynomialDecay l k f → Asymptotics.SuperpolynomialDecay l k (k * f)
The theorem `Asymptotics.SuperpolynomialDecay.param_mul` states that for any types `α` and `β` where `β` is a commutative semiring with a topology, any filter `l` on `α`, and any functions `k` and `f` from `α` to `β`, if the function `f` has superpolynomial decay in terms of parameter `k` along filter `l`, then the function `k * f` also has superpolynomial decay in the same terms. In the context of asymptotics, superpolynomial decay means that the magnitude of `f` decreases faster than any polynomial rate of `k`. So here, even after multiplying `f` by `k`, it still satisfies the property of superpolynomial decay.
More concisely: If a function `f` from `α` to a commutative semiring `β` with a topology has superpolynomial decay in terms of parameter `k` along filter `l`, then the function `k * f` also has superpolynomial decay in the same terms.
|
Mathlib.Analysis.Asymptotics.SuperpolynomialDecay._auxLemma.2
theorem Mathlib.Analysis.Asymptotics.SuperpolynomialDecay._auxLemma.2 :
∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * (b * c) = a * b * c
This theorem, named `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay._auxLemma.2`, states that for any type `G` that forms a semigroup, the multiplication operation is associative. In simpler terms, given any three elements `a`, `b`, and `c` of type `G`, the product of `a` with the product of `b` and `c` is the same as the product of `a`, `b`, and `c` taken in a row without bracketing. It's a formal encoding of the mathematical principle that in a semigroup, the way in which we group factors in a product does not change the result, i.e., `(a * (b * c)) = ((a * b) * c)`.
More concisely: In a semigroup, the associativity of multiplication holds: `(a * (b * c)) = ((a * b) * c)` for all elements `a`, `b`, and `c`.
|
Asymptotics.SuperpolynomialDecay.congr
theorem Asymptotics.SuperpolynomialDecay.congr :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β]
[inst_1 : CommSemiring β],
Asymptotics.SuperpolynomialDecay l k f → (∀ (x : α), f x = g x) → Asymptotics.SuperpolynomialDecay l k g
The theorem `Asymptotics.SuperpolynomialDecay.congr` states that for all types `α` and `β`, a given filter `l` over `α`, functions `k`, `f`, and `g` from `α` to `β`, and for a given topological space and a commutative semiring over `β`, if the function `f` has superpolynomial decay for the parameter `k` along the filter `l`, and for every `x` of type `α`, `f x` equals `g x`, then the function `g` also has superpolynomial decay for the parameter `k` along the filter `l`. In other words, if two functions are equal for every `x` in the domain, and if one of them has superpolynomial decay, then the other one also has superpolynomial decay.
More concisely: If two functions are equal and one of them has superpolynomial decay along a filter, then the other function also has superpolynomial decay along that filter.
|