refactor(measure_theory): add typeclasses for measurability of operat…

…ions (#6832)

With these typeclasses and lemmas we can use, e.g., `measurable.mul` for any type with measurable `uncurry (*)`, not only those with `has_continuous_mul`.

New typeclasses:

* `has_measurable_add`, `has_measurable_add₂`: measurable left/right addition and measurable `uncurry (+)`;
* `has_measurable_mul`, `has_measurable_mul₂`: measurable left/right multiplication and measurable `uncurry (*)`;
* `has_measurable_pow`: measurable `uncurry (^)`
* `has_measurable_sub`, `has_measurable_sub₂`: measurable left/right subtraction and measurable `λ (a, b), a - b`
* `has_measurable_div`, `has_measurable_div₂` : measurability of division as a function of numerator/denominator and measurability of `λ (a, b), a / b`;
* `has_measurable_neg`, `has_measurable_inv`: measurable negation/inverse;
* `has_measurable_const_smul`, `has_measurable_smul`: measurable `λ x, c • x` and measurable `λ (c, x), c • x`

src/analysis/mean_inequalities.lean

@@ -699,11 +699,10 @@ begin
   begin
     simp only [div_eq_mul_inv],
     rw lintegral_add',
-    { rw [lintegral_mul_const'' _ hf.ennreal_rpow_const,
-        lintegral_mul_const'' _ hg.ennreal_rpow_const, hf_norm, hg_norm, ← div_eq_mul_inv,
-        ← div_eq_mul_inv, hpq.inv_add_inv_conj_ennreal], },
-    { exact hf.ennreal_rpow_const.ennreal_mul ae_measurable_const, },
-    { exact hg.ennreal_rpow_const.ennreal_mul ae_measurable_const, },
+    { rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const'' _ (hg.pow_const q),
+        hf_norm, hg_norm, ← div_eq_mul_inv, ← div_eq_mul_inv, hpq.inv_add_inv_conj_ennreal], },
+    { exact (hf.pow_const _).mul_const _, },
+    { exact (hg.pow_const _).mul_const _, },
   end
 end
 
@@ -731,7 +730,7 @@ lemma lintegral_rpow_fun_mul_inv_snorm_eq_one {p : ℝ} (hp0_lt : 0 < p) {f : α
   ∫⁻ c, (fun_mul_inv_snorm f p μ c)^p ∂μ = 1 :=
 begin
   simp_rw fun_mul_inv_snorm_rpow hp0_lt,
-  rw [lintegral_mul_const'' _ hf.ennreal_rpow_const, mul_inv_cancel hf_nonzero hf_top],
+  rw [lintegral_mul_const'' _ (hf.pow_const p), mul_inv_cancel hf_nonzero hf_top],
 end
 
 /-- Hölder's inequality in case of finite non-zero integrals -/
@@ -759,16 +758,16 @@ begin
     refine mul_le_mul _ (le_refl (npf * nqg)),
     have hf1 := lintegral_rpow_fun_mul_inv_snorm_eq_one hpq.pos hf hf_nonzero hf_nontop,
     have hg1 := lintegral_rpow_fun_mul_inv_snorm_eq_one hpq.symm.pos hg hg_nonzero hg_nontop,
-    exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.ennreal_mul ae_measurable_const)
-      (hg.ennreal_mul ae_measurable_const) hf1 hg1,
+    exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _)
+      (hg.mul_const _) hf1 hg1,
   end
 end
 
 lemma ae_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0_lt : 0 < p) {f : α → ℝ≥0∞}
   (hf : ae_measurable f μ) (hf_zero : ∫⁻ a, (f a)^p ∂μ = 0) :
   f =ᵐ[μ] 0 :=
 begin
-  rw lintegral_eq_zero_iff' hf.ennreal_rpow_const at hf_zero,
+  rw lintegral_eq_zero_iff' (hf.pow_const p) at hf_zero,
   refine filter.eventually.mp hf_zero (filter.eventually_of_forall (λ x, _)),
   dsimp only,
   rw [pi.zero_apply, rpow_eq_zero_iff],
@@ -857,16 +856,14 @@ begin
   end
   ... < ⊤ :
   begin
-    rw [lintegral_add', lintegral_const_mul'' _ hf.ennreal_rpow_const,
-      lintegral_const_mul'' _ hg.ennreal_rpow_const, ennreal.add_lt_top],
+    rw [lintegral_add', lintegral_const_mul'' _ (hf.pow_const p),
+      lintegral_const_mul'' _ (hg.pow_const p), ennreal.add_lt_top],
     { have h_two : (2 : ℝ≥0∞) ^ (p - 1) < ⊤,
       from ennreal.rpow_lt_top_of_nonneg (by simp [hp1]) ennreal.coe_ne_top,
       repeat {rw ennreal.mul_lt_top_iff},
       simp [hf_top, hg_top, h_two], },
-    { exact (ennreal.continuous_const_mul (by simp)).measurable.comp_ae_measurable
-        hf.ennreal_rpow_const, },
-    { exact (ennreal.continuous_const_mul (by simp)).measurable.comp_ae_measurable
-        hg.ennreal_rpow_const },
+    { exact (hf.pow_const _).const_mul _ },
+    { exact (hg.pow_const _).const_mul _ },
   end
 end
 
@@ -896,7 +893,7 @@ begin
   begin
     refine ennreal.rpow_le_rpow _ (by simp [hp0]),
     simp_rw ennreal.rpow_mul,
-    exact ennreal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 hf.ennreal_rpow_const hg.ennreal_rpow_const,
+    exact ennreal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)
   end
   ... = (∫⁻ (a : α), (f a) ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), (g a) ^ r ∂μ) ^ (1 / r) :
   begin
@@ -916,7 +913,7 @@ lemma lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ}
   (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hf_top : ∫⁻ a, (f a) ^ p ∂μ ≠ ⊤) :
   ∫⁻ a, (f a) * (g a) ^ (p - 1) ∂μ ≤ (∫⁻ a, (f a)^p ∂μ) ^ (1/p) * (∫⁻ a, (g a)^p ∂μ) ^ (1/q) :=
 begin
-  refine le_trans (ennreal.lintegral_mul_le_Lp_mul_Lq μ hpq hf hg.ennreal_rpow_const) _,
+  refine le_trans (ennreal.lintegral_mul_le_Lp_mul_Lq μ hpq hf (hg.pow_const _)) _,
   by_cases hf_zero_rpow : (∫⁻ (a : α), (f a) ^ p ∂μ) ^ (1 / p) = 0,
   { rw [hf_zero_rpow, zero_mul],
     exact zero_le _, },
@@ -956,12 +953,12 @@ begin
     ... = ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ :
   begin
     have h_add_m : ae_measurable (λ (a : α), ((f + g) a) ^ (p-1)) μ,
-      from (hf.add hg).ennreal_rpow_const,
+      from (hf.add hg).pow_const _,
     have h_add_apply : ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ
       = ∫⁻ (a : α), (f a + g a) * (f + g) a ^ (p - 1) ∂μ,
     from rfl,
     simp_rw [h_add_apply, add_mul],
-    rw lintegral_add' (hf.ennreal_mul h_add_m) (hg.ennreal_mul h_add_m),
+    rw lintegral_add' (hf.mul h_add_m) (hg.mul h_add_m),
   end
     ... ≤ ((∫⁻ a, (f a)^p ∂μ) ^ (1/p) + (∫⁻ a, (g a)^p ∂μ) ^ (1/p))
       * (∫⁻ a, (f a + g a)^p ∂μ) ^ (1/q) :

src/analysis/special_functions/pow.lean

@@ -148,6 +148,11 @@ lemma has_fderiv_at_cpow {p : ℂ × ℂ} (hp : 0 < p.1.re ∨ p.1.im ≠ 0) :
       (p.1 ^ p.2 * log p.1) • continuous_linear_map.snd ℂ ℂ ℂ) p :=
 (has_strict_fderiv_at_cpow hp).has_fderiv_at
 
+instance : has_measurable_pow ℂ ℂ :=
+⟨measurable.ite (measurable_fst (measurable_set_singleton 0))
+  (measurable.ite (measurable_snd (measurable_set_singleton 0)) measurable_one measurable_zero)
+  (measurable_fst.clog.mul measurable_snd).cexp⟩
+
 end complex
 
 section lim
@@ -156,12 +161,6 @@ open complex
 
 variables {α : Type*}
 
-lemma measurable.cpow [measurable_space α] {f g : α → ℂ} (hf : measurable f) (hg : measurable g) :
-  measurable (λ x, f x ^ g x) :=
-measurable.ite (hf $ measurable_set_singleton _)
-  (measurable.ite (hg $ measurable_set_singleton _) measurable_const measurable_const)
-  (hf.clog.mul hg).cexp
-
 lemma filter.tendsto.cpow {l : filter α} {f g : α → ℂ} {a b : ℂ} (hf : tendsto f l (𝓝 a))
   (hg : tendsto g l (𝓝 b)) (ha : 0 < a.re ∨ a.im ≠ 0) :
   tendsto (λ x, f x ^ g x) l (𝓝 (a ^ b)) :=
@@ -835,30 +834,11 @@ end
 
 end sqrt
 
-end real
-
-section measurability_real
-
-open complex
-
-lemma measurable.rpow {α} [measurable_space α] {f g : α → ℝ} (hf : measurable f)
-  (hg : measurable g) :
-  measurable (λ a : α, (f a) ^ (g a)) :=
-measurable_re.comp $ ((measurable_of_real.comp hf).cpow (measurable_of_real.comp hg))
+instance : has_measurable_pow ℝ ℝ :=
+⟨complex.measurable_re.comp $ ((complex.measurable_of_real.comp measurable_fst).pow
+  (complex.measurable_of_real.comp measurable_snd))⟩
 
-lemma measurable.rpow_const {α} [measurable_space α] {f : α → ℝ} (hf : measurable f) {y : ℝ} :
-  measurable (λ a : α, (f a) ^ y) :=
-hf.rpow measurable_const
-
-lemma ae_measurable.rpow_const {α} [measurable_space α] {f : α → ℝ}
-  {μ : measure_theory.measure α} (hf : ae_measurable f μ) {y : ℝ} :
-  ae_measurable (λ a : α, (f a) ^ y) μ :=
-measurable.comp_ae_measurable (measurable.rpow_const measurable_id) hf
-
-lemma real.measurable_rpow_const {y : ℝ} : measurable (λ x : ℝ, x ^ y) :=
-measurable_id.rpow_const
-
-end measurability_real
+end real
 
 section differentiability
 open real
@@ -1147,23 +1127,10 @@ begin
   rw [←nnreal.coe_rpow, nnreal.of_real_coe],
 end
 
-end nnreal
-
-namespace measurable
-
-variables {α : Type*} [measurable_space α]
+instance : has_measurable_pow ℝ≥0 ℝ :=
+⟨(measurable_fst.nnreal_coe.pow measurable_snd).subtype_mk⟩
 
-lemma nnreal_rpow {f : α → ℝ≥0} (hf : measurable f)
-  {g : α → ℝ} (hg : measurable g) :
-  measurable (λ a : α, (f a) ^ (g a)) :=
-(hf.nnreal_coe.rpow hg).subtype_mk
-
-lemma nnreal_rpow_const {f : α → ℝ≥0} (hf : measurable f)
-  {y : ℝ} :
-  measurable (λ a : α, (f a) ^ y) :=
-hf.nnreal_rpow measurable_const
-
-end measurable
+end nnreal
 
 open filter
 
@@ -1695,42 +1662,17 @@ lemma rpow_left_monotone_of_nonneg {x : ℝ} (hx : 0 ≤ x) : monotone (λ y : 
 lemma rpow_left_strict_mono_of_pos {x : ℝ} (hx : 0 < x) : strict_mono (λ y : ℝ≥0∞, y^x) :=
 λ y z hyz, rpow_lt_rpow hyz hx
 
-end ennreal
-
-section measurability_ennreal
-
-variables {α : Type*} [measurable_space α]
-
-lemma ennreal.measurable_rpow : measurable (λ p : ℝ≥0∞ × ℝ, p.1 ^ p.2) :=
+instance : has_measurable_pow ℝ≥0∞ ℝ :=
 begin
-  refine ennreal.measurable_of_measurable_nnreal_prod _ _,
+  refine ⟨ennreal.measurable_of_measurable_nnreal_prod _ _⟩,
   { simp_rw ennreal.coe_rpow_def,
     refine measurable.ite _ measurable_const
-      (measurable_fst.nnreal_rpow measurable_snd).ennreal_coe,
+      (measurable_fst.pow measurable_snd).ennreal_coe,
     exact measurable_set.inter (measurable_fst (measurable_set_singleton 0))
       (measurable_snd measurable_set_Iio), },
   { simp_rw ennreal.top_rpow_def,
     refine measurable.ite measurable_set_Ioi measurable_const _,
     exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const, },
 end
 
-lemma measurable.ennreal_rpow {f : α → ℝ≥0∞} (hf : measurable f) {g : α → ℝ} (hg : measurable g) :
-  measurable (λ a : α, (f a) ^ (g a)) :=
-begin
-  change measurable ((λ p : ℝ≥0∞ × ℝ, p.1 ^ p.2) ∘ (λ a, (f a, g a))),
-  exact ennreal.measurable_rpow.comp (measurable.prod hf hg),
-end
-
-lemma measurable.ennreal_rpow_const {f : α → ℝ≥0∞} (hf : measurable f) {y : ℝ} :
-  measurable (λ a : α, (f a) ^ y) :=
-hf.ennreal_rpow measurable_const
-
-lemma ennreal.measurable_rpow_const {y : ℝ} : measurable (λ a : ℝ≥0∞, a ^ y) :=
-measurable_id.ennreal_rpow_const
-
-lemma ae_measurable.ennreal_rpow_const {α} [measurable_space α] {f : α → ℝ≥0∞}
-  {μ : measure_theory.measure α} (hf : ae_measurable f μ) {y : ℝ} :
-  ae_measurable (λ a : α, (f a) ^ y) μ :=
-ennreal.measurable_rpow_const.comp_ae_measurable hf
-
-end measurability_ennreal
+end ennreal

src/measure_theory/ae_eq_fun.lean

@@ -372,7 +372,8 @@ instance [topological_space γ] [borel_space γ] [comm_group γ] [topological_gr
 
 section semimodule
 
-variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜]
+variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜] [measurable_space 𝕜]
+  [opens_measurable_space 𝕜]
 variables [topological_space γ] [borel_space γ] [add_comm_monoid γ] [semimodule 𝕜 γ]
   [has_continuous_smul 𝕜 γ]
 

src/measure_theory/ae_eq_fun_metric.lean

@@ -94,7 +94,7 @@ induction_on₃ f g h $ λ f hf g hg h hh, by simp [edist_mk_mk, edist_dist, dis
 
 section normed_space
 
-variables {𝕜 : Type*} [normed_field 𝕜]
+variables {𝕜 : Type*} [normed_field 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜]
 variables [normed_group γ] [second_countable_topology γ] [normed_space 𝕜 γ] [borel_space γ]
 
 lemma edist_smul (c : 𝕜) (f : α →ₘ[μ] γ) : edist (c • f) 0 = (ennreal.of_real ∥c∥) * edist f 0 :=