Measurability of entries of matrix and fun_prop

Stream: mathlib4

[Fred Rajasekaran]

I am trying add the fun_prop attribute to the following lemma:

@[fun_prop]
lemma measurable_entry {m n : ℕ} (X : Ω → Matrix (Fin m) (Fin n) α) (hX : Measurable X) :
∀ (i : Fin m) (j : Fin n), Measurable (fun ω ↦ X ω i j) := by
  intros i j
  fun_prop

(the MeasurableSpace structure on Matrix (Fin m) (Fin n) α is the product one where α is a MeasurableSpace). However, I get an error Not a valid `fun_prop` theorem!. I believe it has to do with the ∀ (i : Fin m) (j : Fin n) part (correct me if I'm wrong please). What's the correct way to state this and still have a lemma with the fun_prop attribute that states that the entries are measurable functions?

[Ruben Van de Velde]

It would be helpful to make your code a #mwe

[Michael Rothgang]

A #mwe would be helpful: barring that, here's my guess how to rephrase your code:

@[fun_prop]
lemma measurable_entry {m n : ℕ} (X : Ω → Matrix (Fin m) (Fin n) α) (hX : Measurable X) (i : Fin m) (j : Fin n) :
Measurable (fun ω ↦ X ω i j) := by
  fun_prop

[Michael Rothgang]

The mathlib style guide https://leanprover-community.github.io/contribute/style.html has a section "hypotheses left of colon", which tells you to do exactly this.

[Michael Rothgang]

If fun_prop can prove your goal, you need not (but still can) mark your lemma as fun_prop.

[Eric Wieser]

I would not expect fun_prop to prove this unless the lemma already exists

[Etienne Marion]

fun_prop does work, although the error is still here:

import Mathlib

variable (α Ω : Type*) [MeasurableSpace α] [MeasurableSpace Ω]

instance (m n : ℕ) : MeasurableSpace (Matrix (Fin m) (Fin n) α) := inferInstanceAs <| MeasurableSpace <| (Fin m) → (Fin n) → α

@[fun_prop]
lemma measurable_entry {m n : ℕ} (X : Ω → Matrix (Fin m) (Fin n) α) (hX : Measurable X) (i : Fin m) (j : Fin n) :
    Measurable (fun ω ↦ X ω i j) := by
  fun_prop

[David Ledvinka]

I believe this can't be a fun_prop lemma because fun_prop does not allow the head of a function body to be a free variable unless its in the form of one of the lambda theorems listed here. Its not really a problem here though since fun_prop can prove it (its just a composition of lambda theorems as show_term fun_prop reveals)

[Tomas Skrivan]

David Ledvinka said:

I believe this can't be a fun_prop lemma because fun_prop does not allow the head of a function body to be a free variable unless its in the form of one of the lambda theorems listed here. Its not really a problem here though since fun_prop can prove it (its just a composition of lambda theorems as show_term fun_prop reveals)

It is exactly as you say. fun_prop can figure out that the theorem is just a consequence of Measurable.comp' and measurable_pi_apply. Therefore there is not need to mark this theorem with fun_prop.

[Tomas Skrivan]

Just few thoughts on this. In a way, for A : Matrix m n R and i : m, j : n the expression A i j is defeq abuse. Similar, for x : WithLp 2 (Fin n → ℝ) and i : Fin n we could consider x i a defeq abuse.

If Matrix would be one field structure

structure Matrix (m n R : Type*) where
  data : m → n → R

then evaluation for A : Matrix m n R, i : m, j : n would be A.data i j and

lemma measurable_entry {m n : ℕ} (X : Ω → Matrix (Fin m) (Fin n) α) (hX : Measurable X) :
∀ (i : Fin m) (j : Fin n), Measurable (fun ω ↦ (X ω).data i j) := ...

would be a valid fun_prop theorem as the head of the function body is Matrix.data.

[Eric Wieser]

I guess we could even call data row, and have a delaborator for A.row i j