contDiff_norm_sq
theorem contDiff_norm_sq :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst : InnerProductSpace π E]
[inst : NormedSpace β E] {n : ββ}, ContDiff β n fun x => βxβ ^ 2
The theorem `contDiff_norm_sq` states that for any type `π`, any normed additive commutative group `E` over `π`, any inner product space over `E` and `π`, any normed space over `E` and real numbers, and any natural number `n` (which could also be infinite), the function that maps `x` to the square of its norm, `βxβ ^ 2`, is `n` times continuously differentiable over real numbers.
More concisely: For any normed additive commutative group `E` over a field `π`, any inner product space and normed space over `E` and `π`, the function `x β¦ βxβΒ²` is `n`-times continuously differentiable on the real numbers.
|
ContDiffAt.norm
theorem ContDiffAt.norm :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst : InnerProductSpace π E]
[inst : NormedSpace β E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace β G] {f : G β E}
{x : G} {n : ββ}, ContDiffAt β n f x β f x β 0 β ContDiffAt β n (fun y => βf yβ) x
This theorem states that if a function `f` from a Normed Additive Commutative Group `G` to an Inner Product Space `E` over a Ring Completeness-like structure `π` is continuously differentiable at a point `x` up to order `n`, and if `f(x)` is not equal to zero, then the function that gives the norm of `f(y)` is also continuously differentiable at `x` up to the same order `n`. Here, `ββ` represents the extended natural numbers, which includes the infinite order of differentiability.
More concisely: If `f` is a continuously differentiable function of order `n` from a Normed Additive Commutative Group `G` to an Inner Product Space `E` over a Ring Completeness-like structure `π`, and `f(x) β 0`, then the norm of `f` is a continuously differentiable function of order `n` at `x`.
|
ContDiffAt.norm_sq
theorem ContDiffAt.norm_sq :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst : InnerProductSpace π E]
[inst : NormedSpace β E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace β G] {f : G β E}
{x : G} {n : ββ}, ContDiffAt β n f x β ContDiffAt β n (fun x => βf xβ ^ 2) x
The theorem `ContDiffAt.norm_sq` states that for any given normed-additive commutative group `E` with an inner product space over a ring `π` that behaves like real numbers (`RCLike π`) and is a normed space over real numbers, and another normed-additive commutative group `G` which is also a normed space over real numbers, if a function `f` mapping from `G` to `E` is continuously differentiable at a point `x` in `G` to any degree `n` (which can be a natural number or infinity), then the function that maps `x` to the squared norm of `f(x)` is also continuously differentiable at `x` to the same degree `n`.
More concisely: If `f:` `G` -> `E` is `n`-times continuously differentiable at `x` in the normed spaces `G` over `π` and `E` over real numbers, then the function `x` -> `β₯f(x)β₯Β²` is also `n`-times continuously differentiable at `x`.
|
contDiffAt_norm
theorem contDiffAt_norm :
β (π : Type u_1) {E : Type u_2} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst : InnerProductSpace π E]
[inst : NormedSpace β E] {n : ββ} {x : E}, x β 0 β ContDiffAt β n norm x
The theorem `contDiffAt_norm` states that for any real or complex field π, a normed add commutative group E, an inner product space over E, a normed space over E, and any natural number or infinity n, if vector x in E is not the zero vector, then the norm function is continuously differentiable at x of order n.
More concisely: For any normed add commutative group E over a real or complex field, inner product space, and normed space over E, if $x \in E$ is nonzero, then the norm function is continuously differentiable of order $n$ at $x$.
|