Delete or rename AEMeasurable.fst and AEMeasurable.snd

Stream: mathlib4

[David Ledvinka]

In an effort to make fun_prop better at proving AEMeasurable I want to add the lambda theorems AEMeasurable.fst and AEMeasurable.snd in the form they are given here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp.html. Note this is also the form that Measurable.fst, Measurable.snd (and other fun_prop) theorems take. Currently AEMeasurable.fst and AEMeasurable.snd express a different theorem (which can't even be used by fun_prop). I would like to remove or rename these theorems but wanted to check if this was ok first. All of its uses can be easily replaced by fun_prop. Perhaps sometimes the proof term is preferable though? If you think I should just rename the theorems let me know what I should rename them to (I don't believe the corresponding theorem exists for any of the other fun_prop theorems as far as I could tell). I have a draft #24273 which removes all uses.

[Yury G. Kudryashov]

They should be renamed to comp_fst/comp_snd.

[Yury G. Kudryashov]

Same for docs#AEStronglyMeasurable.fst. I have a WIP PR #24248 that needs them and adds versions for Integrable (under certain assumptions).

[Yury G. Kudryashov]

BTW, please make the new fst/snd theorems protected.

[David Ledvinka]

Ok I changed the name for AEStronglyMeasurable and StronglyMeasurable as well and then proved the appropriate lambda lemmas for both these classes.

[Yury G. Kudryashov]

I've left some minor comments on Github.

[Eric Wieser]

Yury G. Kudryashov said:

They should be renamed to comp_fst/comp_snd.

Are you suggesting that the majority of the *able API should gain comp_ in it's name?

[Eric Wieser]

E.g docs#Differentiable.fst

[Eric Wieser]

Ah nevermind, I guess the rule you propose is only to do so for precomposition

[David Ledvinka]

Currently for some of these APIs .fst and .snd mean precomposition and sometimes it means postcomposition, so the goal of this PR is to standardize it.

[Yury G. Kudryashov]

E.g., for continuity we have docs#continuous_fst, docs#Continuous.fst, and docs#Continuous.fst'

[Yury G. Kudryashov]

We should choose a naming scheme here and follow it for all properties. I have no preference on which of the natural naming schemes is used.

[Floris van Doorn]

I'm happy with the comp_fst/comp_snd naming scheme.

[David Ledvinka]

So the proposal is:

xable_fst : Xable Prod.fst
Xable.fst : Xable (fun x => (f x).1)
Xable.comp_fst : Xable (fun x => f x.1)

Should I deprecate Continuous.fst' and make it an alias of Continuous.comp_fst?

[Yaël Dillies]

Ì don't think that's so good, because you're losing out on the new anonymous dot notation possibilities

[Yaël Dillies]

What about

Foo.fst : Foo Prod.fst
Foo.fst_comp : Foo fun x  ↦ (f x).1
Foo.comp_fst  : Foo fun x  ↦ f x.1

[David Ledvinka]

That is probably the most sensible name-wise but would be a much larger change (I think all of the xable_fstexamples are currently consistent with the proposal I mentioned). I can work on this if people think its worth it though.

[Yury G. Kudryashov]

How should we name lemmas like docs#MeasureTheory.integral_prod_swap docs#MeasureTheory.integral_fun_fst docs#MeasureTheory.integral_fn_integral_add ?

[Floris van Doorn]

Yaël Dillies said:

What about

Foo.fst : Foo Prod.fst
Foo.fst_comp : Foo fun x  ↦ (f x).1
Foo.comp_fst  : Foo fun x  ↦ f x.1

The lemmas Foo.fst_comp are the most useful, so I would prefer to have the shortest names for them.
Also dot notation for Foo Prod.fst isn't that useful, since you usually want to compose it with other Foo-lemmas, and .fst.fst_comp (in your naming scheme) doesn't elaborate correctly, since Lean doesn't know the type of the .fst.

[Eric Wieser]

David Ledvinka said:

So the proposal is:

xable_fst : Xable Prod.fst
Xable.fst : Xable (fun x => (f x).1)
Xable.comp_fst : Xable (fun x => f x.1)

Should I deprecate Continuous.fst' and make it an alias of Continuous.comp_fst?

What about the case where xable is a def like deriv or integral (as Yury asked above), and there is no namespace to hide in to disambiguate the first two?

[David Ledvinka]

I was only thinking about function properties but it does appear fderiv uses this as well. fderiv_fst gives the theorem about the derivative of Prod.fst, whereas fderiv.fst gives the theorem about the derivative of (fun x => (f x).1)

[Eric Wieser]

I think docs#fderiv.fst goes against #naming in that . is not appropriate here

[Yaël Dillies]

Floris van Doorn said:

dot notation for Foo Prod.fst isn't that useful, since you usually want to compose it with other Foo-lemmas

FWIW that's not really my experience. My code was littered with continous_id.neg at some point

[David Ledvinka]

So should we go with @Yaël Dillies suggestion? should I make some sort of poll? I have no strong opinions and my main desire is to get

AEMeasurable (fun x  => (f x).1)
AEMeasurable (fun x  => (f x).2)

as theorems in Mathlib so that I can use them with fun_prop, but I am happy to work on a refactor if we can come to a consensus.

[Yaël Dillies]

I am happy with my own suggestion :smile:

[Bhavik Mehta]

Yaël Dillies said:

FWIW that's not really my experience. My code was littered with continous_id.neg at some point

I don't think that's disagreeing with Floris' point (and I agree with his point), the idea is that Foo Prod.fst : Foo.fst would correspond to continuous_id : Continuous id here, and changing to Continuous.id would be .id.neg, which in your situation wouldn't have worked.

[Yaël Dillies]

No, the idea is that Continuous.neg would mean Continuous fun x ↦ -x and then my continous_id.neg would have been .neg.