ae of a finite measure

Stream: mathlib4

[Yaël Dillies]

@Yury G. Kudryashov recently generalised docs#MeasureTheory.ae so that it would work with μ : OuterMeasure Ω. However as a result it doesn't work with μ : FiniteMeasure Ω (nor μ : ProbabilityMeasure Ω) anymore.

[Yaël Dillies]

The reason is that, when μ : FiniteMeasure Ω, we were able to just write f =ᵐ[μ] g and Lean would automatically insert the coercion to get f =ᵐ[↑μ] g, as opposed to now where it tries to synthesize OuterMeasureClass (FiniteMeasure Ω) (Set Ω) ℝ≥0∞, which doesn't exist.

[Yaël Dillies]

I see four ways out:

1. Write f =ᵐ[(μ : Measure Ω)] g everywhere. Kind of defeats the point of having a notation in the first place.
2. We add FunLike and OuterMeasureClass instances for FiniteMeasure Ω/ProbabilityMeasure Ω. I am doing that in #13171 because that's needed anyway for other reasons (the CoeFun for FiniteMeasure Ω/ProbabilityMeasure Ω unfolds to a lambda, so simp can't index any lemma of the form ⇑μ _ = _). However there is a catch: The instance I'm adding is OuterMeasureClass (FiniteMeasure Ω) (Set Ω) ℝ≥0, not OuterMeasureClass (FiniteMeasure Ω) (Set Ω) ℝ≥0∞ and I don't think we want the latter. So that doesn't really solve the problem unless we also generalise away the ℝ≥0/ℝ≥0∞ codomain, which sounds like overengineering.
3. We revert the generalisation.
4. We write a more robust elaborator for f =ᵐ[μ] g. Then we might want to reconsider the generalisation: There might be a way to not introduce OuterMeasureClass by getting the elaborator to do more work.

[Yaël Dillies]

I think (4) is the only reasonable alternative.

[Yaël Dillies]

Context is bumping PFR: https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture

[Sébastien Gouëzel]

The generalization is not just to have the notation f =ᵐ[μ] g, it's mainly to be able to prove simultaneously many lemmas both for measures and outer measures, see the content of the file MeasureTheory.OuterMeasure.Basic.

I agree with you that the natural FunLike instance on FiniteMeasure takes values in ℝ≥0, not ℝ≥0∞. And still it would be nice to be able to talk about ae μ in a transparent way when μ is a finite measure. Would it work to not use the FunLike mechanism for OuterMeasureClass, but instead register a tailor-made class?

[Sébastien Gouëzel]

I am answering my own question: not really, because lemmas in MeasureTheory.OuterMeasure.Basic are phrased in terms of the FunLike instance, so if there is no such instance then the lemmas can't even be stated.

[Yaël Dillies]

Yep. The one way to solve it would be axiomatise ℝ≥0/ℝ≥0∞

[Yaël Dillies]

Sébastien Gouëzel said:

The generalization is not just to have the notation f =ᵐ[μ] g, it's mainly to be able to prove simultaneously many lemmas both for measures and outer measures, see the content of the file MeasureTheory.OuterMeasure.Basic.

Yes, I am aware.

[Sébastien Gouëzel]

I'd say for now the reasonable solution is to use f =ᵐ[(μ : Measure Ω)] g just for the bump, and see if we can improve the elaborator. It's not unreasonable: we are really using the coercion to measures, after all!

[Richard Osborn]

Could this be solved with scoped notation overriding f =ᵐ[μ] g?

[Yaël Dillies]

Yeah sure, but like the notation should Just Work :tm:

[Yaël Dillies]

Yaël Dillies said:

2. We add FunLike and OuterMeasureClass instances for FiniteMeasure Ω/ProbabilityMeasure Ω.

Update: #13171 now passes CI. I don't think it will directly help with the problem at hand, but at least it won't hurt

[Yury G. Kudryashov]

I can generalize to NNReal/ENNReal this weekend. I'm sorry for breaking it for you.

[Sébastien Gouëzel]

Is there really anything to generalize? Even when mu is a FiniteMeasure, the associated a.e. filter should be the one associated to the corresponding measure, right? The problem is more that the notation f =ᵐ[μ] g is not firing because the coercion from finite measures to measures can not be inserted automatically here. In an ideal world, this notation could mean: if μ is an OuterMeasureClass, then use it, otherwise try to coerce μ to a measure. In the real world, I think I like Richard's idea to have a scoped notation that would insert the coercion to measures (so, it would fail for outer measures, but work for FiniteMeasure or ProbabilityMeasure) that one would activate when needed. Since one essentially never uses FiniteMeasure and OuterMeasure simultaneously, this should be essentially optimal, right?

[Yaël Dillies]

Sébastien Gouëzel said:

Since one essentially never uses FiniteMeasure and OuterMeasure simultaneously, this should be essentially optimal, right?

Lean 4's notation capabilities are so great that I say "No, we can make one notation work in all cases".

[Yaël Dillies]

It's not very hard, just some expected type manipulation. If nobody has managed it in 10 days (aka when my exams end), I'll do it quickly

[Yaël Dillies]

I have opened #13740, but I need help