transporting measurability proofs

Stream: maths

[Koundinya Vajjha]

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]

measurable_id?

[Mario Carneiro]

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]

Riight. I have a lot of implicit arguments and measurable_id doesn't work in the proof..

[Mario Carneiro]

well, MWE then

[Mario Carneiro]

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

[Koundinya Vajjha]

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

[Mario Carneiro]

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

[Koundinya Vajjha]

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]

did you try exact measurable_id?

[Mario Carneiro]

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

[Patrick Massot]

Where is that "apply bug" emoticon again?

[Koundinya Vajjha]

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]

pp.all?

[Mario Carneiro]

well why didn't you say so

[Mario Carneiro]

it's not the same measure

[Mario Carneiro]

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

[Koundinya Vajjha]

what's not the same measure?

[Mario Carneiro]

didn't measurable.comp recently get its arguments flipped? I'm not sure if you or I are out of date

[Koundinya Vajjha]

I didn't update mathlib in a while

[Mario Carneiro]

nnreal is defined to be {r : ℝ // 0 ≤ r}, so it has a measurable space from subtype applied to the measure on real

[Mario Carneiro]

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

[Koundinya Vajjha]

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

[Mario Carneiro]

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]

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