# 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 :=
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: Aug 03 2023 at 10:10 UTC