The sigma algebra generated by a family of measurable fcts

Stream: maths

[Golol]

Alright, so today I managed to formalize this and proof some lemmas about it, with the idea of trying to do something which could theoretically, possibly, actually be used in the mathlib.
What I am looking for is feedback on what would keep this from getting added to the mathlib.
Some points:
1) The proofs are surely way longer than they need to be - Theoretically only an aesthetic issue but it would probably not be nice to have walls of tactics when a short, elegant proof does the job. In particular I suspect that the correct usage of some lemmas already in the mathlib would have made things smoother.
2) Some of the arguments should probably be implicit but for now I just kept it simple.
3) Are these kinds of lemmas worthwhile? Do they actually exist alreadyß

import measure_theory.measurable_space

universes u v w

variables {α β γ : Type u}


/--- the induced σ-algebra of a family of functions --/
protected def comap_family (I : Type u) (f: I -> α -> β) (m : measurable_space β) :
  measurable_space α :=
  have is_measurable' : set α -> Prop, from
  λ (a : set α), ∃ i : I, (measurable_space.comap (f i) m).is_measurable' a,
  measurable_space.generate_from {a : set α | is_measurable' a}

/-- the induced σ-algebra makes all functions of the family measurable --/
lemma comap_family_all_measurable (I : Type u) (f : I -> α -> β) (m : measurable_space β) :
  ∀ i : I, @measurable α β (comap_family I f m) m (f i) :=
  λ (i : I), iff.mpr (@measurable_iff_comap_le α β (comap_family I f m) m (f i))
  begin
    intro a,
    unfold comap_family,
    intro h,
    unfold measurable_space.generate_from,
    simp,
    have p : a ∈ {a : set α | ∃ (i : I), (measurable_space.comap (f i) m).is_measurable' a},
      exact ⟨ i, h ⟩,
    generalize q : {a : set α | ∃ (i : I), (measurable_space.comap (f i) m).is_measurable' a} = x,
    have hp : a ∈ x,
      rw eq.symm q, exact p,
    exact @measurable_space.generate_measurable.basic α x a hp,
  end

/-- The function is monotone w.r. to inclusion on the index set and measurable spaces --/
lemma comap_le_if_family_le (I: Type u) (f: I -> α -> β) (m : measurable_space β)
  (J : Type u) (inj : J -> I) (hinj: function.injective inj) :
  comap_family J (λ j, f (inj j)) m ≤ comap_family I f m :=
  begin
    intro a,
    unfold comap_family,
    apply measurable_space.generate_from_le_generate_from,
    simp,
    intro b,
    intro j,
    intro h,
    exact ⟨ inj j, h ⟩,
  end

/-- The σ-algebra generated by a measurable space is the space itself --/
lemma generate_from_measurable_space_id (m : measurable_space β) :
  measurable_space.generate_from (set_of m.is_measurable')
  = m :=
  begin
    unfold set_of,
    ext x,
    unfold measurable_space.generate_from,
    simp,
    split,
    intro h,
      induction h,
      exact h_H,
      exact m.is_measurable_empty,
      exact m.is_measurable_compl h_s h_ih,
      exact m.is_measurable_Union h_f h_ih,
    intro h,
    exact @measurable_space.generate_measurable.basic β m.is_measurable' x h,
    end

/-- THe function comap_family is a generalization - in the case that the Index type has one element,
it reduces to comap --/
lemma comap_family_is_comap_for_singleton (I : Type u) (h : ∀ (i j : I), i = j)
  (f: I -> α -> β) (m : measurable_space β) :
  ∀ (i : I), comap_family I f m = measurable_space.comap (f i) m :=
  begin
    intro i,
    unfold comap_family,
    simp,
    have hp : (∀ (a : set α), (∃ (i : I),
        (measurable_space.comap (f i) m).is_measurable' a)
        ↔ (measurable_space.comap (f i) m).is_measurable' a),
      intro a,
      apply iff.intro,
      intro h,
        cases h with hx hy,
        rw h i hx,
        apply hy,
      intro h,
        exact ⟨ i, h ⟩,
    have hq : {a : set α | ∃ (i : I), (measurable_space.comap (f i) m).is_measurable' a}
        = {a : set α | (measurable_space.comap (f i) m).is_measurable' a},
      ext a,
      simp,
      exact hp a,
    rw hq,
    simp,
    exact generate_from_measurable_space_id (measurable_space.comap (f i) m),
  end

[Mario Carneiro]

Looking at comap_family, my first thought is to try to factor it into two parts: constructing a measurable space from a family of measurable spaces, and pulling back a measurable space along a function

[Mario Carneiro]

the latter we already have, that's comap, and the former is the lattice operation on measurable_space (which is a complete lattice IIRC)

[Golol]

Would the product be the sigma algebra generated by the finite dimensional cylinder sets?

[Mario Carneiro]

It's just \bigcap i, m i

[Mario Carneiro]

it's the supremum (or infimum, I always get them mixed up) of the family of measurable spaces

[Mario Carneiro]

you certainly don't need any generate_from stuff, and that will hugely simplify the proofs

[Mario Carneiro]

/--- the induced σ-algebra of a family of functions --/
protected def comap_family (I : Type u) (f: I -> α -> β) (m : measurable_space β) :
  measurable_space α := ⨆ i, m.comap (f i)

lemma comap_family_all_measurable (I : Type u) (f : I -> α -> β) (m : measurable_space β)
  (i : I) : @measurable α β (comap_family I f m) m (f i) :=
measurable_iff_comap_le.2 (le_supr _ i)

lemma comap_le_if_family_le (I: Type u) (f: I -> α -> β) (m : measurable_space β)
  (J : Type u) (inj : J -> I) (hinj: function.injective inj) :
  comap_family J (λ j, f (inj j)) m ≤ comap_family I f m :=
supr_le $ λ j, measurable_iff_comap_le.1 $ comap_family_all_measurable I f m (inj j)

lemma comap_family_is_comap_for_singleton (I : Type u) [subsingleton I]
  (f: I -> α -> β) (m : measurable_space β) (i : I) :
  comap_family I f m = m.comap (f i) :=
le_antisymm (supr_le $ λ j, by cases subsingleton.elim i j; refl') (le_supr _ i)

[Mario Carneiro]

I think there are some missing theorems about measurable functions wrt the supr measurable space though

[Patrick Massot]

If this is true then the proofs of these missing theorems should be verbatim copy of the corresponding topological theorems.

[Mario Carneiro]

I think they are, more or less

[Golol]

Oh that makes me realize, I actually wanted to do this for a family f_i -> \b_i, the target spaces should change. I should generalize it.
My plan is to follow a script I have on stochastic processes. There is this basic theorem which tells you that the obvious choices for sigma algebras for your stochastic process are the same and you dont have to worry, would be nice to have that.

[Mario Carneiro]

The point I'm making is that you don't really need this definition because it factors cleanly into two more reusable parts (about which we already have a bunch of theorems)

[Mario Carneiro]

if you wanted the measurable spaces to change, it would just become ⨆ i, (m i).comap (f i) instead

[Golol]

Ah yes yes, I realized that. I just want to practice doing some "theorybuilding" in lean. And if an earlier definition in the theory is inefficient, then that can be generalized later I suppose.

[Mario Carneiro]

Yes, as always it is getting the definitions right that is the hard part

[Mario Carneiro]

One way to do theory building would be to pick a target theorem and figure out what the library would need to state and prove the theorem, like the planning phase of an expedition

[Mario Carneiro]

make sure that all the theorems are easy to state and all the notions involved have enough API theorems to be usable together