Weighted lower bounds for the product norm

The norm on a product of seminormed groups is the maximum of the coordinate norms. Prod.min_mul_norm_sq_le_add bounds a weighted sum of squared coordinate norms below by min a b * ‖x‖², provided at least one coefficient is nonnegative. The other coefficient may be negative, allowing the estimate to apply to quadratic forms with a signed mass term.

theorem Prod.min_mul_norm_sq_le_add {E : Type u_1} {F : Type u_2} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E × F) {a b : ℝ} (h : 0 ≤ max a b) : min a b * ‖x‖ ^ 2 ≤ a * ‖x.1‖ ^ 2 + b * ‖x.2‖ ^ 2

A weighted sum of squared coordinate norms bounds the squared product norm below with coefficient min a b, provided at least one coefficient is nonnegative.