# Zulip Chat Archive

## Stream: maths

### Topic: transporting measurability proofs

#### Koundinya Vajjha (Jul 03 2019 at 14:55):

I am stuck in a proof where I have a seemingly trivial goal: `measurable (λ (a : nnreal), a)`

.

Nothing I try seems to work!

I guess the section on measurable equivalences was set up to solve goals like this, but I'm not able to use it. I'd appreciate any help!

#### Mario Carneiro (Jul 03 2019 at 14:57):

`measurable_id`

?

#### Mario Carneiro (Jul 03 2019 at 14:58):

I'm not sure what you mean about measurable equivalences. As always with this kind of thing, there are a hundred implicit arguments so that line is insufficient context

#### Koundinya Vajjha (Jul 03 2019 at 15:00):

Riight. I have a lot of implicit arguments and `measurable_id`

doesn't work in the proof..

#### Mario Carneiro (Jul 03 2019 at 15:01):

well, MWE then

#### Mario Carneiro (Jul 03 2019 at 15:02):

I'm not sure how you expect me to know what the context is if there is something funky going on

#### Koundinya Vajjha (Jul 03 2019 at 15:05):

yes im working on a MWE, sorry i only realized about the implicit arguments after i posted the question

#### Mario Carneiro (Jul 03 2019 at 15:06):

you could also post your entire goal and/or the partial proof

#### Koundinya Vajjha (Jul 03 2019 at 15:25):

Here's the MWE:

import measure_theory.giry_monad universe u open measure_theory measure_theory.measure set section variables (α : Type*) (β : Type*) [measurable_space α] [measurable_space β] structure probability_measure extends measure_theory.measure α := (measure_univ : to_measure univ = 1) instance : has_coe_to_fun (probability_measure α) := ⟨λ_, set α → nnreal, λp s, ennreal.to_nnreal (p.to_measure s)⟩ variable (p : probability_measure α) lemma prob_diff {s₁ s₂ : set α}(h : s₂ ⊆ s₁) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : p (s₁ \ s₂) = p s₁ - p s₂ := by sorry lemma prob_univ : p univ = 1 := by sorry lemma mwe [measurable_space α] [measurable_space β] (f : α → probability_measure β) : ∀ t : set β, is_measurable t → measurable (λ b:α,(f b) t) → measurable (λ b:α,(f b) (- t)) := begin intros t ht hA, rw compl_eq_univ_diff, conv{congr, funext, rw [prob_diff _ _ (subset_univ _) is_measurable.univ ht]}, simp [prob_univ], apply measurable.comp hA, apply measurable.comp, apply measurable_sub, apply measurable_const, apply measurable_subtype_val, swap, apply measurable_of_continuous, apply nnreal.continuous_of_real, apply @measurable_id nnreal _, end end

#### Mario Carneiro (Jul 03 2019 at 15:27):

did you try `exact measurable_id`

?

#### Mario Carneiro (Jul 03 2019 at 15:27):

`apply measurable_id`

probably won't work because of the apply bug

#### Patrick Massot (Jul 03 2019 at 15:27):

Where is that "apply bug" emoticon again?

#### Koundinya Vajjha (Jul 03 2019 at 15:28):

pp.all trace

invalid type ascription, term has type @measurable.{?l_1 ?l_1} ?m_2 ?m_2 ?m_3 ?m_3 (@id.{?l_1+1} ?m_2) but is expected to have type @measurable.{0 0} nnreal (@subtype.{1} real (λ (r : real), @has_le.le.{0} real real.has_le (@has_zero.zero.{0} real (@no_zero_divisors.to_has_zero.{0} real (@domain.to_no_zero_divisors.{0} real real.domain))) r)) (@measure_theory.borel.{0} nnreal nnreal.topological_space) (@subtype.measurable_space.{0} real (λ (r : real), @has_le.le.{0} real real.has_le (@has_zero.zero.{0} real (@no_zero_divisors.to_has_zero.{0} real (@domain.to_no_zero_divisors.{0} real real.domain))) r) (@measure_theory.borel.{0} real (@uniform_space.to_topological_space.{0} real (@metric_space.to_uniform_space'.{0} real (@normed_field.to_metric_space.{0} real real.normed_field))))) (λ (a : nnreal), a)

#### Mario Carneiro (Jul 03 2019 at 15:28):

pp.all?

#### Mario Carneiro (Jul 03 2019 at 15:29):

well why didn't you say so

#### Mario Carneiro (Jul 03 2019 at 15:29):

it's not the same measure

#### Mario Carneiro (Jul 03 2019 at 15:29):

your MWE doesn't work for me, it fails at the first `apply`

#### Koundinya Vajjha (Jul 03 2019 at 15:30):

what's not the same measure?

#### Mario Carneiro (Jul 03 2019 at 15:30):

didn't `measurable.comp`

recently get its arguments flipped? I'm not sure if you or I are out of date

#### Koundinya Vajjha (Jul 03 2019 at 15:31):

I didn't update mathlib in a while

#### Mario Carneiro (Jul 03 2019 at 15:32):

`nnreal`

is defined to be `{r : ℝ // 0 ≤ r}`

, so it has a measurable space from `subtype`

applied to the measure on `real`

#### Mario Carneiro (Jul 03 2019 at 15:32):

but it is also a topological space and so it gets the borel measurable space

#### Koundinya Vajjha (Jul 03 2019 at 15:34):

yes, which is why i thought I should use `ennreal_equiv_nnreal`

and transport it somehow...

#### Mario Carneiro (Jul 03 2019 at 15:40):

this works for me:

lemma mwe [measurable_space α] [measurable_space β] (f : α → probability_measure β) (t : set β) (ht : is_measurable t) (hA : measurable (λ b:α, f b t)) : measurable (λ b:α, f b (- t)) := begin rw compl_eq_univ_diff, conv{congr, funext, rw [prob_diff _ _ (subset_univ _) is_measurable.univ ht]}, simp [prob_univ], refine measurable.comp _ hA, refine measurable.comp _ (measurable_sub measurable_const _), refine measurable_of_continuous nnreal.continuous_of_real, exact measurable_of_continuous nnreal.continuous_coe, end

#### Koundinya Vajjha (Jul 03 2019 at 15:45):

worked with some modifications for me as well. Thanks mario!

Last updated: May 18 2021 at 06:15 UTC