## 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 :=
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ä (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
:=
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.)

Last updated: Dec 20 2023 at 11:08 UTC