Convex bodies

Stream: maths

[Paul Reichert]

In preparation for more convex geometry / Brunn-Minkowski stuff, I'd like to contribute convex bodies to mathlib.
I think a sensible way would be to first introduce a is_convex_body predicate, checking whether a set is convex, compact, and nonempty, and then to define a subtype convex_body V containing convex bodies in some real vector space V.
Then I'd love to spend a module nnreal (convex_body V) instance.

Does my plan sound about right?

One thing I'm still unsure about are the assumptions. My experience with convex geometry is about finite-dimensional real vector spaces but I will try to generalize as much as possible.

[Yaël Dillies]

Note. You will want to use docs#set_like. A typical example of the design is docs#topological_space.closeds.

[Yaël Dillies]

I doubt we need is_convex_body, because we tend to separate assumptions (this is yet another effect of currying). But convex_body sounds good, although I should check whether it's the mathematically correct notion here.

[Yaël Dillies]

Also, let me tell you about file#data/set/pointwise if you haven't seen it already.

[Paul Reichert]

Regarding the correct definition, there seems to be some inconsistency in the literature whether a convex body has to have a nonempty interior, i.e. has to be full-dimensional. Wikipedia says that it has to, Rolf Schneider's "Convex Bodies: The Brunn-Minkowski Theory" does not.
My personal opinion is that convex bodies should not need to have a nonempty interior. Lots of constructions do not require this assumption, for example above-mentioned module nnreal instance. Also, faces of convex bodies are convex bodies again, except that they are not full-dimensional.

[Yaël Dillies]

There's antecedent to haivng both. See docs#topological_space.compacts, docs#topological_space.positive_compacts

[Paul Reichert]

I have opened a WIP pull request: https://github.com/leanprover-community/mathlib/pull/16297
I appreciate any feedback. :octopus: :+1:

Still, I have to find the right place for the two declarations marked with -- MOVE.
Probably, is_compact.smul should go into topology/subset_properties.lean, just like is_compact, and nnreal.has_continuous_const_smul should go into data/real/nnreal.lean, but I'm not sure.

is_compact.add, for example, already exists but is defined in the monoid module which is not appropriate for smul.

[Yaël Dillies]

is_compact.smul and is_compact.add definitely should go under topology.algebra.

[Paul Reichert]

Yes, now I agree that is a better place.
However, I currently have problems with the check_reducibility linter because my add_monoid class uses set.has_add, which is a localized instance (i.e., not defined as an instance). I found some mentions in Zulip and the note on reducible non-instances but I do not fully understand the problem.
Is there a way to legally use set.has_add in the instance or do I have to localize all instances depending on set.has_add, too? (I think you mentioned something similar in an older chat, @Yaël Dillies...)

Furthermore, this linter error only appears in the CI, just adding the #lint command at the end of my only changed file does not produce it, although check_reducibility is part of the linters enumerated by #list_linters. Is there a way to reproduce the problem locally so that I do not have to litter the CI with my premature debugging attempts?

[Junyan Xu]

Why not define a ℝ-module structure (would you then automatically get the ℝ≥0-module structure?

[Apurva Nakade]

Paul Reichert said:

Yes, now I agree that is a better place.
However, I currently have problems with the check_reducibility linter because my add_monoid class uses set.has_add, which is a localized instance (i.e., not defined as an instance). I found some mentions in Zulip and the note on reducible non-instances but I do not fully understand the problem.
Is there a way to legally use set.has_add in the instance or do I have to localize all instances depending on set.has_add, too? (I think you mentioned something similar in an older chat, Yaël Dillies...)

Furthermore, this linter error only appears in the CI, just adding the #lint command at the end of my only changed file does not produce it, although check_reducibility is part of the linters enumerated by #list_linters. Is there a way to reproduce the problem locally so that I do not have to litter the CI with my premature debugging attempts?

I'm encountering this same problem in #16213
I tried adding @[reducible] to set.has_add but that didn't build so I reverted to using the explicit definition as I didn't really need any of the set.has_add API. Would love to hear a better solution and this is very hacky.

[Yaël Dillies]

Junyan Xu said:

Why not define a ℝ-module structure (would you then automatically get the ℝ≥0-module structure?

Because it's wrong, right? s - s = 1 • s + (-1) • s ≠ (1 - 1) • s = 0

[Yaël Dillies]

Apurva Nakade said:

I reverted to using the explicit definition as I didn't really need any of the set.has_add API. Would love to hear a better solution and this is very hacky.

Yes, this is the way to go. See docs#set_semiring.non_unital_non_assoc_semiring

[Junyan Xu]

Oh yes, add_smul is the nontrivial part. distrib_mul_action should be generalizable to an ℝ-action nonetheless.

[Reid Barton]

What about s + s = 1 • s + 1 • s ≠ 2 • s?

[Yaël Dillies]

This is true for convex bodies, though?

[Reid Barton]

Oh, for convex things yes.

[Paul Reichert]

Yaël Dillies said:

Yes, this is the way to go. See docs#set_semiring.non_unital_non_assoc_semiring

Fine. Thanks for your help! I changed the definition of add and added set.image2_add to the simp sets of the add_monoid proofs. Now it works.

[Paul Reichert]

My preferred next step is to endow convex bodies with the Hausdorff metric, basically by packaging the existing lemmata about the Hausdorff pseudometric into an instance and proving that it's a metric for convex bodies

[Kalle Kytölä]

docs#metric.Hausdorff_dist should be good for that purpose.

[Paul Reichert]

Apurva Nakade said:

I'm encountering this same problem in #16213
I tried adding @[reducible] to set.has_add but that didn't build so I reverted to using the explicit definition as I didn't really need any of the set.has_add API. Would love to hear a better solution and this is very hacky.

I settled with a solution very similar to yours. I just used set.image (+) as proposed by Yaël Dillies. That also enabled me to use the set.has_add instance in the proof as follows:

add_assoc := λ K L M, by { ext, simp only [coe_mk, set.image2_add, add_assoc] }

It's very similar to yours and it's still a bit hacky.

[Paul Reichert]

One question: Is it better to create small PRs for different but related changes or multiple smaller ones?

[Moritz Doll]

generally you want to do smaller PRs

[Paul Reichert]

I just completed the Hausdorff metric instance for convex bodies. If you are interested, you can find it here: #16338

Another thing I'd enjoy to formalize are facts about the relative interior (relint) of a set in a (mostly finite-dimensional) normed space: the interior of the set after restricting the ambient space to the affine hull of the set.
A useful fact is that the relint of a nonempty convex set is nonempty. This corresponds to the existing lemma convex.interior_nonempty_iff_affine_span_eq_top if the convex set is of full dimension, i.e., the affine span is \top.
I hope to be able to use this existing proof to derive the more general statement but I still need some time to figure it out.
(branch: convex_relint)

[Yaël Dillies]

I would actually love seeing this. I've been trying to write API for that several times. See here.

[Paul Reichert]

Thanks for the link. I really like the name "intrinsic interior" because it describes what it is more than "relative interior".
Without having adopted that nomenclature yet, the current state on the branch is that I succeeded with an untidied proof that the intrinsic interior is nonempty if the convex set itself is nonempty.

[Paul Reichert]

Hmm, the most natural setting for the intrinsic interior would be affine spaces / add_torsor.

def intrinsic_interior' (𝕜 : Type) {V P : Type} [normed_field 𝕜] [seminormed_add_comm_group V] [normed_space 𝕜 V]
  [pseudo_metric_space P] [normed_add_torsor V P]
  (A : set P) :=
(coe : affine_span R A → P) '' interior ((coe : affine_span R A → P) ⁻¹' A)

This would enable us to conveniently state the property that it is intrinsic:

def isometry_range_intrinsic_interior {𝕜 V V₂ P P₂: Type}
  [normed_field 𝕜] [seminormed_add_comm_group V] [seminormed_add_comm_group V₂] [normed_space 𝕜 V]
  [normed_space 𝕜 V₂] [pseudo_metric_space P] [pseudo_metric_space P₂] [normed_add_torsor V P]
  [normed_add_torsor V₂ P₂]
  (φ : P →ᵃⁱ[𝕜] P₂) (A : set P) :
φ '' intrinsic_interior' 𝕜 A = intrinsic_interior' 𝕜 (φ '' A) := sorry

It is somewhat painful that affine_subspace may be empty but add_torsormust not be, hindering us from defining the inclusion of an affine_subspace as an affine map (except we fill the nonempty instance manually or add a new type nonempty_affine_subspace)...

[Yaël Dillies]

In fact I myself find that having add_torsor α imply nonempty α to be a problem on branch#linear_algebra_lint.

[Paul A. Reichert]

Update: convex_relint has been rewritten such that the intrinsic interior/frontier/closure is defined in affine spaces and I proved that the intrinsic interior of a nonempty convex set in a normed space over some normed field is nonempty (which we can generalize as soon as convex is defined for arbitrary affine spaces, not only modules).

Most of the file intrinsic.lean are helper lemmata that I should move into other files. Beyond that, I have to remove some old code blocks I commented out.

I also get some looping instances because of add_torsor and nonempty, so we will have to hold back merging until we have resolved Empty torsors in some way.

I appreciate any kind of feedback.

[Paul A. Reichert]

One aspect of the code that is very ugly is that I had to redeclare all variables in every definition or theorem. I tried this:

variables (R : Type) {V P : Type} [ring R] [seminormed_add_comm_group V] [module R V]
  [pseudo_metric_space P] [normed_add_torsor V P]

def intrinsic_interior (A : set P) := (coe : affine_span R A → P) '' interior ((coe : affine_span R A → P) ⁻¹' A)

But based on the signature of the definition, Lean seems to think that the instance of normed_add_torsor is not needed and forgets it, just to throw an error because it cannot derive add_torsor.

[Yaël Dillies]

You should include V, because Lean does not see it in the statement of the declaration, so does not add it to the context.

[Paul A. Reichert]

Just as an update, I'm currently creating small PRs for the several prerequisites that should go into other files -- as soon as that is done, I'll PR the intrinsic module.