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

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)


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