[Merged by Bors] - feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine independence #8892
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ocfnash
force-pushed
the
refined_caratheodory
branch
from
0d434d7
to
c264f20
Compare
Evidently, these are just thin wrappers around `well_founded.min` but I think this use case is common enough to deserve this specialisation.
ocfnash
force-pushed
the
refined_caratheodory
branch
from
c264f20
to
86f1489
Compare
github-actions
bot
added
the
blocked-by-other-PR
ocfnash
force-pushed
the
refined_caratheodory
branch
2 times, most recently
from
a9887f8
to
3e533ab
Compare
…o provide affine independence
ocfnash
force-pushed
the
refined_caratheodory
branch
from
3e533ab
to
59dd3b7
Compare
ocfnash
added
awaiting-review
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
YaelDillies
approved these changes
Sep 4, 2021
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
2 tasks
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Sep 6, 2021
…o provide affine independence (#8892) The changes here are: - Use hypothesis `¬ affine_independent ℝ (coe : t → E)` instead of `finrank ℝ E + 1 < t.card` - Drop no-longer-necessary `[finite_dimensional ℝ E]` assumption - Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via `min_card_finset_of_mem_convex_hull` - Provide a single alternative form of Carathéodory's lemma `eq_pos_convex_span_of_mem_convex_hull` - In the alternate form, define the explicit linear combination using elements parameterised by a new `fintype` rather than on the entire ambient space `E` (we thus avoid the issue of junk values outside of the relevant subset)
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Sep 6, 2021
…o provide affine independence (#8892) The changes here are: - Use hypothesis `¬ affine_independent ℝ (coe : t → E)` instead of `finrank ℝ E + 1 < t.card` - Drop no-longer-necessary `[finite_dimensional ℝ E]` assumption - Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via `min_card_finset_of_mem_convex_hull` - Provide a single alternative form of Carathéodory's lemma `eq_pos_convex_span_of_mem_convex_hull` - In the alternate form, define the explicit linear combination using elements parameterised by a new `fintype` rather than on the entire ambient space `E` (we thus avoid the issue of junk values outside of the relevant subset)
|
Build failed (retrying...): |
1 task
bors bot
pushed a commit
that referenced
this pull request
Sep 6, 2021
…o provide affine independence (#8892) The changes here are: - Use hypothesis `¬ affine_independent ℝ (coe : t → E)` instead of `finrank ℝ E + 1 < t.card` - Drop no-longer-necessary `[finite_dimensional ℝ E]` assumption - Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via `min_card_finset_of_mem_convex_hull` - Provide a single alternative form of Carathéodory's lemma `eq_pos_convex_span_of_mem_convex_hull` - In the alternate form, define the explicit linear combination using elements parameterised by a new `fintype` rather than on the entire ambient space `E` (we thus avoid the issue of junk values outside of the relevant subset)
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Sep 7, 2021
…o provide affine independence (#8892) The changes here are: - Use hypothesis `¬ affine_independent ℝ (coe : t → E)` instead of `finrank ℝ E + 1 < t.card` - Drop no-longer-necessary `[finite_dimensional ℝ E]` assumption - Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via `min_card_finset_of_mem_convex_hull` - Provide a single alternative form of Carathéodory's lemma `eq_pos_convex_span_of_mem_convex_hull` - In the alternate form, define the explicit linear combination using elements parameterised by a new `fintype` rather than on the entire ambient space `E` (we thus avoid the issue of junk values outside of the relevant subset)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The changes here are:
¬ affine_independent ℝ (coe : t → E)instead offinrank ℝ E + 1 < t.card[finite_dimensional ℝ E]assumptionmin_card_finset_of_mem_convex_hulleq_pos_convex_span_of_mem_convex_hullfintyperather than on the entire ambient spaceE(we thus avoid the issue of junk values outside of the relevant subset)function.argmin,function.argmin_on#8895