Rescaling a vector by a real root

For a ≥ 0 and q ≠ 0, scaling a vector v in a normed space over 𝕜 = ℝ or ℂ by the real scalar a ^ (1 / q) multiplies ‖v‖ ^ q by a. This is how weights are absorbed into the points of a finite family when estimating ℓᵖ sums. The extremal vector ‖x‖ ^ (r - 2) • x of the Lʳ norm has norm at most ‖x‖ ^ (r - 1).

theorem TauCeti.norm_ofReal_rpow_inv_smul_rpow {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {a q : ℝ} (ha : 0 ≤ a) (hq : q ≠ 0) (v : E) : ‖↑(a ^ q⁻¹) • v‖ ^ q = a * ‖v‖ ^ q

Scaling v by the real scalar a ^ q⁻¹, for a ≥ 0 and q ≠ 0, multiplies ‖v‖ ^ q by a.

theorem TauCeti.norm_ofReal_rpow_sub_two_smul_le {𝕜 : Type u_1} [RCLike 𝕜] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace 𝕜 V] (r : ℝ) (x : V) : ‖↑(‖x‖ ^ (r - 2)) • x‖ ≤ ‖x‖ ^ (r - 1)

The extremal vector ‖x‖ ^ (r - 2) • x of the Lʳ norm has norm at most ‖x‖ ^ (r - 1).