norm_smul_inv_norm
theorem norm_smul_inv_norm :
โ {๐ : Type u_1} [inst : RCLike ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E]
{x : E}, x โ 0 โ โ(โโxโ)โปยน โข xโ = 1
This theorem states that for any non-zero vector `x` in a normed space `E` over either the real numbers `โ` or the complex numbers `โ`, if we scale `x` by the reciprocal of its norm, the norm of the resulting vector is 1. In other words, this process normalizes the vector to unit length.
More concisely: For any non-zero vector `x` in a normed space `E` over `โ` or `โ`, the normalized vector `x / norm x` has norm 1.
|
LinearMap.bound_of_ball_bound'
theorem LinearMap.bound_of_ball_bound' :
โ {๐ : Type u_1} [inst : RCLike ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E]
{r : โ},
0 < r โ โ (c : โ) (f : E โโ[๐] ๐), (โ z โ Metric.closedBall 0 r, โf zโ โค c) โ โ (z : E), โf zโ โค c / r * โzโ
The theorem `LinearMap.bound_of_ball_bound'` states that for any nontrivially normed field `๐`, a normed additive commutative group `E`, and a normed space over `๐` and `E`, if a real number `r` is positive, then for any real number `c` and a linear map `f` from `E` to `๐`, if the norm of the output of `f` is less than or equal to `c` for all points within a closed ball of radius `r` centered at 0, then the norm of the output of `f` for any point in `E` is less than or equal to `c / r` times the norm of that point. In simpler terms, it says that if the output of a linear map is bounded within a certain sphere around the origin, then you can estimate an upper bound for the output of the linear map anywhere, based on the norm of the input.
More concisely: For any normed field `๐`, normed additive commutative group `E`, and normed space over `๐` and `E`, if a linear map `f` from `E` to `๐` is norm-bounded on a closed ball of radius `r` centered at 0, then for all `x` in `E`, `โโfxโโโคโโxโโโc/rโ`.
|
norm_smul_inv_norm'
theorem norm_smul_inv_norm' :
โ {๐ : Type u_1} [inst : RCLike ๐] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ๐ E]
{r : โ}, 0 โค r โ โ {x : E}, x โ 0 โ โ(โr * (โโxโ)โปยน) โข xโ = r
This theorem states that for any real number `r` that is greater than or equal to zero and any nonzero vector `x` in a normed space `E` over a field `๐` (which is either the real numbers `โ` or the complex numbers `โ`), the norm (or length) of the vector obtained by scaling `x` by the factor `r` divided by the norm of `x` is equal to `r`. Here, `โข` denotes the scalar multiplication operation in the normed space.
More concisely: For any nonzero vector `x` in a normed space `E` over a field `โ` or `โ`, and any real number `r โฅ 0`, the norm of `r * x / ||x||` is equal to `r`.
|