[Merged by Bors] - feat(analysis/convex/strict_convex_space): Strictly convex spaces

[YaelDillies]

Define strictly_convex_space, a Prop-valued mixin to state that a normed space is strictly convex.

---

• depends on: [Merged by Bors] - chore(analysis): move lemmas around #12621
• depends on: [Merged by Bors] - chore(analysis/convex/strict): Reduce typeclass assumptions, golf #12627
• depends on: [Merged by Bors] - refactor(linear_algebra/ray): redefine same_ray to allow zero vectors #12618

[urkud]

I'm sorry for a long silence: I was busy with my ITP paper. I mostly like the code. Tomorrow I'm going to double check that TC assumptions in the new "two semirings" lemmas are indeed minimal. Also, I don't like the new lemmas that represent (closed) balls as images of the unit (closed) ball under some map. I think that we should swap LHS with RHS and name them smul_unit_ball etc.

BTW, could you please prove that the triangle inequality is an equality iff one of the points belongs to the segment (probably, starting with a proof that ∥u + v∥ = ∥u∥ + ∥v∥ implies that u and v are proportional)?

[YaelDillies]

Let's give it a go!

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - chore(analysis): move lemmas around #12621
• [Merged by Bors] - chore(analysis/convex/strict): Reduce typeclass assumptions, golf #12627
• [Merged by Bors] - refactor(linear_algebra/ray): redefine same_ray to allow zero vectors #12618
  By Dependent Issues (🤖). Happy coding!

[ericrbg]

lgtm though! i guess the two things I noticed have good reasons for being this way

[mcdoll]

I don't know anything about strictly convex spaces. The code looks good.

[j-loreaux]

Mainly I'm not quite sure why you chose this particular definition, see comments within.

[j-loreaux]

I know it follows from the strict convexity of a single ball, but the definition you gave is in terms of all balls of positive radius centered at the origin.

Suggested change

	field (e.g., `ℝ` or `ℚ`) is strictly convex. The definition requires strict convexity of a closed
	ball of positive radius with center at the origin; strict convexity of any other closed ball follows
	field (e.g., `ℝ` or `ℚ`) is strictly convex. The definition requires strict convexity of all closed
	balls of positive radius with center at the origin; strict convexity of any other closed ball follows

[j-loreaux]

I feel like this is a weird middle ground to have as the definition. What I mean is this: strict convexity follows from strict convexity of the unit ball, and in a strictly convex space, all balls are strictly convex. So, in the definition, I would expect one of those two (unit ball or all balls), and presumably the former with a theorem for the latter. As it is now, whenever someone makes a strict_convex_space they will always opt for the constructor lemma strict_convex_space.of_strict_convex_closed_unit_ball, but instead you could just make that the definition. So, to be clear, I'm asking for:

class strict_convex_space (𝕜 E : Type*) [normed_linear_ordered_field 𝕜] [normed_group E]
  [normed_space 𝕜 E] : Prop :=
(strict_convex_closed_ball : strict_convex 𝕜 (closed_ball (0 : E) (1 : ℝ))

With a new proof of strict_convex_closed_ball and deleting strict_convex_space.of_strict_convex_closed_unit_ball. Of course, if you implement this, ignore the documentation comments above about "all balls"

[j-loreaux]

Is the point that strict convexity of the unit ball only implies strict convexity of all other balls if E is an ℝ-vector space? If so, is there an easy counterexample? In that case, just say so and ignore this comment.

[urkud]

For me, the main question is "do we want to have 𝕜 in this file?"
All useful theorems only work for 𝕜 = ℝ. See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311794.20Strictly.20convex.20spaces
The proof of the implication "unit ball → any ball" only works for 𝕜 = ℝ. Not sure about a counterexample.

[YaelDillies]

Proving strict convexity of a ball at the origin is significantly easier than proving strict convexity of the unit ball, because you can use the norm in place of the distance to 0. Proving strict convexity of the unit ball does not seem significantly easier than proving strict convexity of any ball at the origin.

I believe 𝕜 = ℚ also works, because the main restriction to "unit ball → any ball" is that your points might reach only a discrete set of norms. Hence I believe some polynomial ring over some space will make "unit ball → any ball" fail.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests