infotheo
infotheo copied to clipboard
affeldt-aist
Carathéodory
Strengthens convA' and convACA' and adds a few lemmas. Defines l-modules as convex spaces. Proves Carathéodory's Theorem. Contains general purpose lemmas that should not stay here (e.g. everything in section split_prod and everything in section caratheodory except lemma caratheodory).
I tried to improve a few things in this branch: https://github.com/affeldt-aist/infotheo/commits/tragicus_master. You can maybe cherry-pick the last commit.
You seem to have created the PR from your master branch.
Indeed, is that bad practice ?
Indeed, is that bad practice ?
Yes. :-)
Oh, sorry. I do not see a way to change the branch now, I will pay attention in the future. Many thanks for the review and sorry for the "admit". I see that some checks failed, should I make the code compatible with mathcomp-1.13.0? Also, the "Require Import div" raises a warning, should it be put at the beginning of the file?
should I make the code compatible with mathcomp-1.13.0?
If it is not too much of a burden.
Also, the "Require Import div" raises a warning, should it be put at the beginning of the file?
Yes.
I have just tried to rebase. The HB.instance line 2040 does not compile and I could not fix it (everything else works fine).
I have just tried to rebase. The HB.instance line 2040 does not compile and I could not fix it (everything else works fine).
You mean fun_orderedConvType? I am a bit puzzled because the last commit compiles fine on my machine.
About your PR: you are PRing from your master and the list of commits seems to reveal duplications of commits
that are already in master.
I have just tried to rebase. The HB.instance line 2040 does not compile and I could not fix it (everything else works fine).
You mean
fun_orderedConvType? I am a bit puzzled because the last commit compiles fine on my machine. About your PR: you are PRing from your master and the list of commits seems to reveal duplications of commits that are already in master.
I had missed the updated dependency on hierarchy-builder, it is fixed. I may have messed up with the rebase. Should I try to make a new clean branch and redo the PR ?
Should I try to make a new clean branch and redo the PR ?
I think it is easier this way.
I couldn't push (at least without push-force) so I put a new commit in another branch: https://github.com/affeldt-aist/infotheo/pull/85
You'll find a new commit here: https://github.com/affeldt-aist/infotheo/pull/85 (still reading)
@Tragicus We've merged PR #85 which should contained all the commits of this PR, so that it should be ok to close.
Your second proofreading does not appear in the list of commits. Besides, the definition of linear_affine was broken due to HB, I have just fixed it.
Your second proofreading does not appear in the list of commits.
Really? I thought I squashed my last commits into one.
Besides, the definition of linear_affine was broken due to HB, I have just fixed it.
I also fixed it in PR #85 .