chore(measure_theory/group/arithmetic): use implicit argument for mea…

…surable_space (#11205)

The `measurable_space` argument is inferred from other arguments (like `measurable f` or a measure for example) instead of being a type class. This ensures that the lemmas are usable without `@` when several measurable space structures are used for the same type.

Also use more `variables`.

src/measure_theory/function/conditional_expectation.lean

@@ -85,7 +85,7 @@ function. This is similar to `ae_measurable`, but the `measurable_space` structu
 measurability statement and for the measure are different. -/
 def ae_measurable' {α β} [measurable_space β] (m : measurable_space α) {m0 : measurable_space α}
   (f : α → β) (μ : measure α) : Prop :=
-∃ g : α → β, @measurable α β m _ g ∧ f =ᵐ[μ] g
+∃ g : α → β, measurable[m] g ∧ f =ᵐ[μ] g
 
 namespace ae_measurable'
 
@@ -101,14 +101,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', h_f'_meas.add h_g'_meas, hff'.add hgg'⟩,
 end
 
 lemma neg [has_neg β] [has_measurable_neg β] {f : α → β} (hfm : ae_measurable' m f μ) :
   ae_measurable' m (-f) μ :=
 begin
   rcases hfm with ⟨f', hf'_meas, hf_ae⟩,
-  refine ⟨-f', @measurable.neg _ _ _ _ _ m _ hf'_meas, hf_ae.mono (λ x hx, _)⟩,
+  refine ⟨-f', hf'_meas.neg, hf_ae.mono (λ x hx, _)⟩,
   simp_rw pi.neg_apply,
   rw hx,
 end
@@ -119,8 +119,7 @@ lemma sub [has_sub β] [has_measurable_sub₂ β] {f g : α → β}
 begin
   rcases hfm with ⟨f', hf'_meas, hf_ae⟩,
   rcases hgm with ⟨g', hg'_meas, hg_ae⟩,
-  refine ⟨f'-g', @measurable.sub _ _ _ _ m _ _ _ hf'_meas hg'_meas,
-    hf_ae.mp (hg_ae.mono (λ x hx1 hx2, _))⟩,
+  refine ⟨f'-g', hf'_meas.sub hg'_meas, hf_ae.mp (hg_ae.mono (λ x hx1 hx2, _))⟩,
   simp_rw pi.sub_apply,
   rw [hx1, hx2],
 end
@@ -129,7 +128,7 @@ lemma const_smul [has_scalar 𝕜 β] [has_measurable_smul 𝕜 β] (c : 𝕜) (
   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', h_f'_meas.const_smul c, _⟩,
   exact eventually_eq.fun_comp hff' (λ x, c • x),
 end
 
@@ -139,8 +138,7 @@ lemma const_inner {𝕜} [is_R_or_C 𝕜] [inner_product_space 𝕜 β]
   ae_measurable' m (λ x, (inner c (f x) : 𝕜)) μ :=
 begin
   rcases hfm with ⟨f', hf'_meas, hf_ae⟩,
-  refine ⟨λ x, (inner c (f' x) : 𝕜),
-    @measurable.inner _ _ _ _ _ m _ _ _ _ _ (@measurable_const _ _ _ m _) hf'_meas,
+  refine ⟨λ x, (inner c (f' x) : 𝕜), (@measurable_const _ _ _ m _).inner hf'_meas,
     hf_ae.mono (λ x hx, _)⟩,
   dsimp only,
   rw hx,
@@ -378,7 +376,7 @@ begin
   ext1,
   refine eventually_eq.trans _ (Lp.coe_fn_add _ _).symm,
   refine ae_eq_trim_of_measurable hm (Lp.measurable _) _ _,
-  { exact @measurable.add _ _ _ _ m _ _ _ (Lp.measurable _) (Lp.measurable _), },
+  { exact (Lp.measurable _).add (Lp.measurable _), },
   refine (Lp_meas_subgroup_to_Lp_trim_ae_eq hm _).trans _,
   refine eventually_eq.trans _
     (eventually_eq.add (Lp_meas_subgroup_to_Lp_trim_ae_eq hm f).symm
@@ -416,7 +414,7 @@ begin
   ext1,
   refine eventually_eq.trans _ (Lp.coe_fn_smul _ _).symm,
   refine ae_eq_trim_of_measurable hm (Lp.measurable _) _ _,
-  { exact @measurable.const_smul _ _ α _ _ _ m _ _ (Lp.measurable _) c, },
+  { exact (Lp.measurable _).const_smul c, },
   refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _,
   refine (Lp.coe_fn_smul _ _).trans _,
   refine (Lp_meas_to_Lp_trim_ae_eq hm f).mono (λ x hx, _),
@@ -965,7 +963,7 @@ end
 variables {𝕜}
 
 lemma set_lintegral_nnnorm_condexp_L2_indicator_le (hm : m ≤ m0) (hs : measurable_set s)
-  (hμs : μ s ≠ ∞) (x : E') {t : set α} (ht : @measurable_set _ m t) (hμt : μ t ≠ ∞) :
+  (hμs : μ s ≠ ∞) (x : E') {t : set α} (ht : measurable_set[m] t) (hμt : μ t ≠ ∞) :
   ∫⁻ a in t, ∥condexp_L2 𝕜 hm (indicator_const_Lp 2 hs hμs x) a∥₊ ∂μ ≤ μ (s ∩ t) * ∥x∥₊ :=
 calc ∫⁻ a in t, ∥condexp_L2 𝕜 hm (indicator_const_Lp 2 hs hμs x) a∥₊ ∂μ
     = ∫⁻ a in t, ∥(condexp_L2 ℝ hm (indicator_const_Lp 2 hs hμs (1 : ℝ)) a) • x∥₊ ∂μ :
@@ -1052,7 +1050,7 @@ lemma condexp_ind_smul_ae_eq_smul (hm : m ≤ m0) (hs : measurable_set s) (hμs
 (to_span_singleton ℝ x).coe_fn_comp_LpL _
 
 lemma set_lintegral_nnnorm_condexp_ind_smul_le (hm : m ≤ m0) (hs : measurable_set s)
-  (hμs : μ s ≠ ∞) (x : G) {t : set α} (ht : @measurable_set _ m t) (hμt : μ t ≠ ∞) :
+  (hμs : μ s ≠ ∞) (x : G) {t : set α} (ht : measurable_set[m] t) (hμt : μ t ≠ ∞) :
   ∫⁻ a in t, ∥condexp_ind_smul hm hs hμs x a∥₊ ∂μ ≤ μ (s ∩ t) * ∥x∥₊ :=
 calc ∫⁻ a in t, ∥condexp_ind_smul hm hs hμs x a∥₊ ∂μ
     = ∫⁻ a in t, ∥condexp_L2 ℝ hm (indicator_const_Lp 2 hs hμs (1 : ℝ)) a • x∥₊ ∂μ :

src/measure_theory/function/special_functions.lean

@@ -89,7 +89,7 @@ end is_R_or_C
 
 section real_composition
 open real
-variables {α : Type*} [measurable_space α] {f : α → ℝ} (hf : measurable f)
+variables {α : Type*} {m : measurable_space α} {f : α → ℝ} (hf : measurable f)
 
 @[measurability] lemma measurable.exp : measurable (λ x, real.exp (f x)) :=
 real.measurable_exp.comp hf
@@ -119,7 +119,7 @@ end real_composition
 
 section complex_composition
 open complex
-variables {α : Type*} [measurable_space α] {f : α → ℂ} (hf : measurable f)
+variables {α : Type*} {m : measurable_space α} {f : α → ℂ} (hf : measurable f)
 
 @[measurability] lemma measurable.cexp : measurable (λ x, complex.exp (f x)) :=
 complex.measurable_exp.comp hf
@@ -146,9 +146,11 @@ end complex_composition
 
 section is_R_or_C_composition
 
-variables {α 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α]
+variables {α 𝕜 : Type*} [is_R_or_C 𝕜] {m : measurable_space α}
   {f : α → 𝕜} {μ : measure_theory.measure α}
 
+include m
+
 @[measurability] lemma measurable.re (hf : measurable f) : measurable (λ x, is_R_or_C.re (f x)) :=
 is_R_or_C.measurable_re.comp hf
 
@@ -163,6 +165,8 @@ is_R_or_C.measurable_im.comp hf
   ae_measurable (λ x, is_R_or_C.im (f x)) μ :=
 is_R_or_C.measurable_im.comp_ae_measurable hf
 
+omit m
+
 end is_R_or_C_composition
 
 section
@@ -231,14 +235,14 @@ variables {α : Type*} {𝕜 : Type*} {E : Type*} [is_R_or_C 𝕜] [inner_produc
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
 @[measurability]
-lemma measurable.inner [measurable_space α] [measurable_space E] [opens_measurable_space E]
+lemma measurable.inner {m : measurable_space α} [measurable_space E] [opens_measurable_space E]
   [topological_space.second_countable_topology E]
   {f g : α → E} (hf : measurable f) (hg : measurable g) :
   measurable (λ t, ⟪f t, g t⟫) :=
 continuous.measurable2 continuous_inner hf hg
 
 @[measurability]
-lemma ae_measurable.inner [measurable_space α] [measurable_space E] [opens_measurable_space E]
+lemma ae_measurable.inner {m : measurable_space α} [measurable_space E] [opens_measurable_space E]
   [topological_space.second_countable_topology E]
   {μ : measure_theory.measure α} {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
   ae_measurable (λ x, ⟪f x, g x⟫) μ :=
@@ -247,8 +251,7 @@ begin
   refine hf.ae_eq_mk.mp (hg.ae_eq_mk.mono (λ x hxg hxf, _)),
   dsimp only,
   congr,
-  { exact hxf, },
-  { exact hxg, },
+  exacts [hxf, hxg],
 end
 
 end