feat(measure_theory): add @[to_additive] (#8142)

This PR adds `@[to_additive]` to `haar_measure` and everything that depends on. This will allow us to define the Lebesgue measure on `ℝ` and `ℝ ^ n` as the Haar measure (or just show that it is equal to it).



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

src/algebra/group/to_additive.lean

@@ -137,7 +137,7 @@ structure value_type : Type :=
 
 /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. -/
 meta def add_comm_prefix : bool → string → string
-| tt s := ("comm_" ++ s)
+| tt s := "comm_" ++ s
 | ff s := s
 
 /-- Dictionary used by `to_additive.guess_name` to autogenerate names. -/
@@ -163,6 +163,8 @@ meta def tr : bool → list string → list string
 | is_comm ("subgroup" :: s)    := ("add_" ++ add_comm_prefix is_comm "subgroup")  :: tr ff s
 | is_comm ("semigroup" :: s)   := ("add_" ++ add_comm_prefix is_comm "semigroup") :: tr ff s
 | is_comm ("magma" :: s)       := ("add_" ++ add_comm_prefix is_comm "magma")     :: tr ff s
+| is_comm ("haar" :: s)        := ("add_" ++ add_comm_prefix is_comm "haar")      :: tr ff s
+| is_comm ("prehaar" :: s)     := ("add_" ++ add_comm_prefix is_comm "prehaar")   :: tr ff s
 | is_comm ("comm" :: s)        := tr tt s
 | is_comm (x :: s)             := (add_comm_prefix is_comm x :: tr ff s)
 | tt []                        := ["comm"]

src/measure_theory/arithmetic.lean

@@ -25,18 +25,28 @@ because on some types (e.g., `ℕ`, `ℝ≥0∞`) division and/or subtraction ar
 For instances relating, e.g., `has_continuous_mul` to `has_measurable_mul` see file
 `measure_theory.borel_space`.
 
+## Implementation notes
+
+For the heuristics of `@[to_additive]` it is important that the type with a multiplication
+(or another multiplicative operations) is the first (implicit) argument of all declarations.
+
 ## Tags
 
 measurable function, arithmetic operator
+
+## Todo
+
+* Uniformize the treatment of `pow` and `smul`.
+* Use `@[to_additive]` to send `has_measurable_pow` to `has_measurable_smul₂`.
+* This might require changing the definition (swapping the arguments in the function that is
+  in the conclusion of `measurable_smul`.)
 -/
 
 universes u v
 
 open_locale big_operators
 open measure_theory
 
-variables {α : Type*} [measurable_space α]
-
 /-!
 ### Binary operations: `(+)`, `(*)`, `(-)`, `(/)`
 -/
@@ -73,7 +83,7 @@ export has_measurable_mul₂ (measurable_mul)
 
 section mul
 
-variables {M : Type*} [measurable_space M] [has_mul M]
+variables {M α : Type*} [measurable_space M] [has_mul M] [measurable_space α]
 
 @[to_additive, measurability]
 lemma measurable.const_mul [has_measurable_mul M] {f : α → M} (hf : measurable f) (c : M) :
@@ -148,8 +158,8 @@ end⟩
 
 section pow
 
-variables {β γ : Type*} [measurable_space β] [measurable_space γ] [has_pow β γ]
-  [has_measurable_pow β γ]
+variables {β γ α : Type*} [measurable_space β] [measurable_space γ] [has_pow β γ]
+  [has_measurable_pow β γ] [measurable_space α]
 
 @[measurability]
 lemma measurable.pow {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) :
@@ -213,7 +223,7 @@ export has_measurable_div₂ (measurable_div)
 
 section div
 
-variables {G : Type*} [measurable_space G] [has_div G]
+variables {G α : Type*} [measurable_space G] [has_div G] [measurable_space α]
 
 @[to_additive, measurability]
 lemma measurable.const_div [has_measurable_div G] {f : α → G} (hf : measurable f) (c : G) :
@@ -313,7 +323,7 @@ instance has_measurable_div_of_mul_inv (G : Type*) [measurable_space G]
 
 section inv
 
-variables {G : Type*} [has_inv G] [measurable_space G] [has_measurable_inv G]
+variables {G α : Type*} [has_inv G] [measurable_space G] [has_measurable_inv G] [measurable_space α]
 
 @[to_additive, measurability]
 lemma measurable.inv {f : α → G} (hf : measurable f) :
@@ -406,7 +416,8 @@ instance has_measurable_smul₂_of_mul (M : Type*) [monoid M] [measurable_space
 
 section smul
 
-variables {M β : Type*} [measurable_space M] [measurable_space β] [has_scalar M β]
+variables {M β α : Type*} [measurable_space M] [measurable_space β] [has_scalar M β]
+  [measurable_space α]
 
 @[measurability]
 lemma measurable.smul [has_measurable_smul₂ M β]
@@ -460,8 +471,8 @@ end smul
 
 section mul_action
 
-variables {M β : Type*} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β]
-  [has_measurable_smul M β] {f : α → β} {μ : measure α}
+variables {M β α : Type*} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β]
+  [has_measurable_smul M β] [measurable_space α] {f : α → β} {μ : measure α}
 
 variables {G : Type*} [group G] [measurable_space G] [mul_action G β]
   [has_measurable_smul G β]
@@ -506,9 +517,11 @@ end mul_action
 ### Big operators: `∏` and `∑`
 -/
 
+section monoid
+variables {M α : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M] [measurable_space α]
+
 @[to_additive, measurability]
-lemma list.measurable_prod' {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M]
-  (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) :
+lemma list.measurable_prod' (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) :
   measurable l.prod :=
 begin
   induction l with f l ihl, { exact measurable_one },
@@ -518,9 +531,8 @@ begin
 end
 
 @[to_additive, measurability]
-lemma list.ae_measurable_prod' {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M]
-  {μ : measure α} (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) :
-  ae_measurable l.prod μ :=
+lemma list.ae_measurable_prod' {μ : measure α} (l : list (α → M))
+  (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable l.prod μ :=
 begin
   induction l with f l ihl, { exact ae_measurable_one },
   rw [list.forall_mem_cons] at hl,
@@ -529,68 +541,66 @@ begin
 end
 
 @[to_additive, measurability]
-lemma list.measurable_prod {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M]
-  (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) :
+lemma list.measurable_prod (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) :
   measurable (λ x, (l.map (λ f : α → M, f x)).prod) :=
 by simpa only [← pi.list_prod_apply] using l.measurable_prod' hl
 
 @[to_additive, measurability]
-lemma list.ae_measurable_prod {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M]
-  {μ : measure α} (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) :
+lemma list.ae_measurable_prod {μ : measure α} (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) :
   ae_measurable (λ x, (l.map (λ f : α → M, f x)).prod) μ :=
 by simpa only [← pi.list_prod_apply] using l.ae_measurable_prod' hl
 
+end monoid
+
+section comm_monoid
+variables {M ι α : Type*} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M]
+  [measurable_space α]
+
 @[to_additive, measurability]
-lemma multiset.measurable_prod' {M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] (l : multiset (α → M)) (hl : ∀ f ∈ l, measurable f) :
+lemma multiset.measurable_prod' (l : multiset (α → M)) (hl : ∀ f ∈ l, measurable f) :
   measurable l.prod :=
 by { rcases l with ⟨l⟩, simpa using l.measurable_prod' (by simpa using hl) }
 
 @[to_additive, measurability]
-lemma multiset.ae_measurable_prod' {M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] {μ : measure α} (l : multiset (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) :
-  ae_measurable l.prod μ :=
+lemma multiset.ae_measurable_prod' {μ : measure α} (l : multiset (α → M))
+  (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable l.prod μ :=
 by { rcases l with ⟨l⟩, simpa using l.ae_measurable_prod' (by simpa using hl) }
 
 @[to_additive, measurability]
-lemma multiset.measurable_prod {M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] (s : multiset (α → M)) (hs : ∀ f ∈ s, measurable f) :
+lemma multiset.measurable_prod (s : multiset (α → M)) (hs : ∀ f ∈ s, measurable f) :
   measurable (λ x, (s.map (λ f : α → M, f x)).prod) :=
 by simpa only [← pi.multiset_prod_apply] using s.measurable_prod' hs
 
 @[to_additive, measurability]
-lemma multiset.ae_measurable_prod {M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] {μ : measure α} (s : multiset (α → M)) (hs : ∀ f ∈ s, ae_measurable f μ) :
-  ae_measurable (λ x, (s.map (λ f : α → M, f x)).prod) μ :=
+lemma multiset.ae_measurable_prod {μ : measure α} (s : multiset (α → M))
+  (hs : ∀ f ∈ s, ae_measurable f μ) : ae_measurable (λ x, (s.map (λ f : α → M, f x)).prod) μ :=
 by simpa only [← pi.multiset_prod_apply] using s.ae_measurable_prod' hs
 
 @[to_additive, measurability]
-lemma finset.measurable_prod' {ι M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) :
+lemma finset.measurable_prod' {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) :
   measurable (∏ i in s, f i) :=
 finset.prod_induction _ _ (λ _ _, measurable.mul) (@measurable_one M _ _ _ _) hf
 
 @[to_additive, measurability]
-lemma finset.measurable_prod {ι M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) :
+lemma finset.measurable_prod {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) :
   measurable (λ a, ∏ i in s, f i a) :=
 by simpa only [← finset.prod_apply] using s.measurable_prod' hf
 
 @[to_additive, measurability]
-lemma finset.ae_measurable_prod' {ι M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] {μ : measure α} {f : ι → α → M} (s : finset ι)
+lemma finset.ae_measurable_prod' {μ : measure α} {f : ι → α → M} (s : finset ι)
   (hf : ∀i ∈ s, ae_measurable (f i) μ) :
   ae_measurable (∏ i in s, f i) μ :=
 multiset.ae_measurable_prod' _ $
   λ g hg, let ⟨i, hi, hg⟩ := multiset.mem_map.1 hg in (hg ▸ hf _ hi)
 
 @[to_additive, measurability]
-lemma finset.ae_measurable_prod {ι M : Type*} [comm_monoid M] [measurable_space M]
-  [has_measurable_mul₂ M] {f : ι → α → M} {μ : measure α} (s : finset ι)
+lemma finset.ae_measurable_prod {f : ι → α → M} {μ : measure α} (s : finset ι)
   (hf : ∀i ∈ s, ae_measurable (f i) μ) :
   ae_measurable (λ a, ∏ i in s, f i a) μ :=
 by simpa only [← finset.prod_apply] using s.ae_measurable_prod' hf
 
+end comm_monoid
+
 attribute [measurability] list.measurable_sum' list.ae_measurable_sum' list.measurable_sum
   list.ae_measurable_sum multiset.measurable_sum' multiset.ae_measurable_sum'
   multiset.measurable_sum multiset.ae_measurable_sum finset.measurable_sum'

src/measure_theory/conditional_expectation.lean

@@ -43,14 +43,14 @@ lemma add [has_add β] [has_measurable_add₂ β] (hf : ae_measurable' m f μ)
 begin
   rcases hf with ⟨f', h_f'_meas, hff'⟩,
   rcases hg with ⟨g', h_g'_meas, hgg'⟩,
-  exact ⟨f' + g', @measurable.add α m _ _ _ _ f' g' h_f'_meas h_g'_meas, hff'.add hgg'⟩,
+  exact ⟨f' + g', @measurable.add _ _ _ _ m _ f' g' h_f'_meas h_g'_meas, hff'.add hgg'⟩,
 end
 
 lemma const_smul [has_scalar 𝕜 β] [has_measurable_smul 𝕜 β] (c : 𝕜) (hf : ae_measurable' m f μ) :
   ae_measurable' m (c • f) μ :=
 begin
   rcases hf with ⟨f', h_f'_meas, hff'⟩,
-  refine ⟨c • f', @measurable.const_smul α m _ _ _ _ _ _ f' h_f'_meas c, _⟩,
+  refine ⟨c • f', @measurable.const_smul _ _ _ _ _ _ m _ f' h_f'_meas c, _⟩,
   exact eventually_eq.fun_comp hff' (λ x, c • x),
 end
 
@@ -216,7 +216,7 @@ begin
   refine eventually_eq.trans _ (@Lp.coe_fn_add _ _ m _ _ _ _ _ _ _ _).symm,
   refine ae_eq_trim_of_measurable hm _ _ _,
   { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, },
-  { exact @measurable.add _ m _ _ _ _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _)
+  { exact @measurable.add _ _ _ _ m _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _)
       (@Lp.measurable _ _ m _ _ _ _ _ _ _), },
   refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _,
   refine eventually_eq.trans _
@@ -234,7 +234,7 @@ begin
   refine eventually_eq.trans _ (@Lp.coe_fn_smul _ _ m _ _ _ _ _ _ _ _ _ _ _ _ _).symm,
   refine ae_eq_trim_of_measurable hm _ _ _,
   { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, },
-  { exact @measurable.const_smul _ m _ _ _ _ _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) c, },
+  { exact @measurable.const_smul _ _ _ _ _ _ m _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) c, },
   refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _,
   refine (Lp.coe_fn_smul c _).trans _,
   refine (Lp_meas_to_Lp_trim_ae_eq hm f).mono (λ x hx, _),

src/measure_theory/content.lean

@@ -193,7 +193,7 @@ lemma is_mul_left_invariant_inner_content [group G] [topological_group G]
   (U : opens G) : μ.inner_content (U.comap $ continuous_mul_left g) = μ.inner_content U :=
 by convert μ.inner_content_comap (homeomorph.mul_left g) (λ K, h g) U
 
--- @[to_additive] (fails for now)
+@[to_additive]
 lemma inner_content_pos_of_is_mul_left_invariant [t2_space G] [group G] [topological_group G]
   (h3 : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K)
   (K : compacts G) (hK : 0 < μ K) (U : opens G) (hU : (U : set G).nonempty) :
@@ -299,15 +299,14 @@ begin
   apply inner_content_mono'
 end
 
--- @[to_additive] (fails for now)
+@[to_additive]
 lemma outer_measure_pos_of_is_mul_left_invariant [group G] [topological_group G]
   (h3 : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K)
   (K : compacts G) (hK : 0 < μ K) {U : set G} (h1U : is_open U) (h2U : U.nonempty) :
   0 < μ.outer_measure U :=
 by { convert μ.inner_content_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U,
      exact μ.outer_measure_opens ⟨U, h1U⟩ }
 
-
 variables [S : measurable_space G] [borel_space G]
 include S
 

src/measure_theory/group.lean

@@ -155,7 +155,7 @@ section group
 variables [group G] [topological_group G]
 
 /-! Properties of regular left invariant measures -/
-@[to_additive measure_theory.measure.is_add_left_invariant.null_iff_empty]
+@[to_additive]
 lemma is_mul_left_invariant.null_iff_empty [regular μ] (h2μ : is_mul_left_invariant μ)
   (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) : μ s = 0 ↔ s = ∅ :=
 begin
@@ -177,7 +177,7 @@ begin
     rwa [inv_mul_cancel_right] }
 end
 
-@[to_additive measure_theory.measure.is_add_left_invariant.null_iff]
+@[to_additive]
 lemma is_mul_left_invariant.null_iff [regular μ] (h2μ : is_mul_left_invariant μ)
   {s : set G} (hs : is_open s) : μ s = 0 ↔ s = ∅ ∨ μ = 0 :=
 begin
@@ -186,15 +186,15 @@ begin
   exact h2μ.null_iff_empty h3μ hs,
 end
 
-@[to_additive measure_theory.measure.is_add_left_invariant.measure_ne_zero_iff_nonempty]
+@[to_additive]
 lemma is_mul_left_invariant.measure_ne_zero_iff_nonempty [regular μ]
   (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
   μ s ≠ 0 ↔ s.nonempty :=
 by simp_rw [← ne_empty_iff_nonempty, ne.def, h2μ.null_iff_empty h3μ hs]
 
 /-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
   `f` is 0 iff `f` is 0. -/
--- @[to_additive] (fails for now)
+@[to_additive]
 lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ]
   (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {f : G → ℝ≥0∞} (hf : continuous f) :
   ∫⁻ x, f x ∂μ = 0 ↔ f = 0 :=