Zulip Chat Archive

Stream: general

Topic: nnreal.measurable_space = borel nnreal

Hunter Monroe (May 29 2021 at 18:15):

How can I prove the first of these? The second and third go through. This is from formal-ml, where I am fixing the proofs that no longer work with the current version of mathlib.

lemma nnreal_measurable_space_def:nnreal.measurable_space = borel nnreal := rfl lemma real_measurable_space_def:real.measurable_space = borel real := rfl lemma ennreal_measurable_space_def:ennreal.measurable_space = borel ennreal := rfl

Kalle Kytölä (May 29 2021 at 21:31):

I guess the current measurable space structure on nnreal is inherited from that of (which indeed is by definition the Borel sigma-algebra) via the inclusion coe : nnreal → ℝ, i.e., the measurable space is comap coe _. (At least this is where I got via subtype.measurable_space etc.)

In that case the relevant doc should be this.

Kalle Kytölä (May 29 2021 at 21:32):

I copy the existing code and docstring of comap below, because I have one tiny comment about the docstring, and more importantly the definition does not seem to behave the way I expected:

/-- The reverse image of a measure space under a function. `comap f m` contains the sets `s : set α`
  such that `s` is the `f`-preimage of a measurable set in `β`. -/
protected def comap (f : α  β) (m : measurable_space β) : measurable_space α :=
{ measurable_set'      := λ s, s', m.measurable_set' s'  f ⁻¹' s' = s,
  measurable_set_empty := , m.measurable_set_empty, rfl⟩,
  measurable_set_compl := assume s s', h₁, h₂⟩, s', m.measurable_set_compl _ h₁, h₂  rfl⟩,
  measurable_set_Union := assume s hs,
    let s', hs' := classical.axiom_of_choice hs in
     i, s' i, m.measurable_set_Union _ (λ i, (hs' i).left), by simp [hs']  }

Kalle Kytölä (May 29 2021 at 21:32):

It seems first of all that there is a tiny misprint in the docstring: "measure space" should be "measurable space".

Kalle Kytölä (May 29 2021 at 21:33):

But what I don't understand is why I fail to use this definition in my attempt below...

Otherwise the following should prove what @Hunter Monroe asked above (although the proof would anyway be terribly inelegant), but there is one really puzzling sorry in it (puzzling to me, at least):

import topology.instances.real
import topology.instances.nnreal
import measure_theory.borel_space
import measure_theory.measurable_space
import topology.algebra.ordered.basic

open set
open measurable_space

lemma open_imp_borel {γ : Type*} [top_γ : topological_space γ]
  {G : set γ} : is_open G  (borel γ).measurable_set' G := measurable_set_generate_from

lemma closed_imp_borel {γ : Type*} [top_γ : topological_space γ]
  {F : set γ} : is_closed F  (borel γ).measurable_set' F :=
  set G := F with hG ,
  have FeqGc := compl_compl F ,
  rw  hG at FeqGc ,
  intro hFclosed ,
  have Gmble := open_imp_borel (is_open_compl_iff.mpr hFclosed) ,
  rw  FeqGc ,
  exact (borel γ).measurable_set_compl G Gmble ,

lemma nnreal_measurable_space_def:nnreal.measurable_space = borel nnreal
  apply le_antisymm ,
  { intros B hB ,
    -- I thought the following `suffices` is what `subtype.measurable_space`
    -- literally means by definition, but...
    suffices :  (s' : set ) , real.measurable_space.measurable_set' s'  (coe⁻¹' s') = B ,
    { cases this with C hC ,
      -- use C , -- I expected this to lead to a goal which is just `hC`...
      -- ...but it leads to a strange goal requiring to prove openness of `C`!
      -- Am I using `use` incorrectly to provide the set required by the ∃
      -- in `∃s', m.measurable_set' s' ∧ f ⁻¹' s' = s,` ?
      sorry , } ,
    rcases hB with  A , mble_A , hAB  ,
    set A' := A  {x :  | 0  x} with hA' ,
    set H := {x :  | 0  x} with hH ,
    have clos_H : is_closed H := is_closed_ge' 0 ,
    have mble_A' : real.measurable_space.measurable_set' A' ,
    { apply measurable_set.inter mble_A (closed_imp_borel clos_H) , } ,
    have key : (coe⁻¹' A') = B := by tidy ,
    use [A' ,  mble_A' , key ⟩] , } ,
  { suffices :  (U : set nnreal), is_open U  nnreal.measurable_space.measurable_set' U ,
    { exact opens_measurable_space.borel_le , } ,
    intros U hU ,
    have key :  (V : set ), is_open V  (coe⁻¹' V) = U := by tidy ,
    rcases key with  V , V_open , hVU  ,
    use V ,
    exact  open_imp_borel V_open , hVU  , } ,

Kalle Kytölä (May 29 2021 at 21:59):

Btw, I started fiercely hitting the keyboard in the above as if it was a level of the NNG :) --- i.e., without thinking.

I guess the right way would instead be to prove that subtype.measurable_space of any borel_space is the borel space on the subtype (perhaps one needs the assumption that the subtype was a Borel set to start with...). But much of the above should already work to that case.

I didn't immediately find that in the library, though.

Kalle Kytölä (May 29 2021 at 22:26):

In fact, unsurprisingly the right way (namely via subtype.borel_space) is already in measure_theory.borel_space, and the following works:

import measure_theory.borel_space

lemma nnreal_measurable_space_def:nnreal.measurable_space = borel nnreal
  exact borel_space.measurable_eq ,

Sorry about the thoughtless answer before! (Although I still don't understand why use didn't work in it... I would appreciate if someone is able to clarify it to me.)

Last updated: Aug 03 2023 at 10:10 UTC