feat(measure_theory): add is_R_or_C.measurable_space (#10417)

Don't remove specific instances because otherwise Lean fails to generate `borel_space (ι → ℝ)`.

src/measure_theory/constructions/borel_space.lean

@@ -1140,6 +1140,14 @@ instance nat.borel_space : borel_space ℕ := ⟨borel_eq_top_of_discrete.symm
 instance int.borel_space : borel_space ℤ := ⟨borel_eq_top_of_discrete.symm⟩
 instance rat.borel_space : borel_space ℚ := ⟨borel_eq_top_of_encodable.symm⟩
 
+@[priority 900]
+instance is_R_or_C.measurable_space {𝕜 : Type*} [is_R_or_C 𝕜] : measurable_space 𝕜 := borel 𝕜
+@[priority 900]
+instance is_R_or_C.borel_space {𝕜 : Type*} [is_R_or_C 𝕜] : borel_space 𝕜 := ⟨rfl⟩
+
+/- Instances on `real` and `complex` are special cases of `is_R_or_C` but without these instances,
+Lean fails to prove `borel_space (ι → ℝ)`, so we leave them here. -/
+
 instance real.measurable_space : measurable_space ℝ := borel ℝ
 instance real.borel_space : borel_space ℝ := ⟨rfl⟩
 

src/measure_theory/function/conditional_expectation.lean

@@ -133,14 +133,14 @@ begin
   exact eventually_eq.fun_comp hff' (λ x, c • x),
 end
 
-lemma const_inner [is_R_or_C 𝕜] [borel_space 𝕜] [inner_product_space 𝕜 β]
+lemma const_inner {𝕜} [is_R_or_C 𝕜] [inner_product_space 𝕜 β]
   [second_countable_topology β] [opens_measurable_space β]
   {f : α → β} (hfm : ae_measurable' m f μ) (c : β) :
   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,
+    @measurable.inner _ _ _ _ _ m _ _ _ _ _ (@measurable_const _ _ _ m _) hf'_meas,
     hf_ae.mono (λ x hx, _)⟩,
   dsimp only,
   rw hx,
@@ -185,7 +185,7 @@ lemma ae_eq_trim_iff_of_ae_measurable' {α β} [add_group β] [measurable_space
 
 
 variables {α β γ E E' F F' G G' H 𝕜 : Type*} {p : ℝ≥0∞}
-  [is_R_or_C 𝕜] [measurable_space 𝕜] -- 𝕜 for ℝ or ℂ, together with a measurable_space
+  [is_R_or_C 𝕜] -- 𝕜 for ℝ or ℂ
   [measurable_space β] -- β for a generic measurable space
   -- E for an inner product space
   [inner_product_space 𝕜 E] [measurable_space E] [borel_space E] [second_countable_topology E]
@@ -519,7 +519,7 @@ section uniqueness_of_conditional_expectation
 
 /-! ## Uniqueness of the conditional expectation -/
 
-variables {m m0 : measurable_space α} {μ : measure α} [borel_space 𝕜]
+variables {m m0 : measurable_space α} {μ : measure α}
 
 lemma Lp_meas.ae_eq_zero_of_forall_set_integral_eq_zero
   (hm : m ≤ m0) (f : Lp_meas E' 𝕜 m p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
@@ -694,7 +694,7 @@ section condexp_L2
 
 local attribute [instance] fact_one_le_two_ennreal
 
-variables [complete_space E] [borel_space 𝕜] {m m0 : measurable_space α} {μ : measure α}
+variables [complete_space E] {m m0 : measurable_space α} {μ : measure α}
   {s t : set α}
 
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
@@ -721,11 +721,11 @@ lemma integrable_condexp_L2_of_is_finite_measure (hm : m ≤ m0) [is_finite_meas
   integrable (condexp_L2 𝕜 hm f) μ :=
 integrable_on_univ.mp $ integrable_on_condexp_L2_of_measure_ne_top hm (measure_ne_top _ _) f
 
-lemma norm_condexp_L2_le_one (hm : m ≤ m0) : ∥@condexp_L2 α E 𝕜 _ _ _ _ _ _ _ _ _ _ μ hm∥ ≤ 1 :=
+lemma norm_condexp_L2_le_one (hm : m ≤ m0) : ∥@condexp_L2 α E 𝕜 _ _ _ _ _ _ _ _ μ hm∥ ≤ 1 :=
 by { haveI : fact (m ≤ m0) := ⟨hm⟩, exact orthogonal_projection_norm_le _, }
 
 lemma norm_condexp_L2_le (hm : m ≤ m0) (f : α →₂[μ] E) : ∥condexp_L2 𝕜 hm f∥ ≤ ∥f∥ :=
-((@condexp_L2 _ E 𝕜 _ _ _ _ _ _ _ _ _ _ μ hm).le_op_norm f).trans
+((@condexp_L2 _ E 𝕜 _ _ _ _ _ _ _ _ μ hm).le_op_norm f).trans
   (mul_le_of_le_one_left (norm_nonneg _) (norm_condexp_L2_le_one hm))
 
 lemma snorm_condexp_L2_le (hm : m ≤ m0) (f : α →₂[μ] E) :
@@ -904,7 +904,7 @@ begin
   exact integral_condexp_L2_eq_of_fin_meas_real _ hs hμs,
 end
 
-variables {E'' 𝕜' : Type*} [is_R_or_C 𝕜'] [measurable_space 𝕜'] [borel_space 𝕜']
+variables {E'' 𝕜' : Type*} [is_R_or_C 𝕜']
   [measurable_space E''] [inner_product_space 𝕜' E''] [borel_space E'']
   [second_countable_topology E''] [complete_space E''] [normed_space ℝ E'']
   [is_scalar_tower ℝ 𝕜 E'] [is_scalar_tower ℝ 𝕜' E'']
@@ -1111,7 +1111,7 @@ calc ∫ a in s, (condexp_ind_smul hm ht hμt x) a ∂μ
 ... = (∫ a in s, condexp_L2 ℝ hm (indicator_const_Lp 2 ht hμt (1 : ℝ)) a ∂μ) • x :
   integral_smul_const _ x
 ... = (∫ a in s, indicator_const_Lp 2 ht hμt (1 : ℝ) a ∂μ) • x :
-  by rw @integral_condexp_L2_eq α _ ℝ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hm
+  by rw @integral_condexp_L2_eq α _ ℝ _ _ _ _ _ _ _ _ _ _ _ _ hm
     (indicator_const_Lp 2 ht hμt (1 : ℝ)) hs hμs
 ... = (μ (t ∩ s)).to_real • x :
   by rw [set_integral_indicator_const_Lp (hm s hs), smul_assoc, one_smul]
@@ -1132,7 +1132,7 @@ seen as an element of `α →₁[μ] G`.
 
 local attribute [instance] fact_one_le_two_ennreal
 
-variables {m m0 : measurable_space α} {μ : measure α} [borel_space 𝕜] [is_scalar_tower ℝ 𝕜 E']
+variables {m m0 : measurable_space α} {μ : measure α} [is_scalar_tower ℝ 𝕜 E']
   {s t : set α} [normed_space ℝ G]
 
 section condexp_ind_L1_fin
@@ -1417,7 +1417,7 @@ section condexp_L1
 
 local attribute [instance] fact_one_le_one_ennreal
 
-variables {m m0 : measurable_space α} {μ : measure α} [borel_space 𝕜] [is_scalar_tower ℝ 𝕜 F']
+variables {m m0 : measurable_space α} {μ : measure α} [is_scalar_tower ℝ 𝕜 F']
   {hm : m ≤ m0} [sigma_finite (μ.trim hm)] {f g : α → F'} {s : set α}
 
 /-- Conditional expectation of a function as a linear map from `α →₁[μ] F'` to itself. -/
@@ -1666,7 +1666,7 @@ open_locale classical
 
 local attribute [instance] fact_one_le_one_ennreal
 
-variables {𝕜} {m m0 : measurable_space α} {μ : measure α} [borel_space 𝕜] [is_scalar_tower ℝ 𝕜 F']
+variables {𝕜} {m m0 : measurable_space α} {μ : measure α} [is_scalar_tower ℝ 𝕜 F']
   {hm : m ≤ m0} [sigma_finite (μ.trim hm)] {f g : α → F'} {s : set α}
 
 /-- Conditional expectation of a function. Its value is 0 if the function is not integrable. -/

src/measure_theory/function/l1_space.lean

@@ -680,19 +680,17 @@ end
 end normed_space_over_complete_field
 
 section is_R_or_C
-variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] {f : α → 𝕜}
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {f : α → 𝕜}
 
-lemma integrable.of_real [borel_space 𝕜] {f : α → ℝ} (hf : integrable f μ) :
+lemma integrable.of_real {f : α → ℝ} (hf : integrable f μ) :
   integrable (λ x, (f x : 𝕜)) μ :=
 by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.of_real }
 
-lemma integrable.re_im_iff [borel_space 𝕜] :
+lemma integrable.re_im_iff :
   integrable (λ x, is_R_or_C.re (f x)) μ ∧ integrable (λ x, is_R_or_C.im (f x)) μ ↔
   integrable f μ :=
 by { simp_rw ← mem_ℒp_one_iff_integrable, exact mem_ℒp_re_im_iff }
 
-variable [opens_measurable_space 𝕜]
-
 lemma integrable.re (hf : integrable f μ) : integrable (λ x, is_R_or_C.re (f x)) μ :=
 by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.re, }
 
@@ -702,8 +700,7 @@ by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.im, }
 end is_R_or_C
 
 section inner_product
-variables {𝕜 E : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
-  [inner_product_space 𝕜 E]
+variables {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
   [measurable_space E] [opens_measurable_space E] [second_countable_topology E]
   {f : α → E}
 

src/measure_theory/function/l2_space.lean

@@ -62,8 +62,6 @@ end
 section inner_product_space
 open_locale complex_conjugate
 
-variables [measurable_space 𝕜] [borel_space 𝕜]
-
 include 𝕜
 
 instance : has_inner 𝕜 (α →₂[μ] E) := ⟨λ f g, ∫ a, ⟪f a, g a⟫ ∂μ⟩
@@ -137,7 +135,7 @@ end inner_product_space
 
 section indicator_const_Lp
 
-variables [measurable_space 𝕜] [borel_space 𝕜] {s : set α}
+variables {s : set α}
 
 variables (𝕜)
 
@@ -195,7 +193,7 @@ end L2
 section inner_continuous
 
 variables {α : Type*} [topological_space α] [measure_space α] [borel_space α] {𝕜 : Type*}
-  [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
+  [is_R_or_C 𝕜]
 variables (μ : measure α) [is_finite_measure μ]
 
 open_locale bounded_continuous_function complex_conjugate

src/measure_theory/function/lp_space.lean

@@ -1118,7 +1118,7 @@ end
 end monotonicity
 
 section is_R_or_C
-variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜}
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {f : α → 𝕜}
 
 lemma mem_ℒp.re (hf : mem_ℒp f p μ) : mem_ℒp (λ x, is_R_or_C.re (f x)) p μ :=
 begin
@@ -1137,8 +1137,7 @@ end
 end is_R_or_C
 
 section inner_product
-variables {E' 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
-  [inner_product_space 𝕜 E']
+variables {E' 𝕜 : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E']
   [measurable_space E'] [opens_measurable_space E'] [second_countable_topology E']
 
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 E' _ x y
@@ -1822,7 +1821,7 @@ lemma comp_mem_ℒp' (L : E →L[𝕜] F) {f : α → E} (hf : mem_ℒp f p μ)
 
 section is_R_or_C
 
-variables {K : Type*} [is_R_or_C K] [measurable_space K] [borel_space K]
+variables {K : Type*} [is_R_or_C K]
 
 lemma _root_.measure_theory.mem_ℒp.of_real
   {f : α → ℝ} (hf : mem_ℒp f p μ) : mem_ℒp (λ x, (f x : K)) p μ :=

src/measure_theory/function/special_functions.lean

@@ -79,7 +79,7 @@ end complex
 
 namespace is_R_or_C
 
-variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜]
+variables {𝕜 : Type*} [is_R_or_C 𝕜]
 
 @[measurability] lemma measurable_re : measurable (re : 𝕜 → ℝ) := continuous_re.measurable
 
@@ -146,8 +146,8 @@ end complex_composition
 
 section is_R_or_C_composition
 
-variables {α 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α] [measurable_space 𝕜]
-  [opens_measurable_space 𝕜] {f : α → 𝕜} {μ : measure_theory.measure α}
+variables {α 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α]
+  {f : α → 𝕜} {μ : measure_theory.measure α}
 
 @[measurability] lemma measurable.re (hf : measurable f) : measurable (λ x, is_R_or_C.re (f x)) :=
 is_R_or_C.measurable_re.comp hf
@@ -167,8 +167,8 @@ end is_R_or_C_composition
 
 section
 
-variables {α 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α] [measurable_space 𝕜]
-  [borel_space 𝕜] {f : α → 𝕜} {μ : measure_theory.measure α}
+variables {α 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α]
+  {f : α → 𝕜} {μ : measure_theory.measure α}
 
 @[measurability] lemma is_R_or_C.measurable_of_real : measurable (coe : ℝ → 𝕜) :=
 is_R_or_C.continuous_of_real.measurable
@@ -232,14 +232,14 @@ local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
 @[measurability]
 lemma measurable.inner [measurable_space α] [measurable_space E] [opens_measurable_space E]
-  [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜]
+  [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]
-  [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜]
+  [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⟫) μ :=
 begin

src/measure_theory/integral/set_integral.lean

@@ -520,7 +520,7 @@ We prove that for any set `s`, the function `λ f : α →₁[μ] E, ∫ x in s,
 
 section continuous_set_integral
 variables [normed_group E] [measurable_space E] [second_countable_topology E] [borel_space E]
-  {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜]
+  {𝕜 : Type*} [is_R_or_C 𝕜]
   [normed_group F] [measurable_space F] [second_countable_topology F] [borel_space F]
   [normed_space 𝕜 F]
   {p : ℝ≥0∞} {μ : measure α}
@@ -543,7 +543,7 @@ end
 
 /-- For `f : Lp E p μ`, we can define an element of `Lp E p (μ.restrict s)` by
 `(Lp.mem_ℒp f).restrict s).to_Lp f`. This map commutes with scalar multiplication. -/
-lemma Lp_to_Lp_restrict_smul [opens_measurable_space 𝕜] (c : 𝕜) (f : Lp F p μ) (s : set α) :
+lemma Lp_to_Lp_restrict_smul (c : 𝕜) (f : Lp F p μ) (s : set α) :
   ((Lp.mem_ℒp (c • f)).restrict s).to_Lp ⇑(c • f) = c • (((Lp.mem_ℒp f).restrict s).to_Lp f) :=
 begin
   ext1,
@@ -569,8 +569,7 @@ end
 variables (α F 𝕜)
 /-- Continuous linear map sending a function of `Lp F p μ` to the same function in
 `Lp F p (μ.restrict s)`. -/
-def Lp_to_Lp_restrict_clm [borel_space 𝕜] (μ : measure α) (p : ℝ≥0∞) [hp : fact (1 ≤ p)]
-  (s : set α) :
+def Lp_to_Lp_restrict_clm (μ : measure α) (p : ℝ≥0∞) [hp : fact (1 ≤ p)] (s : set α) :
   Lp F p μ →L[𝕜] Lp F p (μ.restrict s) :=
 @linear_map.mk_continuous 𝕜 𝕜 (Lp F p μ) (Lp F p (μ.restrict s)) _ _ _ _ _ _ (ring_hom.id 𝕜)
   ⟨λ f, mem_ℒp.to_Lp f ((Lp.mem_ℒp f).restrict s), λ f g, Lp_to_Lp_restrict_add f g s,
@@ -580,7 +579,7 @@ def Lp_to_Lp_restrict_clm [borel_space 𝕜] (μ : measure α) (p : ℝ≥0∞)
 variables {α F 𝕜}
 
 variables (𝕜)
-lemma Lp_to_Lp_restrict_clm_coe_fn [borel_space 𝕜] [hp : fact (1 ≤ p)] (s : set α) (f : Lp F p μ) :
+lemma Lp_to_Lp_restrict_clm_coe_fn [hp : fact (1 ≤ p)] (s : set α) (f : Lp F p μ) :
   Lp_to_Lp_restrict_clm α F 𝕜 μ p s f =ᵐ[μ.restrict s] f :=
 mem_ℒp.coe_fn_to_Lp ((Lp.mem_ℒp f).restrict s)
 variables {𝕜}
@@ -766,12 +765,11 @@ lemma set_integral_comp_Lp (L : E →L[𝕜] F) (φ : Lp E p μ) {s : set α} (h
   ∫ a in s, (L.comp_Lp φ) a ∂μ = ∫ a in s, L (φ a) ∂μ :=
 set_integral_congr_ae hs ((L.coe_fn_comp_Lp φ).mono (λ x hx hx2, hx))
 
-lemma continuous_integral_comp_L1 [measurable_space 𝕜] [opens_measurable_space 𝕜] (L : E →L[𝕜] F) :
+lemma continuous_integral_comp_L1 (L : E →L[𝕜] F) :
   continuous (λ (φ : α →₁[μ] E), ∫ (a : α), L (φ a) ∂μ) :=
 by { rw ← funext L.integral_comp_Lp, exact continuous_integral.comp (L.comp_LpL 1 μ).continuous, }
 
-variables [complete_space E] [measurable_space 𝕜] [opens_measurable_space 𝕜]
-  [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] [is_scalar_tower ℝ 𝕜 F]
+variables [complete_space E] [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E] [is_scalar_tower ℝ 𝕜 F]
 
 lemma integral_comp_comm (L : E →L[𝕜] F) {φ : α → E} (φ_int : integrable φ μ) :
   ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
@@ -820,7 +818,6 @@ variables [measurable_space F] [borel_space F] [second_countable_topology F] [co
   [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
   [borel_space E] [second_countable_topology E] [complete_space E] [normed_space ℝ E]
   [is_scalar_tower ℝ 𝕜 E]
-  [measurable_space 𝕜] [opens_measurable_space 𝕜]
 
 lemma integral_comp_comm (L : E →ₗᵢ[𝕜] F) (φ : α → E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
 L.to_continuous_linear_map.integral_comp_comm' L.antilipschitz _
@@ -830,7 +827,6 @@ end linear_isometry
 variables [borel_space E] [second_countable_topology E] [complete_space E] [normed_space ℝ E]
   [measurable_space F] [borel_space F] [second_countable_topology F] [complete_space F]
   [normed_space ℝ F]
-  [measurable_space 𝕜] [borel_space 𝕜]
 
 @[norm_cast] lemma integral_of_real {f : α → ℝ} : ∫ a, (f a : 𝕜) ∂μ = ↑∫ a, f a ∂μ :=
 (@is_R_or_C.of_real_li 𝕜 _).integral_comp_comm f