Suprema and subtypes

Stream: Brownian motion

[David Ledvinka]

Could theorems with ⨆ (s) (t) (hs : s ∈ J) (ht : t ∈ J) be refactored to ⨆ (s) (hs : s ∈ J) (t) (ht : t ∈ J)? Its then easier to apply iSup_subtype lemmas when needed. Of course the sups could just be commuted in the proof but this ordering seems easier to work with unless the other ordering is easier elsewhere.

[Markus Himmel]

You can simp only [iSup₅_eq_iSup₂] :slight_smile:

[Rémy Degenne]

Markus added this: https://github.com/RemyDegenne/brownian-motion/blob/94609e4a4b5c14efd7b2fd56383305a735eb745c/BrownianMotion/Continuity/Chaining.lean#L213

[David Ledvinka]

Oh ok nice!

[Markus Himmel]

But yes, we're quite far along in Chapter 5 now, and by now it's pretty clear that refactoring the statements would make everything slightly cleaner overall. We should do it before PRing the material to mathlib.

[Rémy Degenne]

The proposal is to use these two forms for the suprema?

⨆ (s : {x : E // x ∈ C k}) (t : {x : E // x ∈ C k}), ...

⨆ (s : {x : E // x ∈ C k}) (t : {y : {x : E // x ∈ C k} // edist s y ≤ δ}), ...

If that's easier everywhere, let's change it in the project now. A volunteer?

[David Ledvinka]

I am about to sleep but if no one claims it by the time I wake up then I can do it.

[Markus Himmel]

I will do it now.

[Markus Himmel]

https://github.com/RemyDegenne/brownian-motion/pull/69 No surprises.

[Rémy Degenne]

Nice, thanks! And I see that the supremum is actually not as bad looking as what I wrote above, since it's ⨆ (s : C k) (t : { t : C k // edist s.1 t.1 ≤ δ }.

[Markus Himmel]

You can even write edist s t instead of edist s.1 t.1.

[Rémy Degenne]

Well, let me leave that as review comment on your PR then! I copied the code from there :)

[Markus Himmel]

Oh actually, I take it back. It goes though instPseudoEMetricSpaceSubtype.toEDist then instead of firing the coercions.

[Markus Himmel]

I'll go back and check if that's a problem.

[Markus Himmel]

Okay, seems fine to me.

[Rémy Degenne]

I am not sure of what exactly seems fine to you. The PR as it is now, or the removal of the .1?

[Markus Himmel]

Sorry, I meant that edist s.1 t.1 and edist s t are defeq in a completely benign way, so I don't see any potential problems with using one or the other or a mix of the two. So I'm happy with your changes removing the .1.