nnreal.measurable_space = borel nnreal

Stream: general

[Hunter Monroe]

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ä]

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ä]

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ä]

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

[Kalle Kytölä]

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 :=
begin
  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 ,
end


lemma nnreal_measurable_space_def:nnreal.measurable_space = borel nnreal
  :=
begin
  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 ⟩ , } ,
end

[Kalle Kytölä]

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ä]

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
  :=
begin
  exact borel_space.measurable_eq ,
end

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.)