doc(measure_theory): add some missing to_additive docstrings (#13456)

src/measure_theory/constructions/pi.lean

@@ -553,7 +553,9 @@ measure.pi_closed_ball _ _ hr
 open measure
 /-- We intentionally restrict this only to the nondependent function space, since type-class
 inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces. -/
-@[to_additive]
+@[to_additive "We intentionally restrict this only to the nondependent function space, since
+type-class inference cannot find an instance for `ι → ℝ` when this is stated for dependent function
+spaces."]
 instance pi.is_mul_left_invariant_volume {α} [group α] [measure_space α]
   [sigma_finite (volume : measure α)]
   [has_measurable_mul α] [is_mul_left_invariant (volume : measure α)] :
@@ -562,7 +564,9 @@ pi.is_mul_left_invariant _
 
 /-- We intentionally restrict this only to the nondependent function space, since type-class
 inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces. -/
-@[to_additive]
+@[to_additive "We intentionally restrict this only to the nondependent function space, since
+type-class inference cannot find an instance for `ι → ℝ` when this is stated for dependent function
+spaces."]
 instance pi.is_inv_invariant_volume {α} [group α] [measure_space α]
   [sigma_finite (volume : measure α)]
   [has_measurable_inv α] [is_inv_invariant (volume : measure α)] :

src/measure_theory/group/integration.lean

@@ -46,19 +46,21 @@ section measurable_mul
 
 variables [group G] [has_measurable_mul G]
 
-/-- Translating a function by left-multiplication does not change its `lintegral` with respect to
-a left-invariant measure. -/
-@[to_additive]
+/-- Translating a function by left-multiplication does not change its `measure_theory.lintegral`
+with respect to a left-invariant measure. -/
+@[to_additive "Translating a function by left-addition does not change its
+`measure_theory.lintegral` with respect to a left-invariant measure."]
 lemma lintegral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → ℝ≥0∞) (g : G) :
   ∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ :=
 begin
   convert (lintegral_map_equiv f $ measurable_equiv.mul_left g).symm,
   simp [map_mul_left_eq_self μ g]
 end
 
-/-- Translating a function by right-multiplication does not change its `lintegral` with respect to
-a right-invariant measure. -/
-@[to_additive]
+/-- Translating a function by right-multiplication does not change its `measure_theory.lintegral`
+with respect to a right-invariant measure. -/
+@[to_additive "Translating a function by right-addition does not change its
+`measure_theory.lintegral` with respect to a right-invariant measure."]
 lemma lintegral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) :
   ∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ :=
 begin
@@ -68,7 +70,8 @@ end
 
 /-- Translating a function by left-multiplication does not change its integral with respect to a
 left-invariant measure. -/
-@[to_additive]
+@[to_additive "Translating a function by left-addition does not change its integral with respect to
+a left-invariant measure."]
 lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) :
   ∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ :=
 begin
@@ -79,7 +82,8 @@ end
 
 /-- Translating a function by right-multiplication does not change its integral with respect to a
 right-invariant measure. -/
-@[to_additive]
+@[to_additive "Translating a function by right-addition does not change its integral with respect to
+a right-invariant measure."]
 lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) :
   ∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ :=
 begin
@@ -90,14 +94,16 @@ end
 
 /-- If some left-translate of a function negates it, then the integral of the function with respect
 to a left-invariant measure is 0. -/
-@[to_additive]
+@[to_additive "If some left-translate of a function negates it, then the integral of the function
+with respect to a left-invariant measure is 0."]
 lemma integral_eq_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] (hf' : ∀ x, f (g * x) = - f x) :
   ∫ x, f x ∂μ = 0 :=
 by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]
 
 /-- If some right-translate of a function negates it, then the integral of the function with respect
 to a right-invariant measure is 0. -/
-@[to_additive]
+@[to_additive "If some right-translate of a function negates it, then the integral of the function
+with respect to a right-invariant measure is 0."]
 lemma integral_eq_zero_of_mul_right_eq_neg [is_mul_right_invariant μ]
   (hf' : ∀ x, f (x * g) = - f x) : ∫ x, f x ∂μ = 0 :=
 by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]
@@ -149,7 +155,8 @@ variables [topological_space G] [group G] [topological_group G] [borel_space G]
 
 /-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
   `f` is 0 iff `f` is 0. -/
-@[to_additive]
+@[to_additive "For nonzero regular left invariant measures, the integral of a continuous nonnegative
+function `f` is 0 iff `f` is 0."]
 lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0)
   {f : G → ℝ≥0∞} (hf : continuous f) :
   ∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=

src/measure_theory/group/measure.lean

@@ -67,7 +67,7 @@ lemma map_mul_right_eq_self (μ : measure G) [is_mul_right_invariant μ] (g : G)
 is_mul_right_invariant.map_mul_right_eq_self g
 
 /-- An alternative way to prove that `μ` is left invariant under multiplication. -/
-@[to_additive]
+@[to_additive "An alternative way to prove that `μ` is left invariant under addition."]
 lemma forall_measure_preimage_mul_iff [has_measurable_mul G] (μ : measure G) :
   (∀ (g : G) (A : set G), measurable_set A → μ ((λ h, g * h) ⁻¹' A) = μ A) ↔
   is_mul_left_invariant μ :=
@@ -80,7 +80,7 @@ begin
 end
 
 /-- An alternative way to prove that `μ` is left invariant under multiplication. -/
-@[to_additive]
+@[to_additive "An alternative way to prove that `μ` is left invariant under addition."]
 lemma forall_measure_preimage_mul_right_iff [has_measurable_mul G] (μ : measure G) :
   (∀ (g : G) (A : set G), measurable_set A → μ ((λ h, h * g) ⁻¹' A) = μ A) ↔
   is_mul_right_invariant μ :=
@@ -116,7 +116,8 @@ variables [has_measurable_mul G]
 
 /-- We shorten this from `measure_preimage_mul_left`, since left invariant is the preferred option
   for measures in this formalization. -/
-@[simp, to_additive]
+@[simp, to_additive "We shorten this from `measure_preimage_add_left`, since left invariant is the
+preferred option for measures in this formalization."]
 lemma measure_preimage_mul (μ : measure G) [is_mul_left_invariant μ] (g : G) (A : set G) :
   μ ((λ h, g * h) ⁻¹' A) = μ A :=
 calc μ ((λ h, g * h) ⁻¹' A) = map (λ h, g * h) μ A :
@@ -252,9 +253,11 @@ begin
 end
 
 variables [is_mul_left_invariant μ]
-/-- If a left-invariant measure gives positive mass to a compact set, then
-it gives positive mass to any open set. -/
-@[to_additive]
+
+/-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to
+any open set. -/
+@[to_additive "If a left-invariant measure gives positive mass to a compact set, then it gives
+positive mass to any open set."]
 lemma is_open_pos_measure_of_mul_left_invariant_of_compact
   (K : set G) (hK : is_compact K) (h : μ K ≠ 0) :
   is_open_pos_measure μ :=
@@ -271,7 +274,7 @@ begin
 end
 
 /-- A nonzero left-invariant regular measure gives positive mass to any open set. -/
-@[to_additive]
+@[to_additive "A nonzero left-invariant regular measure gives positive mass to any open set."]
 lemma is_open_pos_measure_of_mul_left_invariant_of_regular [regular μ] (h₀ : μ ≠ 0) :
   is_open_pos_measure μ :=
 let ⟨K, hK, h2K⟩ := regular.exists_compact_not_null.mpr h₀
@@ -299,9 +302,10 @@ lemma measure_pos_iff_nonempty_of_is_mul_left_invariant [regular μ]
   0 < μ s ↔ s.nonempty :=
 pos_iff_ne_zero.trans $ measure_ne_zero_iff_nonempty_of_is_mul_left_invariant h3μ hs
 
-/-- If a left-invariant measure gives finite mass to a nonempty open set, then
-it gives finite mass to any compact set. -/
-@[to_additive]
+/-- If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass
+to any compact set. -/
+@[to_additive "If a left-invariant measure gives finite mass to a nonempty open set, then it gives
+finite mass to any compact set."]
 lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant
   (U : set G) (hU : is_open U) (h'U : U.nonempty) (h : μ U ≠ ∞) {K : set G} (hK : is_compact K) :
   μ K < ∞ :=
@@ -317,7 +321,8 @@ end
 
 /-- If a left-invariant measure gives finite mass to a set with nonempty interior, then
 it gives finite mass to any compact set. -/
-@[to_additive]
+@[to_additive "If a left-invariant measure gives finite mass to a set with nonempty interior, then
+it gives finite mass to any compact set."]
 lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant'
   {U : set G} (hU : (interior U).nonempty) (h : μ U ≠ ∞) {K : set G} (hK : is_compact K) :
   μ K < ∞ :=
@@ -333,7 +338,9 @@ variables [comm_group G]
 /-- In an abelian group every left invariant measure is also right-invariant.
   We don't declare the converse as an instance, since that would loop type-class inference, and
   we use `is_mul_left_invariant` as default hypotheses in abelian groups. -/
-@[priority 100, to_additive]
+@[priority 100, to_additive "In an abelian additive group every left invariant measure is also
+right-invariant. We don't declare the converse as an instance, since that would loop type-class
+inference, and we use `is_add_left_invariant` as default hypotheses in abelian groups."]
 instance is_mul_left_invariant.is_mul_right_invariant {μ : measure G} [is_mul_left_invariant μ] :
   is_mul_right_invariant μ :=
 ⟨λ g, by simp_rw [mul_comm, map_mul_left_eq_self]⟩
@@ -358,10 +365,17 @@ class is_haar_measure {G : Type*} [group G] [topological_space G] [measurable_sp
   (μ : measure G)
   extends is_finite_measure_on_compacts μ, is_mul_left_invariant μ, is_open_pos_measure μ : Prop
 
-/- Record that a Haar measure on a locally compact space is locally finite. This is needed as the
+/-- Record that a Haar measure on a locally compact space is locally finite. This is needed as the
 fact that a measure which is finite on compacts is locally finite is not registered as an instance,
-to avoid an instance loop. -/
-@[priority 100, to_additive] -- see Note [lower instance priority]
+to avoid an instance loop.
+
+See Note [lower instance priority]. -/
+
+@[priority 100, to_additive "Record that an additive Haar measure on a locally compact space is
+locally finite. This is needed as the fact that a measure which is finite on compacts is locally
+finite is not registered as an instance, to avoid an instance loop.
+
+See Note [lower instance priority]"]
 instance is_locally_finite_measure_of_is_haar_measure {G : Type*}
   [group G] [measurable_space G] [topological_space G] [locally_compact_space G]
   (μ : measure G) [is_haar_measure μ] :
@@ -387,8 +401,9 @@ lemma is_haar_measure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞)
   to_is_open_pos_measure := is_open_pos_measure_smul μ cpos }
 
 /-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
-it is a Haar measure -/
-@[to_additive]
+it is a Haar measure. -/
+@[to_additive "If a left-invariant measure gives positive mass to some compact set with nonempty
+interior, then it is an additive Haar measure."]
 lemma is_haar_measure_of_is_compact_nonempty_interior [topological_group G] [borel_space G]
   (μ : measure G) [is_mul_left_invariant μ]
   (K : set G) (hK : is_compact K) (h'K : (interior K).nonempty) (h : μ K ≠ 0) (h' : μ K ≠ ∞) :
@@ -399,7 +414,8 @@ lemma is_haar_measure_of_is_compact_nonempty_interior [topological_group G] [bor
 
 /-- The image of a Haar measure under a group homomorphism which is also a homeomorphism is again
 a Haar measure. -/
-@[to_additive]
+@[to_additive "The image of an additive Haar measure under an additive group homomorphism which is
+also a homeomorphism is again an additive Haar measure."]
 lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [group H]
   [topological_space H] [measurable_space H] [borel_space H] [t2_space H] [topological_group H]
   (f : G ≃* H) (hf : continuous f) (hfsymm : continuous f.symm) :
@@ -423,8 +439,12 @@ lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [gro
   end,
   to_is_open_pos_measure := hf.is_open_pos_measure_map f.surjective }
 
-/-- A Haar measure on a sigma-compact space is sigma-finite. -/
-@[priority 100, to_additive] -- see Note [lower instance priority]
+/-- A Haar measure on a σ-compact space is σ-finite.
+
+See Note [lower instance priority] -/
+@[priority 100, to_additive "A Haar measure on a σ-compact space is σ-finite.
+
+See Note [lower instance priority]"]
 instance is_haar_measure.sigma_finite [sigma_compact_space G] : sigma_finite μ :=
 ⟨⟨{ set := compact_covering G,
   set_mem := λ n, mem_univ _,
@@ -435,11 +455,15 @@ open_locale topological_space
 open filter
 
 /-- If the neutral element of a group is not isolated, then a Haar measure on this group has
-no atom.
+no atoms.
 
-This applies in particular to show that an additive Haar measure on a nontrivial
-finite-dimensional real vector space has no atom. -/
-@[priority 100, to_additive]
+The additive version of this instance applies in particular to show that an additive Haar measure on
+a nontrivial finite-dimensional real vector space has no atom. -/
+@[priority 100, to_additive "If the zero element of an additive group is not isolated, then an
+additive Haar measure on this group has no atoms.
+
+This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional
+real vector space has no atom."]
 instance is_haar_measure.has_no_atoms [topological_group G] [borel_space G]
   [t1_space G] [locally_compact_space G] [(𝓝[≠] (1 : G)).ne_bot]
   (μ : measure G) [μ.is_haar_measure] :