theorem powerDistance_fderiv_pairing_eq_explicit_gradient_pairing {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (p : ℝ) (x0 x y : F) (hp : 2 ≤ p) : ((Module.dualPairing ℝ F) (↑(fderiv ℝ (powerDistance p x0) x) - ↑(fderiv ℝ (powerDistance p x0) y))) (x - y) = inner ℝ (‖x - x0‖ ^ (p - 2) • (x - x0) - ‖y - x0‖ ^ (p - 2) • (y - x0)) (x - y)

Helper for Lemma 4.2.3: on the canonical Hilbert-space owner powerDistance, the derivative pairing is exactly the inner product with the explicit power-gradient difference.

theorem powerDistance_fderiv_mono_ge_norm_rpow_of_explicit_gradient_mono {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (p : ℝ) (x0 x y : F) (hp : 2 ≤ p) (hmono : (1 / 2).rpow (p - 2) * ‖x - y‖.rpow p ≤ inner ℝ (‖x - x0‖ ^ (p - 2) • (x - x0) - ‖y - x0‖ ^ (p - 2) • (y - x0)) (x - y)) : ((Module.dualPairing ℝ F) (↑(fderiv ℝ (powerDistance p x0) x) - ↑(fderiv ℝ (powerDistance p x0) y))) (x - y) ≥ (1 / 2).rpow (p - 2) * ‖x - y‖.rpow p

Helper for Lemma 4.2.3: after rewriting the derivative pairing into the explicit gradient pairing on the owner powerDistance, the source monotonicity estimate is exactly (4.2.14).

theorem powerFunction_uniformConvexOn {E : Type u} [AddCommGroup E] [Module ℝ E] (B : LinearMap.BilinForm ℝ E) (hPos : (LinearMap.BilinMap.toQuadraticMap B).PosDef) (p : ℝ) (x0 : B.PrimalSpace) (hp : 2 ≤ p) : have x := hp; UniformConvexOn Set.univ (uniformConvexPowerModulus ((1 / 2).rpow (p - 2)) p) (powerFunction B p x0)

Lemma 4.2.3 in owner form: on the intrinsic B-weighted space, the degree-p power regularizer is uniformly convex with the textbook modulus (1 / p) * (1 / 2)^(p - 2) * r^p.

theorem powerFunction_fderiv_mono_ge_primalNorm_rpow {E : Type u} [AddCommGroup E] [Module ℝ E] (B : LinearMap.BilinForm ℝ E) (hPos : (LinearMap.BilinMap.toQuadraticMap B).PosDef) (p : ℝ) (x0 x y : B.PrimalSpace) (hp : 2 ≤ p) : have x_1 := hp; ((Module.dualPairing ℝ B.PrimalSpace) (↑(fderiv ℝ (powerFunction B p x0) x) - ↑(fderiv ℝ (powerFunction B p x0) y))) (x - y) ≥ (1 / 2).rpow (p - 2) * ‖x - y‖.rpow p

Lemma 4.2.3 (1): for a positive-definite self-adjoint form B, the Fréchet derivative of the degree-p power function d_p(x) = (1 / p) * ‖x - x₀‖[B]^p is strongly monotone with modulus (1 / 2)^(p - 2) when measured in the intrinsic norm on PrimalSpace B, i.e. in the B-induced norm.

theorem powerFunction_lower_tangent_ge_primalNorm_rpow {E : Type u} [AddCommGroup E] [Module ℝ E] (B : LinearMap.BilinForm ℝ E) (hPos : (LinearMap.BilinMap.toQuadraticMap B).PosDef) (p : ℝ) (x0 x y : B.PrimalSpace) (hp : 2 ≤ p) : have x_1 := hp; powerFunction B p x0 x ≥ powerFunction B p x0 y + ((Module.dualPairing ℝ B.PrimalSpace) ↑(fderiv ℝ (powerFunction B p x0) y)) (x - y) + 1 / p * (1 / 2).rpow (p - 2) * ‖x - y‖.rpow p

Lemma 4.2.3 (2): for a positive-definite self-adjoint form B, the degree-p power function lies above its tangent model at y by at least (1 / p) * (1 / 2)^(p - 2) * ‖x - y‖^p in the intrinsic norm on PrimalSpace B; equivalently, the Bregman gap at y has the same lower bound.