Notation for {Finite,Probability}Measure[mα]

Stream: mathlib4

[Lua Viana Reis]

Given that there is the notation Measure[mα] for specifying the algebra, would it make sense to include analogue notation for FiniteMeasure and ProbabilityMeasure?

[Lua Viana Reis]

(deleted)

[Yaël Dillies]

I see no reason why not! We add such notation as it becomes necessary in applications. If you have such an application, then we will add the notation

[Rémy Degenne]

Yes, it would make sense to have that notation.
I feel obligated to ask if using ProbabilityMeasure is the right choice for what you want to do: you should always prefer Measure together with IsProbabilityMeasure unless you are using the topology on ProbabilityMeasure.

[Lua Viana Reis]

Rémy Degenne said:

Yes, it would make sense to have that notation.
I feel obligated to ask if using ProbabilityMeasure is the right choice for what you want to do: you should always prefer Measure together with IsProbabilityMeasure unless you are using the topology on ProbabilityMeasure.

I agree with using Measure, I think I figured that out yesterday, after creating this topic. I was using them initially because they are NNReal-valued

[Floris van Doorn]

If m is a measure, then m.real s gives the measure of s as a real number.

[Lua Viana Reis]

This is very nitpicky, but any reason why FiniteMeasure.map does not reuse Measure.isFiniteMeasure_map?

I should not have assumed that, but when I saw it, it made me think that the IsFiniteMeasure instance for .map did not exist and I should use the subtype (my deleted message from yesterday :see_no_evil:)

It could be

/-- The push-forward of a finite measure by a function between measurable spaces. -/
noncomputable def map (ν : FiniteMeasure Ω) (f : Ω → Ω') : FiniteMeasure Ω' :=
  ⟨(ν : Measure Ω).map f, (ν : Measure Ω).isFiniteMeasure_map f⟩

[Floris van Doorn]

Nope, your def is nicer. Feel free to PR a fix!

[Lua Viana Reis]

same for ProbabilityMeasure

[Lua Viana Reis]

#31091