Zulip Chat Archive

Stream: maths

Topic: transporting measurability proofs


view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Jul 03 2019 at 14:57):

measurable_id?

view this post on Zulip 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

view this post on Zulip 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..

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:01):

well, MWE then

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:06):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:27):

did you try exact measurable_id?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:27):

apply measurable_id probably won't work because of the apply bug

view this post on Zulip Patrick Massot (Jul 03 2019 at 15:27):

Where is that "apply bug" emoticon again?

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:28):

pp.all?

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:29):

well why didn't you say so

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:29):

it's not the same measure

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:29):

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

view this post on Zulip Koundinya Vajjha (Jul 03 2019 at 15:30):

what's not the same measure?

view this post on Zulip 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

view this post on Zulip Koundinya Vajjha (Jul 03 2019 at 15:31):

I didn't update mathlib in a while

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 03 2019 at 15:32):

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

view this post on Zulip Koundinya Vajjha (Jul 03 2019 at 15:34):

yes, which is why i thought I should use ennreal_equiv_nnreal and transport it somehow...

view this post on Zulip 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

view this post on Zulip 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