Lean roadmap with sorries for int_cvx #8
Conversation
| variables {V : Type*} [add_comm_group V] [vector_space ℝ V] | ||
|
|
||
| /-- The dilation about `c` with scale factor `r`. -/ | ||
| def dilation (c : V) (r : ℝ) : V → V := sorry |
There was a problem hiding this comment.
What do you think about using an affine_space, and define it as a homomorphism to affine self-maps?
There was a problem hiding this comment.
Yes! I haven't actually looked much at affine_space. Is it ready for this?
I'd put in a TODO a few lines higher suggesting this generalisation.
There was a problem hiding this comment.
I see. It really seems like we should redo everything about convexity for affine spaces rather than linear spaces, perhaps before proceeding with much else... You'd made a start on this?
There was a problem hiding this comment.
Yes, it seems to make sense to first work on the affine space part of mathlib.
| sorry | ||
|
|
||
| def affine_independent (s : finset V) : Prop := sorry | ||
|
|
There was a problem hiding this comment.
Do we have the technology to say "this follows from dilation.equiv"? (Well, once we have dilation.equiv for affine spaces)
There was a problem hiding this comment.
What are you commenting Jalex? Is it line 74
There was a problem hiding this comment.
Yes, I meant to refer to the comment in line 74; thanks.
There was a problem hiding this comment.
No, there's no obvious automation to prove dilations of affine independent sets are affine independent.
|
|
||
| -- TODO if a finset is contained in an open set, then for any center `c` there is some ε > 0 | ||
| -- so its dilation by (1+ε) is still in that open set. | ||
|
|
There was a problem hiding this comment.
this is slightly more subtle than I expected, I think it requires that open balls are convex. One may as well go ahead and prove the following, which makes generalizing to finsets easier.
lemma foo (c : V) {x : V} {s : set V} (h : is_open s) (hx : x ∈ s) :
∃ k : ℝ, ∀ ε ≤ k, 0 ≤ ε → dilation c (1+ε) x ∈ s := sorry
There was a problem hiding this comment.
I don't think we need that version.
There was a problem hiding this comment.
We don't need it, and it's also vacuous as stated, by taking k = -1. :-)
With that fixed, I'd have no objection to someone proving this statement by first proving this, but I think that should be left up to whoever wants to write a proof here.
Co-authored-by: Jalex Stark <alexmaplegm@gmail.com>
| variables {V : Type*} [add_comm_group V] [vector_space ℝ V] | ||
|
|
||
| /-- The dilation about `c` with scale factor `r`. -/ | ||
| def dilation (c : V) (r : ℝ) : V → V := sorry |
There was a problem hiding this comment.
Yes, it seems to make sense to first work on the affine space part of mathlib.
| -- In fact, dilations preserve the affine structure, | ||
| -- so one could strengthen this to `ℝ →* End (Aff.of V)`, | ||
| -- if we define `Aff`. | ||
| def dilations (c : V) : ℝ →* category_theory.End V := sorry |
There was a problem hiding this comment.
Do you expect to be able to use the category library here, or is it only for completeness?
There was a problem hiding this comment.
I only did this because it's the only mechanism I know of to quickly put a monoid structure on endomorphisms. This is the same reason the category theory API gets imported on the way to the Hahn-Banach theorem in mathlib!
|
|
||
| -- TODO if a finset is contained in an open set, then for any center `c` there is some ε > 0 | ||
| -- so its dilation by (1+ε) is still in that open set. | ||
|
|
There was a problem hiding this comment.
I don't think we need that version.
|
|
||
| We'll shortly specialise this to the case `c = barycenter t`. | ||
| -/ | ||
| lemma quux (x : V) (t : finset V) (f : V → ℝ) (h : t.center_mass f id = x) (r : ℝ) (c : V) : |
There was a problem hiding this comment.
I'm not sure the dot notation improve readability here. And maybe we need a variation on center_mass when the indexing type is the vector space. This will change if we switch to affine space of course. But in any case it would be more readable to have a notation which looks like a weighted sum.
There was a problem hiding this comment.
Ok. The .center_mass syntax is what's used in mathlib, so I was just following that. Obviously if mathlib changes this can follow, later.
| sorry | ||
|
|
||
| def affine_independent (s : finset V) : Prop := sorry | ||
|
|
There was a problem hiding this comment.
What are you commenting Jalex? Is it line 74
| -- TODO the lemma characterising | ||
| -- the interior of the convex hull of a finset of size `d + 1` | ||
| -- as the strictly positive affine combinations of the points, if the finset is affine independent, | ||
| -- or empty otherwise |
There was a problem hiding this comment.
This lemma is not used in my blueprint. It would be nice to have it, but I don't think we need it.
There was a problem hiding this comment.
I suspect we'll find that generally the more "generic" parts of the project are going to follow a more "steamroller everything, with a thorough API" style" suitable for mathlib, while the specialised parts will closely follow the "shortest path" indicated in the blueprint.
|
|
||
| lemma int_cvx (s : set V) (h : is_open s) : | ||
| convex_hull s = | ||
| ⋃ (t : finset V) (h : ↑t ⊆ s) (b : t.card = findim ℝ V + 1), interior (convex_hull (↑t : set V)) := |
There was a problem hiding this comment.
This is not the statement from the blueprint, which directly gives the conclusion we need, ie expressing points of the convex hull as nice centers of mass.
There was a problem hiding this comment.
No, it's not, but I think like in the Cartheodory PR to mathlib, it's nicest to first give the "soft" statement of the result, and then give the "hard" statement, which should follow by rewriting using the characterisation of the interior directly.
I'll add this statement, too.
There was a problem hiding this comment.
I've now added, and proved (modulo of course all earlier sorries!), the explicit statement.
* Lean roadmap with sorries for int_cvx Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Jalex Stark <alexmaplegm@gmail.com>
@PatrickMassot wrote a human readable proof of Lemma 1.5.
Here I've done the next step --- written out (nearly) all the statements that should appear in the corresponding Lean file, all with sorries as proofs/definitions.
Note that even though it's a single lemma in the text, it's become 13 declarations in this next iteration. (Some of these are "missing background material, rather than the lemma itself.)