generalize onem

[affeldt-aist]

Motivation for this change

this generalization is needed by @t6s in another development

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

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

The changes look good.
I have realized that my original intention (in infotheo) was pointless,
but this generalization here should be valuable on its own.

[proux01]

My opinion (please ignore it): unstable.v and "another development" sounds rather bad considering unstable.v must remain internal to Analysis. I'm also not a great fan of this onem thing that always sounded to me like a hack to workaround deficiencies of other more principled mechanisms. Do we still really need it?

[affeldt-aist]

My opinion (please ignore it): unstable.v and "another development" sounds rather bad considering unstable.v must remain internal to Analysis.

This is a bit particular. This is because onem is used in the convexity theory of infotheo that we are in the process of porting to MCA (convex.v actually comes from infotheo). The porting has been slowed down by the fact that we took the "bad" decision to change the convention for the convexity operator. Saikawa-san recently fixed this, so that the port can now continue (and it does: infotheo now uses MCA's definition). Once it is done, there should not be any use of unstable.v in infotheo.

I'm also not a great fan of this onem thing that always sounded to me like a hack to workaround deficiencies of other more principled mechanisms. Do we still really need it?

It is true that at some point it was used in the way we would use {i01 R} now and as a matter of fact convex.v in MCA uses the latter preferentially now. But it also serves as a substitute for the $\overline{x}$ notation that is used in papers for $1 - x$ and that we note x.~ in infotheo. I think that it helps when we need to write down the complicated side-conditions for, e.g., quasi-associativity.
It is possible that many usages of onem will be subsumed by {i01 R} as we port to the point that the `1- notation will disappear but maybe the usage of onem and its notation .~ might stay for its better aesthetics.

@t6s What do you think?

[t6s]

I feel rather fine to use (abuse) unstable in some other development (like infotheo), but it might be indeed bad to motivate an update to unstable by such an external issue.

Apart from that moral issue, this PR itself is just a simple improvement and would be worth being merged.

As for onem itself, I am happy too if it can be removed at all.

The notation .~ looks slightly better than `1- to me.

[proux01]

Thanks for the explanations! I don't have anything against a _ .~ notation, it's just the 1- _ thing that I dislike.
Anyway it seems we mostly agree on the long term objectives and I understand the shorter term constraints, so please ignore my complaints and go ahead with the current PR.

[affeldt-aist]

Yeah, RIP `1-. 👻