Commit 2022-04-22 18:15 695e0b70

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.