measurability lemma for sums/products of functions

Stream: mathlib4

[Terence Tao]

The existing lemmas docs#Finset.measurable_sum, docs#Finset.measurable_prod don't directly show measurability of a sum or product of functions, if one operates on the function directly rather than at a pointwise level. This seems to require a small additional lemma:

@[to_additive (attr := fun_prop, measurability)]
theorem Finset.measurable_prod_func {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f i)) :
Measurable (∏ i ∈ s, f i) := by
  convert Finset.measurable_prod s hf
  simp only [prod_apply]

With this, measurability works fine for sums/products of functions. Perhaps this can go into mathlib if it isn't duplicating any existing functionality?

[Floris van Doorn]

I think this is fine/good to add to Mathlib.

[Terence Tao]

More generally, many of the operations involving function manipulation are not currently caught by measurability, including some that are definitionally equivalent to ones that are. For instance, I think one needs a lemma like this in order to show measurability of a sum or product of measurable functions directly from measurability:

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem Measurable.mul_func {M : Type u_2} {α : Type u_3} [MeasurableSpace M]
  [Mul M] {m : MeasurableSpace α} {f g : α → M} [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable g) :
   Measurable (f * g) := Measurable.mul hf hg

[Floris van Doorn]

fun_prop is (IMO) a better tactic that unifies continuity, measurability (except the reasoning about MeasurableSet) and other function-properties. I believe it can deal with Measurable (f * g) (but I'm not sure).

[Floris van Doorn]

I checked, this works:

import Mathlib

theorem Measurable.mul_func {M : Type u_2} {α : Type u_3} [MeasurableSpace M]
  [Mul M] {m : MeasurableSpace α} {f g : α → M} [MeasurableMul₂ M] (hf : Measurable f) (hg : Measurable g) :
   Measurable (f * g) := by fun_prop

Using show_term you can see it uses docs#Measurable.mul'. I believe these pointwise operations are special-cased (simplified?) in the logic of fun_prop.

[Floris van Doorn]

(cc @Tomas Skrivan)

[Terence Tao]

Is the long term plan to phase out measurability, continuity, etc. in favor of fun_prop? Or at least to add to the documentation that fun_prop is a preferable tool?

[Floris van Doorn]

#25241 addresses your second question (good idea!)

[Floris van Doorn]

I'd be happy to phase out continuity. measurability is a bit trickier, since it also proves MeasurableSet statements, which presumably falls outside the scope of fun_prop.

[Yaël Dillies]

My hope is that measurability could become a wrapper around fun_prop + some MeasurableSet reasoning

[Tomas Skrivan]

As there is docs#Measurable.mul' variant for docs#Measurable.mul there is also docs#Finset.measurable_prod' variant for docs#Finset.measurable_prod the only issue is that it assumes (hf : ∀ (i : ι), Measurable ↿(f i)) and not (hf : ∀ i ∈ s, Measurable ↿(f i))

import Mathlib

-- `hf` is `∀ i : ι, ...`
theorem Finset.measurable_prod_func {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι) (hf : ∀ i, Measurable (f i)) :
Measurable (∏ i ∈ s, f i) := by
  fun_prop

@[fun_prop]
theorem Finset.measurable_prod'' {M ι α β : Type*}  [CommMonoid M]
  [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {f : ι → α → β → M} {g : α → β} {s : Finset ι}
  (hf : ∀ i ∈ s, Measurable ↿(f i)) (hg : Measurable g) :
  Measurable fun a => (∏ i ∈ s, f i a) (g a) := sorry

-- `hf` is `∀ i ∈ s, ...`
theorem Finset.measurable_prod_func' {M : Type u_2} {ι : Type u_3} {α : Type u_4} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f i)) :
Measurable (∏ i ∈ s, f i) := by
  fun_prop (disch:=assumption)

Maybe Finset.measurable_prod' should be generalized to this version and assumption discharger(which solves i ∈ s) should be enabled by default.

However not having the current version of Finset.measurable_prod' would likely require havingapply Finset.mem_univ as part of the default discharger to cover this case

import Mathlib

example {M : Type u_2} {ι : Type u_3} {α : Type u_4} [MeasurableSpace M] [MeasurableSpace α] {f : ι → α → M} (s : Fintype ι) (hf : ∀ i ∈ Finset.univ, Measurable (f i)) :
∀ i, Measurable (f i) := by
  fun_prop (disch:=apply Finset.mem_univ)

[Tomas Skrivan]

Floris van Doorn said:

believe these pointwise operations are special-cased (simplified?) in the logic of fun_prop.

fun_prop is not doing any special casing for arithmetic operations. (f * g) x = f x * g x can be only prepositionally equal and fun_prop would work the same which is the case for (∏ i ∈ s, f i) x = ∏ i ∈ s, f i x.

[Tomas Skrivan]

Floris van Doorn said:

I'd be happy to phase out continuity. measurability is a bit trickier, since it also proves MeasurableSet statements, which presumably falls outside the scope of fun_prop.

Since measurability is just a customized aesop tactic you can easily call fun_prop (disch:=aesop) or even fun_prop (disch:=measurability) and the discharger is called only on subgoals that are not fun_prop goals.

Having to specify discharger is a stumbling block for beginners though. I see two options:

1. Using autoParam and make fun_prop call them automatically. For example:

@[fun_prop]
theorem measurable_to_nat' {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℕ}
  (hf : ∀ (y : α), MeasurableSet (f ⁻¹' {f y}) := by aesop) : Measurable f := sorry

and when fun_prop tries to apply this theorem it will automatically call aesop on hf without the user explicitly writing (disch := aesop)

2. Specify the "auto param" in the attribute

@[fun_prop (hf := by aesop)]
theorem measurable_to_nat' {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℕ}
  (hf : ∀ (y : α), MeasurableSet (f ⁻¹' {f y})) : Measurable f := sorry

The downside of 1 is that it changes the API of the theorem and forces the autoParam on all other usecases and the downside of 2 is slightly unfamiliar syntax. Of course both can be implemented and it is up to users to decide what is preferable.

(Is there a better example of Measurable theorem requiring MeasurableSet than docs#measurable_to_nat ?)

[Floris van Doorn]

Tomas Skrivan said:

As there is docs#Measurable.mul' variant for docs#Measurable.mul there is also docs#Finset.measurable_prod' variant for docs#Finset.measurable_prod the only issue is that it assumes (hf : ∀ (i : ι), Measurable ↿(f i)) and not (hf : ∀ i ∈ s, Measurable ↿(f i))

Fixed in #25254.
I realize that the default discharger for fun_prop is "do nothing and fail". Maybe that could be something cheap, like solve_by_elim?

[Tomas Skrivan]

Floris van Doorn said:

solve_by_elim

Maybe, for solve_by_elim you have to provide set of theorems, right? What should this set be such that it does not cause slowdowns.

Probably something that can solve very quickly goals like i ∈ Finset.univ n ≤ n``1 ≤ 2 0 ≤ 1 0 ≤ 2 0 ≠ 1 True but more importantly it should fail very quickly on everything else.