Restriction of Measure to a Subset

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Given a measure μ defined on some measurable space α and a subset s of α. I want to obtain a measure on the subtype s by naturally restricting μ. However, μ.restrict s has type Measure α instead of Measure (Subtype s). Is there a reason for this design?

I am also aware of MeasureTheory.Measure.Subtype.measureSpace. However, in order to use this definition, I need the instance [MeasureSpace α], i.e. a canonical measure defined on α. What should I do if I want to restrict instead a non-canonical measure?

[Kenny Lau]

subtypes are generally hard to use, restrict instead makes it supported on the subset given

[Yury G. Kudryashov]

If s is a measurable subset, then you can use (μ.comap Subtype.val : Measure s)

[Kevin Buzzard]

Yongxi Lin said:

Is there a reason for this design?

Subsets are terms, not types. Sometimes terms are easier to deal with. For example if you're going to measure subsets X of s which are actually subsets of α, then if you use μ.restrict s you can just intersect X and s (or just measure X with the restricted measure). but if you use the subtype ↑s you'll have to pull X back to ↑s and explicitly work with the inclusion ↑s -> α and it will generally be messier.

[Yury G. Kudryashov]

E.g., you can't restrict a measure to s, then restrict the result to t if you use subtypes. More precisely, you'll have to restrict the result to the preimage of t under the inclusion of s to the ambient type. And saying something like "restrictions commute" is hard, because the two restrictions are measures on different types.

[Yongxi Lin (Aaron)]

Thank you for all your reply. I think (μ.comap Subtype.val : Measure s) is what I want.

[David Ledvinka]

Also even ignoring the formalization subtleties (which are important) both notions are relevant in paper math. Sometimes one does not want to forget the ambient space, for example if you want to decompose a measure into a sum of restrictions.