strict convexity

Stream: maths

[Yaël Dillies]

Can we define strict convexity without a topology? The definition on wikipedia is

import analysis.convex.basic
import topology.basic

def strict_convex {𝕜 E : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [topological_space E]
  [has_scalar 𝕜 E] (s : set E) : Prop :=
∀ x y, open_segment 𝕜 x y ⊆ interior s

[Yaël Dillies]

I'm thinking of

def strict_convex {𝕜 E : Type*} [ordered_semiring 𝕜] [add_comm_group E] [has_scalar 𝕜 E]
  (s : set E) : Prop :=
∀ t, is_extreme 𝕜 s t → ∀ x y : E, x ≠ y → ∀ z, z ∈ open_segment 𝕜 x y → z ∈ t → t = s

[Yaël Dillies]

which should be read as "There's no plane on the surface of the set"

[Reid Barton]

Is that missing some parentheses?

[Yaël Dillies]

Hmm, no?

[Yaël Dillies]

Here's a maybe cleaner way to write my proposed definition:

def strict_convex {𝕜 E : Type*} [ordered_semiring 𝕜] [add_comm_group E] [has_scalar 𝕜 E]
  (s : set E) : Prop :=
∀ t, is_extreme 𝕜 s t → ∀ x, x ∈ t → x ∉ s.extreme_points 𝕜 → t = s

[Eric Wieser]

That's the same as this definition, right?

∀ t, is_extreme 𝕜 s t → (t \ s.extreme_points 𝕜).nonempty → t = s

[Yaël Dillies]

Yup, because of the elimination rule for ∃.

[Eric Wieser]

Which I guess you could also write as

∀ t, is_extreme 𝕜 s t → ¬(t ⊆ s.extreme_points 𝕜) → t = s

[David Wärn]

is x ∈ interior s different from ∀ v, ∃ r > 0, x + r • v ∈ s at the intended level of generality?

[Yaël Dillies]

Oh yeah. Take a union of infinitely many concentric spheres

[Yaël Dillies]

My above proposed definitions don't imply convex 𝕜 s... Maybe we can just add convex 𝕜 s ∧?

[David Wärn]

I think I wanted to say ∀ v, ∃ r > 0, ∀ t ∈ Icc 0 r, x + t • v ∈ s

[Yaël Dillies]

Ahah! I think I got the idea.

[Yaël Dillies]

What you want is to not have any planar bits on the boundary. So what you can ask for is that any nonzero linear functional reaches a single maximum.

[Yaël Dillies]

which can be rewritten (thanks to someone's API :innocent:) as ∀ t, is_exposed 𝕜 s t → ¬ s ⊆ t → t.subsingleton.

[Yaël Dillies]

The problem with the above definition is that it requires a normed space. I'm going to replace is_exposed with is_extreme.

[Yaël Dillies]

Note that the difference between the usual definition will then be that "flat" sets can be strictly convex, because the topology doesn't see them.

[Yaël Dillies]

Does anyone know whether that'll make a difference in applications?