Subtype of a measure space

Stream: maths

[Yaël Dillies]

Is this true? Context is #2819

import measure_theory.measure.measure_space_def

variables {V : Type*} [measure_space V] {p : V → Prop} {s : set V}

instance subtype.measure_space : measure_space (subtype p) :=
{ volume := measure.comap subtype.val volume,
  ..subtype.measurable_space }

lemma subtype.volume_univ (hs : null_measurable_set s) : volume (univ : set s) = volume s := sorry

[Yaël Dillies]

Note that

lemma subtype.volume_univ' (hs : measurable_set s) : volume (univ : set s) = volume s := sorry

is indeed true.

[Jason KY.]

This is not true. If s is not measurable then the volume is just 0 (while you can certainly have a nonmeasurable set of measure > 0).

lemma subtype.volume_univ (hs : ¬ measurable_set s) : volume (univ : set s) = 0 :=
begin
  change measure.comap subtype.val volume _ = 0,
  rw [measure.comap, dif_neg],
  { refl },
  { rw [not_and_distrib, not_forall],
    refine or.inr ⟨univ, not_imp.2 ⟨measurable_set.univ, _⟩⟩,
    simp [hs] },
end

[Yaël Dillies]

Hmm, this is annoying because that means #2819 can't use docs#measure_theory.is_fundamental_domain.

[Sebastien Gouezel]

This probably means that we should fix the definition of measure.comap, in the same way that we fixed measure.map to allow for almost everywhere measurable functions.

[Yaël Dillies]

Would anyone do that for me? :smiley: I am very unaware of the measure theory library.

[Sebastien Gouezel]

Sorry, no available free time currently for me (in addition to the heavy duties of old people that have been mentioned in the previous thread, you should add that kids take a significant amount of time in July and August :-)

[Rémy Degenne]

I will have a look tomorrow. But if I don't manage to do it in the next two days then I also won't have time before a week or two.

[Rémy Degenne]

@Yaël Dillies see branch#RD_comap . PR coming soon.

[Rémy Degenne]

#15343

[Yaël Dillies]

Still on this, is this now true?

import measure_theory.measure.measure_space_def

variables {V : Type*} [measure_space V] {p : V → Prop} {s : set V}

instance subtype.measure_space : measure_space (subtype p) :=
{ volume := measure.comap subtype.val volume,
  ..subtype.measurable_space }

lemma null_measurable_set.subtype_image {t : set s} (hs : null_measurable_set s) :
  null_measurable_set t → null_measurable_set ((coe : s → V) '' t) := sorry

[Rémy Degenne]

Yes this is true. I just pushed a (rather horrible) proof to branch#RD_comap

[Alex J. Best]

@Rémy Degenne Did you PR your proof of subtype.volume_univ somewhere? It would be great to have this :smile:

[Rémy Degenne]

No I didn't. I was not clear at the time but when I wrote that I pushed stuff to a branch I meant "feel free to take from that branch anything you could need and PR it". I'll try to clean and PR that code next week-end

[Alex J. Best]

Ok I did a little golfing, I'd still like to simplify the long proofs a bit (involving lemma todo for instance).