mathlib

695e0b70 - feat(analysis/convex/strict_convex_space): Verify strict convexity from fixed scalars (#13548)

feat(analysis/convex/strict_convex_space): Verify strict convexity from fixed scalars (#13548) Prove that `∀ x y : E, ∥x∥ ≤ 1 → ∥y∥ ≤ 1 → x ≠ y → ∥a • x + b • y∥ < 1` for **fixed** `a` and `b` is enough for `E` to be a strictly convex space.