ContDiffWithinAt.contDiffBump
theorem ContDiffWithinAt.contDiffBump :
∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup X] [inst_3 : NormedSpace ℝ X] [inst_4 : HasContDiffBump E] {n : ℕ∞} {c g : X → E}
{s : Set X} {f : (x : X) → ContDiffBump (c x)} {x : X},
ContDiffWithinAt ℝ n c s x →
ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x →
ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x →
ContDiffWithinAt ℝ n g s x → ContDiffWithinAt ℝ n (fun x => ↑(f x) (g x)) s x
This theorem states that for any types `E` and `X` where `E` and `X` are normed additive commutative groups and normed spaces over the real numbers, and `E` has a continuous differentiable bump, and for any extended natural number `n`, functions `c` and `g` from `X` to `E`, a set `s` of type `X`, a function `f` from `X` to a continuous differentiable bump of `c(x)`, and an element `x` of `X`, if the functions `c`, `rIn` of `f(x)`, and `rOut` of `f(x)`, and `g` are `n`-times continuously differentiable at `x` within the set `s`, then the function `f(x)` applied to `g(x)` is also `n`-times continuously differentiable at `x` within the set `s`. Here, `ContDiffWithinAt` is a predicate that states a function is continuously differentiable to some order within a set at a point. The continuous differentiable bump, `ContDiffBump`, is a function that is smooth (infinitely differentiable) and its derivatives tend to zero as they move away from a central point.
More concisely: If `E` is a normed additive commutative group and normed space over the real numbers with a continuous differentiable bump, `c` and `g` are `n`-times continuously differentiable functions from `X` to `E` at `x` within the set `s`, `f` is a function from `X` to a continuous differentiable bump of `c(x)`, and `rIn` and `rOut` are `n`-times continuously differentiable at `x` within `s`, then `f(g(x))` is also `n`-times continuously differentiable at `x` within `s`.
|
ContDiffBump.le_one
theorem ContDiffBump.le_one :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
(f : ContDiffBump c) {x : E}, ↑f x ≤ 1
This theorem states that for any type `E` that forms a normed additive commutative group and a normed space over the real numbers, and for any continuous differentiable "bump" function `f` centered at `c` in `E`, the value of `f` at any point `x` in `E` will always be less than or equal to 1. A "bump" function is a smooth function which is equal to 1 at the center and tapers off to 0 away from the center.
More concisely: For any normed additive commutative group `E` over the real numbers, any continuous differentiable "bump" function `f` centered at `c` in `E` satisfies `f(x) ≤ 1` for all `x` in `E`.
|
ContDiffBump.one_lt_rOut_div_rIn
theorem ContDiffBump.one_lt_rOut_div_rIn : ∀ {E : Type u_1} {c : E} (f : ContDiffBump c), 1 < f.rOut / f.rIn
This theorem states that for any continuously differentiable "bump" function `f` centred at a point `c` in a certain type `E`, the ratio of `rOut` to `rIn` is always greater than 1. Here, `rOut` and `rIn` are parameters of the "bump" function that determine its shape, specifically the radii of the outer and inner regions where the function transitions from 0 to its maximum value.
More concisely: For any continuously differentiable bump function `f` on type `E` with radii `rOut` and `rIn` such that `rOut > rIn`, we have `f(x)/f(c) > 1` for all `x ε B(c, rOut) \ B(c, rIn)`.
|
ContDiffBump.support_eq
theorem ContDiffBump.support_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
(f : ContDiffBump c), Function.support ↑f = Metric.ball c f.rOut
This theorem, `ContDiffBump.support_eq`, states that for any Type `E` that is a Normed Additive Commutative Group and a Normed Space over the real numbers, and that also has a bump function that is continuously differentiable (`HasContDiffBump E`), for any point `c` in `E`, and a continuously differentiable bump function `f` centered at `c`, the support of the function is exactly the same as the metric ball centered at `c` with radius corresponding to the outer radius of the bump function. In other words, the set of all points where the bump function `f` is nonzero corresponds precisely to the set of points within a certain distance (`f.rOut`) of `c`.
More concisely: For any Normed Additive Commutative Group and Normed Space `E` over the real numbers with a continuously differentiable bump function, the support of a continuously differentiable bump function `f` centered at a point `c` in `E` equals the metric ball centered at `c` with radius `f.rOut`.
|
ContDiffAt.contDiffBump
theorem ContDiffAt.contDiffBump :
∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : NormedAddCommGroup X] [inst_3 : NormedSpace ℝ X] [inst_4 : HasContDiffBump E] {n : ℕ∞} {c g : X → E}
{f : (x : X) → ContDiffBump (c x)} {x : X},
ContDiffAt ℝ n c x →
ContDiffAt ℝ n (fun x => (f x).rIn) x →
ContDiffAt ℝ n (fun x => (f x).rOut) x → ContDiffAt ℝ n g x → ContDiffAt ℝ n (fun x => ↑(f x) (g x)) x
The theorem `ContDiffAt.contDiffBump` states that for any normed-additive-commutative-groups `E` and `X` with a normed space over the reals, and given a function `c` and `g` mapping from `X` to `E`, a function `f` mapping from `X` to a continuously differentiable bump function at `c x`, and a point `x` in `X`, if `c`, `(f x).rIn`, `(f x).rOut`, and `g` are all continuously differentiable at `x` of any order `n`, then the composed function `f x` applied to `g x` will also be continuously differentiable at `x` of the same order `n`. In simpler terms, it asserts that the composition of continuously differentiable functions remains continuously differentiable.
More concisely: If `c`, `f`, and `g` are continuously differentiable functions at `x` of order `n` in the respective normed spaces `E` and `X`, then the composition `f (g x)` is continuously differentiable at `x` of order `n` in `E`.
|
ContDiffBump.nonneg
theorem ContDiffBump.nonneg :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
(f : ContDiffBump c) {x : E}, 0 ≤ ↑f x
This theorem states that for any type `E`, given it forms a normalized additive commutative group and a normalized real vector space, and has a continuously differentiable "bump" function (a function that is equal to one at a particular point and decreases to zero as you move away from that point), then for any such bump function `f` centered at a point `c` and any point `x` in `E`, the value of the bump function at `x` is always non-negative. This means that the bump function never dips below the x-axis, regardless of the point you're evaluating it at.
More concisely: Given a normalized additive commutative group `E` with a real vector space structure and a continuously differentiable "bump" function `f` on `E` with center `c`, the function `f` is non-negative on `E`, i.e., `f x ≥ 0` for all `x` in `E`.
|
ContDiffBump.rOut_pos
theorem ContDiffBump.rOut_pos : ∀ {E : Type u_1} {c : E} (f : ContDiffBump c), 0 < f.rOut
This theorem, `ContDiffBump.rOut_pos`, states that for any type `E`, any element `c` of `E`, and any continuously differentiable 'bump' function `f` centered at `c`, the radius `rOut` (the outer radius of the support of `f`) is always positive. Essentially, it ensures that the bump function, which is nonzero only in a certain neighborhood of its center, actually 'extends' beyond the center point in the mathematical space `E`.
More concisely: For any continuously differentiable bump function $f$ centered at an element $c$ in a type $E$, the outer radius of its support is positive.
|
ContDiffBump.contDiff
theorem ContDiffBump.contDiff :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
(f : ContDiffBump c) {n : ℕ∞}, ContDiff ℝ n ↑f
This theorem states that for any type `E` that is a normed additive commutative group and a normed space over the real numbers `ℝ`, if `E` also has a continuously differentiable bump function, then for any point `c` in `E` and any `f` which is a continuously differentiable bump function at `c`, `f` is continuously differentiable at all orders `n` (where `n` can be any natural number or infinity).
More concisely: If a normed additive commutative group `E` over the real numbers `ℝ` has a continuously differentiable bump function and is equipped with a norm making it a normed space, then every continuously differentiable bump function at any point in `E` is infinitely differentiable.
|
ContDiffBump.nonneg'
theorem ContDiffBump.nonneg' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
(f : ContDiffBump c) (x : E), 0 ≤ ↑f x
This theorem states that for any normed additive commutative group `E` that is a normed space over the real numbers `ℝ` and has a continuous differentiable bump, and given any point `c` in `E`, the function `ContDiffBump` at `c` is always nonnegative for any `x` in `E`. In other words, the value of the `ContDiffBump` function at any point in the space is always greater than or equal to zero.
More concisely: For any normed additive commutative group `E` over `ℝ` with a continuous differentiable bump function, the function `ContDiffBump` is nonnegative, that is, `ContDiffBump c x ≥ 0` for all `x` in `E`.
|
ContDiffBump.one_of_mem_closedBall
theorem ContDiffBump.one_of_mem_closedBall :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
(f : ContDiffBump c) {x : E}, x ∈ Metric.closedBall c f.rIn → ↑f x = 1
The theorem `ContDiffBump.one_of_mem_closedBall` states that for any type `E` that is a normed additive commutative group and a real normed space, and also has a smoothly varying ("C^∞-") bump function (`HasContDiffBump`), and for any center point `c` and bump function `f` over `c`, if a point `x` lies within the closed ball of radius `f.rIn` centered at `c` (meaning the distance from `x` to `c` is less than or equal to `f.rIn`), then the value of the bump function `f` at the point `x` is equal to 1. This implies that the bump function `f` equals 1 at all points within the given closed ball.
More concisely: For any normed additive commutative group `E` with a smoothly varying bump function `f` over a center point `c`, if `x` is in the closed ball of radius `f.rIn` centered at `c`, then `f(x) = 1`.
|