Skip to content

Conversation

@t6s
Copy link
Member

@t6s t6s commented May 22, 2025

Motivation for this change

This PR changes the convention of the convex combination operation in convex.v from
a <| t |> b = (1-t)a + tb to ta + (1-t)b, to make this compatible with infotheo (https://gihtub.com/affeldt-aist/infotheo).

There has been a discussion about these two options, and the former
has been chosen for its compatibility with the homotopical notion of paths,
while the latter is algebraically natural.

After a discussion in a analysis-dev meeting, a conclusion was made to change it to the latter.
Also, there is now a line_path in set_interval.v which essentially implements the former convention
and has an appropriately geometric name.

Therefore I think it is now reasonable to do this PR.

@CohenCyril @affeldt-aist

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@t6s t6s requested a review from affeldt-aist May 22, 2025 16:20
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great! This will unlock the port of convex spaces from InfoTheo. Regarding the PR in itself, the technical lemmas about the parameters of the quasi-associativity should be better named and documented. However, I think that it will be more efficient for us to do that along the port of more properties of convex spaces. So I am ok to merge with the proviso that we agree to carefully review that part of the library again in the near future.

@t6s
Copy link
Member Author

t6s commented May 28, 2025

I am afraid of naming the submodule QuasiAssoc, observing there are other (likely to be many other) variations of "quasi-associativity" in algebra. E.g. https://academic.oup.com/ptep/article/2014/1/013A03/1552583

@affeldt-aist
Copy link
Member

Let's be more precise and even hide the module name behind a definition in lowercase akin to associative, etc.

@affeldt-aist affeldt-aist added this to the 1.12.0 milestone May 29, 2025
@affeldt-aist affeldt-aist merged commit 92bdcbf into math-comp:master May 29, 2025
34 checks passed
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Jun 12, 2025
* change the convention for the convex combination operation

---------

Co-authored-by: Reynald Affeldt <[email protected]>
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Jun 20, 2025
* change the convention for the convex combination operation

---------

Co-authored-by: Reynald Affeldt <[email protected]>
@affeldt-aist affeldt-aist mentioned this pull request Jun 28, 2025
@t6s t6s deleted the conv_convention branch September 22, 2025 18:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants