chore: Add pp_dot to measure definitions trim, withDensity, `rest…

…rict`, `rnDeriv` and `singularPart` (#11871)

We use dot notation for them everywhere in the code. Let's use it in the infoview as well.

Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

@@ -71,13 +71,15 @@ class HaveLebesgueDecomposition (μ ν : Measure α) : Prop where
 /-- If a pair of measures `HaveLebesgueDecomposition`, then `singularPart` chooses the
 measure from `HaveLebesgueDecomposition`, otherwise it returns the zero measure. For sigma-finite
 measures, `μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)`. -/
+@[pp_dot]
 irreducible_def singularPart (μ ν : Measure α) : Measure α :=
   if h : HaveLebesgueDecomposition μ ν then (Classical.choose h.lebesgue_decomposition).1 else 0
 #align measure_theory.measure.singular_part MeasureTheory.Measure.singularPart
 
 /-- If a pair of measures `HaveLebesgueDecomposition`, then `rnDeriv` chooses the
 measurable function from `HaveLebesgueDecomposition`, otherwise it returns the zero function.
 For sigma-finite measures, `μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)`.-/
+@[pp_dot]
 irreducible_def rnDeriv (μ ν : Measure α) : α → ℝ≥0∞ :=
   if h : HaveLebesgueDecomposition μ ν then (Classical.choose h.lebesgue_decomposition).2 else 0
 #align measure_theory.measure.rn_deriv MeasureTheory.Measure.rnDeriv

Mathlib/MeasureTheory/Measure/Restrict.lean

@@ -41,6 +41,7 @@ noncomputable def restrictₗ {m0 : MeasurableSpace α} (s : Set α) : Measure 
 #align measure_theory.measure.restrictₗ MeasureTheory.Measure.restrictₗ
 
 /-- Restrict a measure `μ` to a set `s`. -/
+@[pp_dot]
 noncomputable def restrict {_m0 : MeasurableSpace α} (μ : Measure α) (s : Set α) : Measure α :=
   restrictₗ s μ
 #align measure_theory.measure.restrict MeasureTheory.Measure.restrict

Mathlib/MeasureTheory/Measure/Trim.lean

@@ -28,6 +28,7 @@ cannot be a measure on `m`, hence the definition of `μ.trim hm`.
 
 This notion is related to `OuterMeasure.trim`, see the lemma
 `toOuterMeasure_trim_eq_trim_toOuterMeasure`. -/
+@[pp_dot]
 noncomputable
 def Measure.trim {m m0 : MeasurableSpace α} (μ : @Measure α m0) (hm : m ≤ m0) : @Measure α m :=
   @OuterMeasure.toMeasure α m μ.toOuterMeasure (hm.trans (le_toOuterMeasure_caratheodory μ))

Mathlib/MeasureTheory/Measure/WithDensity.lean

@@ -29,6 +29,7 @@ variable {α : Type*} {m0 : MeasurableSpace α} {μ : Measure α}
 
 /-- Given a measure `μ : Measure α` and a function `f : α → ℝ≥0∞`, `μ.withDensity f` is the
 measure such that for a measurable set `s` we have `μ.withDensity f s = ∫⁻ a in s, f a ∂μ`. -/
+@[pp_dot]
 noncomputable
 def Measure.withDensity {m : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) : Measure α :=
   Measure.ofMeasurable (fun s _ => ∫⁻ a in s, f a ∂μ) (by simp) fun s hs hd =>