SchwartzMap.isBigO_cocompact_zpow_neg_nat
theorem SchwartzMap.isBigO_cocompact_zpow_neg_nat :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (k : ℕ),
⇑f =O[Filter.cocompact E] fun x => ‖x‖ ^ (-↑k)
This theorem, `SchwartzMap.isBigO_cocompact_zpow_neg_nat`, states that for any Schwartz map `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, both of which are also normed spaces over the real numbers, and for any natural number `k`, the function `f` is big-O of the function that sends `x` to the norm of `x` raised to the power of negative `k` with respect to the filter `Filter.cocompact E`. In other words, `f` grows no faster than the function `x` maps to `‖x‖^(-k)` when considering sequences that converge to points not in compact subsets of `E`.
More concisely: For any Schwartz map `f` from a normed additive commutative group `E` to another normed additive commutative group `F`, and any natural number `k`, `f` is big-O of the function `x ↦ ‖x‖^(-k)` with respect to the filter of cocompact sets in `E`.
|
SchwartzMap.seminormAux_nonneg
theorem SchwartzMap.seminormAux_nonneg :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F),
0 ≤ SchwartzMap.seminormAux k n f
This theorem states that for any Schwartz map `f` from a real normed space `E` to another real normed space `F` (with `E` and `F` both being normed additive commutative groups), and for any non-negative integers `k` and `n`, the auxiliary seminorm of the Schwartz map `f`, denoted by `SchwartzMap.seminormAux k n f`, is always non-negative. In other words, the auxiliary seminorm of a Schwartz map is always a non-negative real number.
More concisely: For any Schwartz map from a real normed space to another real normed space, the auxiliary seminorm is non-negative for all non-negative integers.
|
SchwartzMap.continuous
theorem SchwartzMap.continuous :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F), Continuous ⇑f
This theorem states that every Schwartz function is continuous. Here, a Schwartz function, denoted as `f : SchwartzMap E F`, is a type of function between two normed spaces `E` and `F` over the real numbers. The spaces `E` and `F` are assumed to be normed add commutative groups. Therefore, for any Schwartz function `f`, the function application `⇑f` (i.e., applying `f` to its arguments) is guaranteed to be continuous.
More concisely: Every Schwartz function between two normed spaces is continuous.
|
SchwartzMap.seminorm_le_bound'
theorem SchwartzMap.seminorm_le_bound' :
∀ (𝕜 : Type u_1) {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : NormedField 𝕜]
[inst_3 : NormedSpace 𝕜 F] [inst_4 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap ℝ F) {M : ℝ},
0 ≤ M → (∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M) → (SchwartzMap.seminorm 𝕜 k n) f ≤ M
This theorem, `SchwartzMap.seminorm_le_bound'`, states that for every type 𝕜, a normed additive commutative group F, a normed space over the reals for F, a normed field 𝕜, a normed space over 𝕜 for F, and a commutative multiplication action of ℝ on 𝕜 for F, and every integer values k and n, there exists a Schwartz map from ℝ to F and a non-negative real number M, such that if the absolute value of x raised to the kth power times the norm of the nth iterated derivative of the function at x is less than or equal to M for all x, then the Schwartz seminorm of the function with respect to 𝕜, k, and n is less than or equal to M.
In simpler terms, this theorem states that if we have a bound on the seminorm for every input to a Schwartz function, then we have a bound on the seminorm of the function itself.
More concisely: For any normed additive commutative group F, normed space X over the reals for F, normed field 𝕜 over F, commutative multiplication action of ℝ on 𝕜 for F, integers k and n, there exists a Schwartz map f from ℝ to F and a non-negative real number M, such that |x|^k situation norm(f^(n)''(x)) ≤ M implies situation norm(f, k, n) ≤ M.
|
schwartz_withSeminorms
theorem schwartz_withSeminorms :
∀ (𝕜 : Type u_1) (E : Type u_4) (F : Type u_5) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
[inst_6 : SMulCommClass ℝ 𝕜 F], WithSeminorms (schwartzSeminormFamily 𝕜 E F)
This theorem, `schwartz_withSeminorms`, states that for any type `𝕜` that is a normed field, as well as any types `E` and `F` that are both normed vector spaces over ℝ with an additional normed space structure over `𝕜` for `F`, the family of Schwartz seminorms (represented by `schwartzSeminormFamily 𝕜 E F`) satisfies the property of having seminorms. Here, the `WithSeminorms` property is a characteristic of a seminorm family, indicating that it indeed consists of seminorms. The `SMulCommClass ℝ 𝕜 F` instance asserts that scalar multiplication in `F` is commutative when the scalars are real numbers or elements of `𝕜`.
More concisely: For a normed field `𝕜` and normed vector spaces `E` and `F` over `ℝ` with additional `𝕜`-normed structure on `F`, the family of Schwartz seminorms `schwartzSeminormFamily 𝕜 E F` satisfies the seminorm property and is commutative with respect to scalar multiplication by real numbers or elements of `𝕜` in `F`.
|
SchwartzMap.le_seminorm
theorem SchwartzMap.le_seminorm :
∀ (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
[inst_6 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap E F) (x : E),
‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
This theorem, named `SchwartzMap.le_seminorm`, states the following: for any given type `𝕜`, and normed add commutative groups `E` and `F` with their normed spaces over ℝ, a normed field structure on `𝕜`, a normed space structure on `𝕜` over `F`, and a real-`𝕜`-`F` scalar multiplication commutation relation, for any given natural numbers `k` and `n`, any Schwartz Map `f` from `E` to `F`, and any element `x` from `E`, the `k`-th power of the norm of `x` times the norm of the `n`-th iterated Frechet derivative of `f` at `x` is always less than or equal to the `k`-th, `n`-th seminorm of `f`. This means that the seminorm of the Schwartz map can be used as an upper bound for the product of the `k`-th power of the norm of `x` and the norm of the `n`-th iterated Frechet derivative of the map at `x`.
More concisely: For any Schwartz Map `f` from a normed space `E` to another normed space `F` over a field `𝕜`, and for any `x` in `E`, `k` natural numbers, and `n` positive integers, the `k`-th power of the norm of `x` times the norm of the `n`-th Frechet derivative of `f` at `x` is less than or equal to the `k`-th, `n`-th seminorm of `f` on `x`.
|
SchwartzMap.le_seminormAux
theorem SchwartzMap.le_seminormAux :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) (x : E),
‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ SchwartzMap.seminormAux k n f
This theorem states that, for any normed additively commutative groups E and F, which are also normed spaces over the real numbers, given any two natural numbers `k` and `n`, and a SchwartzMap `f` from E to F, the product of the `k`-th power of the norm of any element `x` in E and the norm of the `n`-th iterated Fréchet derivative of `f` at `x`, is less than or equal to the `k`-th and `n`-th seminorm of `f` in the Schwartz space.
More concisely: For any SchwartzMap `f` between normed additively commutative groups E and F over the real numbers, and for all `x` in E, `k` in ℕ, and `n` in ℕ, the `k`-th power of the norm of `x` times the norm of the `n`-th Fréchet derivative of `f` at `x` is bounded above by the `k`-th seminorm and the `n`-th norm of `f`.
|
SchwartzMap.one_add_le_sup_seminorm_apply
theorem SchwartzMap.one_add_le_sup_seminorm_apply :
∀ {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
[inst_6 : SMulCommClass ℝ 𝕜 F] {m : ℕ × ℕ} {k n : ℕ},
k ≤ m.1 →
n ≤ m.2 →
∀ (f : SchwartzMap E F) (x : E),
(1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
The theorem `SchwartzMap.one_add_le_sup_seminorm_apply` states that for any Schwartz Map `f` from a normed commutative additive group `E` to another `F`, both of which have a real number space structure, and for `F` additionally having a normed field `𝕜` space structure, the norm of the `n`th iterated Frechet derivative of `f` at a point `x` in `E`, multiplied by `(1 + norm(x))^k` is less than or equal to `2^(m.1)` times the supremum of the seminorm over the set `Finset.Iic m` (which contains all pairs `(k', n')` such that `k' ≤ m.1` and `n' ≤ m.2`). This holds true for any natural numbers `k` and `n` such that `k ≤ m.1` and `n ≤ m.2`. The theorem notes that the constant `2^(m.1)` is not necessarily the smallest possible.
More concisely: For any Schwartz Map `f` from a normed commutative additive group `E` to another `F` with real and normed field structures, the norm of the `n`th Frechet derivative of `f` at `x` in `E`, multiplied by `(1 + ||x||)^k`, is bounded by `2^(m.1)` times the supremum of the seminorm of `f` over `Finset.Iic m`.
|
SchwartzMap.seminormAux_le_bound
theorem SchwartzMap.seminormAux_le_bound :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) {M : ℝ},
0 ≤ M → (∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M) → SchwartzMap.seminormAux k n f ≤ M
The theorem `SchwartzMap.seminormAux_le_bound` states that for any normed additive commutative groups `E` and `F` over real numbers, given any Schwartz Map `f` from `E` to `F`, and any nonnegative integers `k` and `n`, if there exists a nonnegative real number `M` such that the norm of `x` raised to the power of `k` multiplied by the norm of the `n`-th iterated Frechet derivative of `f` at `x` is always less than or equal to `M` for every `x` in `E`, then the seminorm of `f` calculated by the auxiliary function `SchwartzMap.seminormAux` with parameters `k` and `n` is also less than or equal to `M`. This means that if we can control the norms of the iterated derivatives of `f` at every point, then we can control the seminorm of `f` itself.
More concisely: If for all x in a normed additive commutative group E and nonnegative integers k and n, the norm of x raised to the power of k times the norm of the n-th iterated Frechet derivative of a Schwartz Map f from E to another normed additive commutative group F at x is bounded by a constant M, then the seminorm of f using SchwartzMap.seminormAux with parameters k and n is also bounded by M.
|
SchwartzMap.differentiable
theorem SchwartzMap.differentiable :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F), Differentiable ℝ ⇑f
The theorem "SchwartzMap.differentiable" states that every Schwartz function is differentiable. In more detail, given any Schwartz function 'f' that maps from a normed additive commutative group 'E' with a real-valued normed space, to another normed additive commutative group 'F' with a real-valued normed space, the function 'f' is differentiable at every point in its domain 'E'. This means that for every point in 'E', the limit of the difference quotient of 'f' exists, implying that 'f' has a derivative at that point.
More concisely: Every Schwartz function between two real normed spaces is differentiable at every point in its domain.
|
SchwartzMap.le_seminorm'
theorem SchwartzMap.le_seminorm' :
∀ (𝕜 : Type u_1) {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : NormedField 𝕜]
[inst_3 : NormedSpace 𝕜 F] [inst_4 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap ℝ F) (x : ℝ),
|x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
This theorem, named `SchwartzMap.le_seminorm'`, states that for any types 𝕜 and F, where F is a Normed Additive Commutative Group and a Normed Space over ℝ and 𝕜, and 𝕜 is a Normed Field, and the multiplication operation is commutative between ℝ and 𝕜 on F, for any natural numbers k and n, any Schwartz Map `f` from ℝ to F, and any real number `x`, the absolute value of `x` raised to the power of `k` times the seminorm of the `n`-th iterated derivative of the function `f` at `x` is less than or equal to the seminorm of the Schwartz Map for `f`. This is a variant for functions `𝓢(ℝ, F)`, asserting that the seminorm controls the Schwartz estimate for any fixed `x`.
More concisely: For any Schwartz Map $f$ from $\mathbb{R}$ to a Normed Additive Commutative Group and Normed Space $F$ over $\mathbb{R}$ and $\mathbb{R}$, where $\mathbb{R}$ is a Normed Field and multiplication is commutative between $\mathbb{R}$ and $F$, and for any natural numbers $k$, $n$, and real number $x$, $|x|^k \cdot ||f^{(n)}(x)|| \leq ||f||$.
|
SchwartzMap.differentiableAt
theorem SchwartzMap.differentiableAt :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) {x : E},
DifferentiableAt ℝ (⇑f) x
The theorem `SchwartzMap.differentiableAt` states that for any Schwartz function `f` mapping from a type `E` to a type `F` (where both `E` and `F` form a normed additive commutative group over the real numbers), the function `f` is differentiable at any point `x` in `E`. In mathematical terms, if `f` is a Schwartz function from a normed space `E` to a normed space `F`, then there exists a derivative of `f` at each point in `E`.
More concisely: Every Schwartz function from a normed additive commutative group `E` to a normed additive commutative group `F` over the real numbers is differentiable at every point in `E`.
|
SchwartzMap.seminorm_le_bound
theorem SchwartzMap.seminorm_le_bound :
∀ (𝕜 : Type u_1) {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
[inst_6 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap E F) {M : ℝ},
0 ≤ M → (∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M) → (SchwartzMap.seminorm 𝕜 k n) f ≤ M
This theorem states that if you can control the seminorm of each element `x` from a normed space `E`, then you can control the seminorm of the whole space. More precisely, given a Schwartz map `f` from `E` to `F` (where both `E` and `F` are normed spaces), a non-negative real number `M`, and integers `k` and `n`, if for every `x` in `E` the product of `k`-th power of the norm of `x` and the norm of the `n`-th iterated Frechet derivative of `f` at `x` is less than or equal to `M`, then the seminorm of the Schwartz map `f` (with respect to the semiring `𝕜`, the integer `k`, and the integer `n`) is also less than or equal to `M`.
More concisely: If for all x in a normed space E, the product of the k-th power of the norm of x and the norm of the n-th Frechet derivative of a Schwartz map f from E to another normed space F at x is less than or equal to M, then the seminorm of f is less than or equal to M.
|
SchwartzMap.decay
theorem SchwartzMap.decay :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (k n : ℕ),
∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
This theorem states that for any Schwartz function `f` mapping from a normed additive commutative group `E` to another `F` (both also being normed spaces over the Reals), all of its derivatives are rapidly decaying. More formally, for any non-negative integers `k` and `n`, there exists a positive constant `C` such that for all `x` in `E`, the `k`-th power of the norm of `x` multiplied by the norm of the `n`-th derivative of `f` at `x` is less than or equal to `C`. This demonstrates that the rate of decay of the derivatives of a Schwartz function increases rapidly as `x` grows.
More concisely: For any Schwartz function `f` from a normed additive commutative group `E` to another normed space `F` over the Reals, the norms of its derivatives rapidly decay, i.e., for all non-negative integers `k` and `n`, there exists a constant `C` such that `∥x∥^k ∥f^(n)(x)∥ <= C` for all `x` in `E`.
|
SchwartzMap.smooth
theorem SchwartzMap.smooth :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (n : ℕ∞), ContDiff ℝ n ⇑f
This theorem states that every Schwartz function is smooth, which means it is infinitely differentiable. In more detail, for any types `E` and `F` (where `E` and `F` are normed additive commutative groups and normed spaces over the real numbers), and for any function `f` that is a Schwartz map from `E` to `F`, the function `f` is continuously differentiable at any order `n`, where `n` is a natural number or infinity.
More concisely: Every Schwartz function is infinitely differentiable.
|