Order on measures

Stream: mathlib4

[Yury G. Kudryashov]

Currently, ≤ on measures is defined as ∀ s, MeasurableSet s → μ s ≤ ν s. I suggest that we redefine it as ∀ s, μ s ≤ ν s (now available as a lemma) for the following reasons:

• this way it is defeq to ≤ on outer measures;
• if we decide to introduce a Preorder/PartialOrder on all DFunLike types and migrate measures to FunLike, then this is unavoidable;
• the current reasoning is "it's slightly easier to prove μ ≤ ν this way"; the counter-argument is "it's slightly harder to apply μ ≤ ν this way".

[Yury G. Kudryashov]

I'll try to PR it today or tomorrow

[Yury G. Kudryashov]

• #10714 :: order on measures
• #10721 :: generic Preorder and PartialOrder on DFunLike

[Yury G. Kudryashov]

@Yaël Dillies This is my motivation for #10721

[Yaël Dillies]

That explains why you want an order on measures, but that doesn't explain why you want to do it via a fun-like-generic instance

[Yury G. Kudryashov]

I want lemmas like ae_mono to work both for measures and outer measures

[Yury G. Kudryashov]

/poll What should I do with #10721?
Leave as is (introduce generic Preorder on DFunLike)
Define an empty typeclass [PointwiseOrder] and enable this Preorder only if [PointwiseOrder] is present
Define a typeclass [PointwiseOrder] saying that the order (defined elsewhere) is equivalent to the pointwise one

[Yury G. Kudryashov]

@Yaël Dillies I see your examples for SetLike (though I'm not sure that a few exceptions justify changes to SetLike; another option is not to use SetLike for these types - let's discuss this elsewhere). Do you have examples of DFunLikes that have a natural non-pointwise order?

[Yury G. Kudryashov]

@Yaël Dillies :up:

[Yury G. Kudryashov]

@Anatole Dedecker Is there a reason to not have a nice defeq for le?

[Anatole Dedecker]

I think this could be annoying for the order on operators of a Hilbert Space. E.g for linear endomorphisms of $\mathbb{R}$ the order you want is not the pointwise order.

[Yury G. Kudryashov]

This explains why not option 1. Why not option 2?

[Anatole Dedecker]

I guess I don't quite understand option 2, I thought it was "make the instance localized" but upon rereading it is not.

[Yury G. Kudryashov]

It's about the following design (not copy+pasting from Lean, so may contain typos):

namespace DFunLike

variable {ι : Type*} {α : ι → Type*} {F : Type*}

class PointwiseOrder (F : Type*) : Prop where -- empty tag

instance [DFunLike F ι α] [∀ i, LE (α i)] [PointwiseOrder F] : LE F where
  le f g := ∀ i, f i ≤ g i

[Yury G. Kudryashov]

The main downside I see is that we can't do the same for PointwiseSup/PointwiseInf.

[Anatole Dedecker]

I guess the question is "are we likely to have orders which are propositionally the pointwise order but not definitionally". Right now I can't think of any, so I'm fine with option 2.

[Yury G. Kudryashov]

OK, I'll change my PR to option 2. We can migrate to option 3 later, if needed.

[Yaël Dillies]

Anatole Dedecker said:

I guess the question is "are we likely to have orders which are propositionally the pointwise order but not definitionally". Right now I can't think of any

One way it could show up is eg if we made (iota -> alpha) x (iota -> beta) be FunLike iota (alpha x beta). The order is defined as (\forall i, f.1 i <= g.1 i) \and (\forall i, f.2 i <= g.2 i), which is not defeq to \forall i, (f.1 i, f.2 i) <= (g.1 i, g.2 i).

[Yury G. Kudryashov]

Are we going to use DFunLike for something other than bundled morphisms?

[Yaël Dillies]

No, my example above is a toy example, but I am not yet convinced that bundled morphisms couldn't somehow disguise that example.

[Yaël Dillies]

Anyway, I would prefer n°3 on the grounds that we shouldn't create data out of nowhere

[Yury G. Kudryashov]

A bundled morphism is a specific type. We define order instances specific to this type.

[Yaël Dillies]

and nicely enough n°3 is very close to what's in !3#16351

[Yury G. Kudryashov]

There is a tradeoff between generality and availability of defeq lemmas...

[Yury G. Kudryashov]

BTW, how much does this design pattern affect instance args term sizes?

[Yury G. Kudryashov]

I mean, now we have just MyType.preorder, MyType.lattice etc, but with classes like PointwiseOrder, PointwiseSup, PointwiseBot etc, we'll get instances like DFunLike.Lattice [DFunLike F ι α] [∀ i, Lattice (α i)] [LE F] [LT F] [PointwiseOrder F ι α] [PointwiseSup F ι α] [PointwiseInf F ι α] : Lattice F

[Yury G. Kudryashov]

Is it better to have these generic instances, or a meta program that defines instances for each specific bundled hom?

[Yury G. Kudryashov]

The downside of meta programming approach is that we can't prove generic lemmas that involve different bundled homs.

[Yaël Dillies]

How many generic lemmas are there?

[Yaël Dillies]

Also surely you can still prove them if PointwiseOrder is a prop-valued mixin?

[Yaël Dillies]

What I'm more worried about is that you are about to create an asymmetry between ∀ i, π i and α × β

[Yaël Dillies]

Basically we're missing some idea here about how to deal with "coordinates" in types. See eg #10565 for a pain demonstration

[Antoine Chambert-Loir]

Browsing the files didn't help me understand what you meant here. Specifically, what do you find annoying/what part would you have wished to be easier?

[Yaël Dillies]

All the lemmas ending in _pi are true for any product of copies of ℝ equipped with the pointwise order (eg ℝ × ℝ, EuclideanSpace ι ℝ), not just ι → ℝ.

[Antoine Chambert-Loir]

Is it possible to have a predicate ‘IsProduct‘ that would allow to handle them simultaneously? This is kind of categorifying the library independently of the files on category theory, so might duplicate some work.

[Yaël Dillies]

I've been looking for something like that, yeah, but I haven't come with anything practical yet

[Yury G. Kudryashov]

We already have a few classes with instances for (conditionally complete) linear orders, pi types and products. E.g., docs#CompactIccSpace