AEMeasurable fun_prop prod

Stream: mathlib4

[David Ledvinka]

In Mathlib.MeasureTheory.Measure.Prod the theorems AEMeasurable.fst and AEMeasurable.snd have a "TODO: make this theorem usuable with fun_prop". If you try to add a fun_prop declaration you get a error that says "Not a valid fun_prop theorem!" What is the issue here and what can I do to fix it?

[Tomas Skrivan]

fun_prop expects the theorem to be of the form AEMeasurable fun x => (f x).1 μ instead of having f x.1. Does it make sense to formulate it like that for AEMeasurable?

[Tomas Skrivan]

David Ledvinka said:

"Not a valid fun_prop theorem!" What is the issue here and what can I do to fix it?

The issue is similar to that fact that the head symbol of lhs of a simp theorem can't be a free variable. Similarly fun_prop does not allow free variable to be the head of the function body except for so called "lambda theorems"(described here)

[David Ledvinka]

I think I am still too new to formalization to give an informed answer to your general question but here is a MWE of my use case that lead me to investigate this:

import Mathlib.MeasureTheory.Measure.Prod

open ENNReal MeasureTheory

variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {f : α → ℝ≥0∞} {g : β → ℝ≥0∞}

-- Works!
example (hf : Measurable f) (hg : Measurable g) : Measurable (fun (x,y) ↦ f x * g y) := by
  fun_prop

variable {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν]

-- My use case doesn't work!
example (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
    AEMeasurable (fun (x,y) ↦ f x * g y) (μ.prod ν) := by
  fun_prop

-- Intermediate case doesn't Work!
example (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
    AEMeasurable (fun (x,y) ↦ (f x, g y)) (μ.prod ν) := by
  fun_prop

I suppose in the "Measurable" case this is a composition of lambda theorems but in the "AEMeasurable" case it is not?

[Floris van Doorn]

Tomas Skrivan said:

fun_prop expects the theorem to be of the form AEMeasurable fun x => (f x).1 μ instead of having f x.1. Does it make sense to formulate it like that for AEMeasurable?

That is a different theorem. Compare docs#Continuous.fst and docs#Continuous.fst'

[Floris van Doorn]

And yes, AEMeasurable is harder to support because the composition of two AEMeasurable functions is not necessarily AEMeasurable.

[Floris van Doorn]

But probably the way to go is to tag docs#MeasureTheory.Measure.QuasiMeasurePreserving, docs#AEMeasurable.comp_quasiMeasurePreserving and docs#MeasureTheory.Measure.quasiMeasurePreserving_fst with @[fun_prop], and then fun_prop can probably handle this.

[Tomas Skrivan]

I played with the code a bit and I can make fun_prop work by adding these two theorems

@[fun_prop]
theorem AEMeasurable.map_fst_measure (hf : AEMeasurable f μ) :
    AEMeasurable f ((μ.prod ν).map Prod.fst) := by
  simp; apply AEMeasurable.smul_measure hf

@[fun_prop]
theorem AEMeasurable.map_snd_measure (hg : AEMeasurable g ν) :
    AEMeasurable g ((μ.prod ν).map Prod.snd) := by
  simp; apply AEMeasurable.smul_measure hg

As you can see the proof uses simp and fun_prop is not doing any reduction on the goal.

Unfortunately it does not scale, this fails

example (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
    AEMeasurable (fun (x,y,z) ↦ (f x, g y, f z)) (μ.prod (ν.prod μ)) := by
  fun_prop

because fun_prop can't prove AEMeasurable (fun x0 => g x0) (Measure.map (fun x => x.2.1) (μ.prod (ν.prod μ)))

---

To make fun_prop work properly it would need a theorem of the form

@[fun_prop]
theorem AEMeasurable.measure_change (hf : AEMeasurable f μ) (h : P μ μ') :
    AEMeasurable f μ' := ...

where P is some appropriate predicate on μ and μ' which can be solve by some other tactic. With that you would run fun_prop with that tactic as discharger.

This theorem would be similar to how fun_prop uses ContDiff.of_le to prove ContDiff R n f from ContDiff R m f

[Tomas Skrivan]

Ohh, now I'm looking at the trace of fun_prop and there is such theorem AEMeasurable.mono'.

I will investigate why fun_prop is not reporting (you can see it in fun_prop trace only)

failed to discharge hypotheses
          Measure.map Prod.fst (μ.prod ν) ≪ μ

in

theorem AEMeasurable.map_fst_measure (hf : AEMeasurable f μ) :
    AEMeasurable f ((μ.prod ν).map Prod.fst) := by
  fun_prop

[Tomas Skrivan]

@David Ledvinka so for your example to work you just need to find a tactic that can solve

example : Measure.map Prod.fst (μ.prod ν) ≪ μ  := by <tactic>

and run fun_prop (disch:=<tactic>)

[Tomas Skrivan]

Tomas Skrivan said:

I will investigate why fun_prop is not reporting (you can see it in fun_prop trace only)

Ohh I know why, because with the current error reporting you would get

Measurable.aemeasurable, failed to discharge hypotheses,  Measurable fun a => f a
@AEMeasurable.mono', failed to discharge hypotheses, Measure.map Prod.fst (μ.prod ν) ≪ μ
@Continuous.aemeasurable, failed to synthesize instance, TopologicalSpace α
@Continuous.aemeasurable, failed to synthesize instance, OpensMeasurableSpace α
@Continuous.aemeasurable, failed to discharge hypotheses, OpensMeasurableSpace α

I consider all of these except one to be false positives. This is relatively simple example, I think on more complicated examples the number of false positives would much larger.

[David Ledvinka]

Tomas Skrivan said:

David Ledvinka so for your example to work you just need to find a tactic that can solve

example : Measure.map Prod.fst (μ.prod ν) ≪ μ  := by <tactic>

and run fun_prop (disch:=<tactic>)

This works thanks!

[Tomas Skrivan]

Cool, which tactic do you use to prove absolute continuity of measures? I couldn't figure it out.

[David Ledvinka]

I couldn't find one single tactic, I just did fun_prop (disch:= intro _ hs; simp [hs]). It works but is this discouraged? (The context I used it in is #24127)

[Tomas Skrivan]

It is totally valid thing to do. I was just hoping for something general that we can recommend to other people to do when proving AEMeasurable

[David Ledvinka]

Floris van Doorn said:

But probably the way to go is to tag docs#MeasureTheory.Measure.QuasiMeasurePreserving, docs#AEMeasurable.comp_quasiMeasurePreserving and docs#MeasureTheory.Measure.quasiMeasurePreserving_fst with @[fun_prop], and then fun_prop can probably handle this.

Ok so after running into this problem a bunch more I decided to go back and try this and it works! (Both for my example above as well as other examples). I am going to submit a PR for this (have a draft #24273) but I wanted to ask if there is a good rule of thumb when to label a theorem fun_prop and when not? Is it better to start conservative and just add more fun_prop tags when needed?

[David Ledvinka]

Could also do MeasurePreserving, is there a worry though that this will slow things down?

[Tomas Skrivan]

Reading this might give you a better idea of what theorems to mark with fun_prop https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp.html

[Tomas Skrivan]

David Ledvinka said:

Could also do MeasurePreserving, is there a worry though that this will slow things down?

That should not be a problem and if something gets suspiciously slow you can always turn on the trace set_option trace.Meta.Tactic.fun_prop true and see where fun_prop took the wrong turn and remove the offending theorem.