Bounded conditional supremum

Stream: Is there code for X?

[Yaël Dillies]

In the naming convention, we have supr for the indexed supremum, bsupr for the bounded indexed supremum, csupr for the conditional indexed supremum. Are people fine with me using bcsupr for the bounded conditional indexed supremum or do you have better alternatives?

[Eric Wieser]

Bounded csuprs don't work in the current design unfortunately (at least, on generalized types), because the csupr when the condition is false is unspecified

[Yaël Dillies]

But I still have a few lemmas about them.

[Eric Wieser]

I'm curious; can you give an example?

[Yaël Dillies]

branch#convexity_modulus

[Yaël Dillies]

You can see that I'm using the fact that when csupr is unspecified it is still equal to some definite value.

[Eric Wieser]

I guess my argument would be that those statements are perhaps worse than useless, as they suggest that bcsupr is actually a useful meaningful thing; but all the times I've seen someone actually try to use it in a generic setting the conclusion was it didn't mean what they wanted it to mean

[Eric Wieser]

lemma bcsupr_mono_right (hg : bdd_above (set.range g)) (hfg : ∀ i, p i → f i ≤ g i) :
  (⨆ (i : ι) (hi : p i), f i) ≤ ⨆ (i : ι) (hi : p i), g i :=

Is indeed a true lemma, but the left and right hand side are not what would usually be considered a bounded supremum, as the semantics are not "exclude the elements where p i doesn't hold", but "replace them with some unspecified constant"

[Eric Wieser]

The meaningful version of that lemma is

lemma csupr_subtype_mono_right (hg : bdd_above (set.range g)) (hfg : ∀ i, p i → f i ≤ g i) :
  (⨆ i : subtype p, f i) ≤ ⨆ i : subtype p, g i :=

But I suspect that's an obvious special case of an existing lemma

[Yaël Dillies]

So what are you suggesting? That I take one sup over all pairs x and y?

[Eric Wieser]

Does taking the nnreal norm make things easier?

[Yaël Dillies]

Why would it? :thinking:

[Eric Wieser]

Because that's a docs#conditionally_complete_lattice_bot which has well-behaved bounded supremums

[Yaël Dillies]

No it doesn't. What you're taking the supremum of must be bounded.

[Yaël Dillies]

Ahah, stop editing :rofl:

[Eric Wieser]

Hmm, is conditionally_complete_lattice_bot gone?

[Eric Wieser]

Oh yeah, order_bot

[Yaël Dillies]

Yeah, since Yakov's refactor

[Eric Wieser]

Sorry, by "bounded" i mean in the sense of bsupr not bdd_below

[Yaël Dillies]

Then I maintain my "no". What if you take Sup univ?

[Eric Wieser]

My claim is that on types with order_bot, ⨆ (i : ι) (hi : p i) and ⨆ i : subtype p, coincide because ⨆ (i : false), _ = bot

[Eric Wieser]

The lemmas you have right now are odd because you know nothing about ⨆ i : false, _

[Yaël Dillies]

Is that a lemma? I doubt it's true because you are still not addressing the case of unbounded sets.

[Eric Wieser]

A lot of the lemmas here look like they ought to generalize to order_bot: https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html#lemmas-about-a-conditionally-complete-linear-order-with-bottom-element

[Eric Wieser]

Oh, at any rate what I meant to link above was docs#conditionally_complete_linear_order_bot

[Eric Wieser]

Which nnreal satisfies

[Yaël Dillies]

I don't like the idea of going through nnreal.

[Eric Wieser]

We have docs#has_nnnorm.nnnorm (∥a∥₊) presumably to help with this kind of thing

[Yaël Dillies]

Yeah but that means I have to coerce back from nnreal to real or have convex_mod be nnreal-valued.

[Eric Wieser]

Is having convex_mod be nnreal-valued a problem?

[Eric Wieser]

That seems like the obvious choice

[Yaël Dillies]

I have yet to formalize a single bit of the applications of convex_mod, so I really don't know.

[Yaël Dillies]

In the literature, they even define convex_mod : Icc 0 2 → Icc 0 1, but that's definitely too extreme.

[Yaël Dillies]

Thinking about this again, @Eric Wieser, should we have a dedicated API for ⨆ x : subtype p, f x?

[Eric Wieser]

Either that or something akin to finsum but for supr

[Eric Wieser]

But maybe that can't exist

[Yaël Dillies]

Isn't supr already akin finsum? Just a badly behaved one.

[Yaël Dillies]

I guess we could have a separate notation and a different naming convention (bcsupr anyone?), bur I'm not yet sure what the notation should look like.

[Floris van Doorn]

Yaël Dillies said:

Thinking about this again, Eric Wieser, should we have a dedicated API for ⨆ x : subtype p, f x?

I think we should have API for ⨆ x : s, f x, but we maybe already have that? It's way more common (for me) to work with sets than with subtypes, so I personally don't see the value of also having API for ⨆ x : subtype p, f x.

[Yaël Dillies]

Can't they be used interchangeably?

[Floris van Doorn]

more or less yes (not in rw/simp probably). I think it would be nicer if they are stated using sets instead of subtypes.

[Yaël Dillies]

I don't really see the point. subtype is morally more general.

[Floris van Doorn]

Note: Sup (f '' s) means the same, and has currently more API. I just think ⨆ x : s, f x is a much nicer way of writing this term.

[Yaël Dillies]

I am fighting my way through a possible API for conditional suprema in branch#convexity_modulus. If people have ocmments on which lemmas are worthy of living, that would be great.