Pairing a vector with its extremal vector

The extremal vector ‖x‖ ^ (r - 2) • x of the Lʳ norm pairs with x to give ‖x‖ ^ r.

theorem TauCeti.inner_ofReal_rpow_sub_two_smul {𝕜 : Type u_1} [RCLike 𝕜] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {r : ℝ} (hr : r ≠ 0) (x : V) : inner 𝕜 x (↑(‖x‖ ^ (r - 2)) • x) = ↑(‖x‖ ^ r)

Pairing a vector with its extremal vector ‖x‖ ^ (r - 2) • x gives ‖x‖ ^ r.