fun_prop with maxTransitionDepth > 1

Stream: mathlib4

[Luigi Massacci]

Hello.

Q: Is there an opinion mathlib-wise on using fun_prop with maxTransitionDepth set to something greater than 1? Grepping for it, it appears to have never been used, so I was wondering if this is because it is considered bad practice or if it just hasn't happened yet.

Context: I'm using LocallyIntegrable a lot, so I put a bunch of fun_prop attributes on it (as well as IntegrableOn and LocallyIntegrableOn, all of which currently have none), but most of the time the result I want is a chain of LocallyIntegrableOn -> IntegrableOn -> Integrable so I need to set the depth to 2. It seems to me that LocallyIntegrableOn lemmas are always going to be used this way more or less anyway.

[Floris van Doorn]

I don't think that there is anything wrong with increasing maxTransitionDepth. Please experiment with it, and report back your findings!

[Tomas Skrivan]

The decision to set it to one was somewhat arbitrary. The thinking was partially that the theorems are usually transitively closed anyway i.e. if there is IntegrableOn -> LocallyIntegrableOn and Integrable -> IntegrableOn then there is usually Integrable -> LocallyIntegrableOn theorem and the transition depth can be one.

Keeping the transition depth low also keeps the search space smaller but I haven't done much testing to see if that is really the case.

So you can do

• Integrable -> LocallyIntegrableOn
• set maxThransitionDepth to two or larger

Either should be fine.

[Luigi Massacci]

Yes I was thinking along the lines that increasing it might cause a terrible slowdown. Adding a relevant lemma (maybe it's already there and only has to be marked too) sounds like a good idea regardless. Thank you