chore(measure_theory): measurability statements for coercions, cohere…

…nt naming (#7854)

Also add a few lemmas on measure theory

src/algebra/ordered_group.lean

@@ -716,6 +716,10 @@ begin
     exact add_le_add h h, }
 end
 
+@[simp] lemma max_zero_sub_max_neg_zero_eq_self (a : α) :
+  max a 0 - max (-a) 0 = a :=
+by { rcases le_total a 0 with h|h; simp [h] }
+
 lemma le_of_forall_pos_le_add [densely_ordered α] (h : ∀ ε : α, 0 < ε → a ≤ b + ε) : a ≤ b :=
 le_of_forall_le_of_dense $ λ c hc,
 calc a ≤ b + (c - b) : h _ (sub_pos_of_lt hc)

src/analysis/mean_inequalities.lean

@@ -1032,7 +1032,7 @@ theorem nnreal.lintegral_mul_le_Lp_mul_Lq {p q : ℝ} (hpq : p.is_conjugate_expo
   ∫⁻ a, (f * g) a ∂μ ≤ (∫⁻ a, (f a)^p ∂μ)^(1/p) * (∫⁻ a, (g a)^q ∂μ)^(1/q) :=
 begin
   simp_rw [pi.mul_apply, ennreal.coe_mul],
-  exact ennreal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.ennreal_coe hg.ennreal_coe,
+  exact ennreal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.coe_nnreal_ennreal hg.coe_nnreal_ennreal,
 end
 
 end lintegral

src/analysis/special_functions/pow.lean

@@ -1152,7 +1152,7 @@ begin
 end
 
 instance : has_measurable_pow ℝ≥0 ℝ :=
-⟨(measurable_fst.nnreal_coe.pow measurable_snd).subtype_mk⟩
+⟨(measurable_fst.coe_nnreal_real.pow measurable_snd).subtype_mk⟩
 
 end nnreal
 
@@ -1691,7 +1691,7 @@ begin
   refine ⟨ennreal.measurable_of_measurable_nnreal_prod _ _⟩,
   { simp_rw ennreal.coe_rpow_def,
     refine measurable.ite _ measurable_const
-      (measurable_fst.pow measurable_snd).ennreal_coe,
+      (measurable_fst.pow measurable_snd).coe_nnreal_ennreal,
     exact measurable_set.inter (measurable_fst (measurable_set_singleton 0))
       (measurable_snd measurable_set_Iio), },
   { simp_rw ennreal.top_rpow_def,

src/data/real/nnreal.lean

@@ -235,6 +235,10 @@ instance : canonically_linear_ordered_add_monoid ℝ≥0 :=
   ..nnreal.order_bot,
   ..nnreal.linear_order }
 
+instance : linear_ordered_add_comm_monoid ℝ≥0 :=
+{ .. nnreal.comm_semiring,
+  .. nnreal.canonically_linear_ordered_add_monoid }
+
 instance : distrib_lattice ℝ≥0 := by apply_instance
 
 instance : semilattice_inf_bot ℝ≥0 :=

src/measure_theory/bochner_integration.lean

@@ -1279,6 +1279,14 @@ begin
     rw [this, hfi], refl }
 end
 
+lemma integral_eq_integral_pos_part_sub_integral_neg_part {f : α → ℝ} (hf : integrable f μ) :
+  ∫ a, f a ∂μ = (∫ a, real.to_nnreal (f a) ∂μ) - (∫ a, real.to_nnreal (-f a) ∂μ) :=
+begin
+  rw [← integral_sub hf.real_to_nnreal],
+  { simp },
+  { exact hf.neg.real_to_nnreal }
+end
+
 lemma integral_nonneg_of_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ∫ a, f a ∂μ :=
 begin
   by_cases hfm : ae_measurable f μ,
@@ -1297,7 +1305,7 @@ end
 lemma integral_to_real {f : α → ℝ≥0∞} (hfm : ae_measurable f μ) (hf : ∀ᵐ x ∂μ, f x < ∞) :
   ∫ a, (f a).to_real ∂μ = (∫⁻ a, f a ∂μ).to_real :=
 begin
-  rw [integral_eq_lintegral_of_nonneg_ae _ hfm.to_real],
+  rw [integral_eq_lintegral_of_nonneg_ae _ hfm.ennreal_to_real],
   { rw lintegral_congr_ae, refine hf.mp (eventually_of_forall _),
     intros x hx, rw [lt_top_iff_ne_top] at hx, simp [hx] },
   { exact (eventually_of_forall $ λ x, ennreal.to_real_nonneg) }

src/measure_theory/borel_space.lean

@@ -8,6 +8,8 @@ import analysis.complex.basic
 import analysis.normed_space.finite_dimension
 import topology.G_delta
 import measure_theory.arithmetic
+import topology.semicontinuous
+import topology.instances.ereal
 
 /-!
 # Borel (measurable) space
@@ -604,13 +606,21 @@ begin
   rintro _ ⟨x, rfl⟩, exact hf x
 end
 
+lemma upper_semicontinuous.measurable [topological_space δ] [opens_measurable_space δ]
+  {f : δ → α} (hf : upper_semicontinuous f) : measurable f :=
+measurable_of_Iio (λ y, (hf.is_open_preimage y).measurable_set)
+
 lemma measurable_of_Ioi {f : δ → α} (hf : ∀ x, measurable_set (f ⁻¹' Ioi x)) : measurable f :=
 begin
   convert measurable_generate_from _,
   exact borel_space.measurable_eq.trans (borel_eq_generate_Ioi _),
   rintro _ ⟨x, rfl⟩, exact hf x
 end
 
+lemma lower_semicontinuous.measurable [topological_space δ] [opens_measurable_space δ]
+  {f : δ → α} (hf : lower_semicontinuous f) : measurable f :=
+measurable_of_Ioi (λ y, (hf.is_open_preimage y).measurable_set)
+
 lemma measurable_of_Iic {f : δ → α} (hf : ∀ x, measurable_set (f ⁻¹' Iic x)) : measurable f :=
 begin
   apply measurable_of_Ioi,
@@ -889,6 +899,9 @@ instance nnreal.borel_space : borel_space ℝ≥0 := subtype.borel_space _
 instance ennreal.measurable_space : measurable_space ℝ≥0∞ := borel ℝ≥0∞
 instance ennreal.borel_space : borel_space ℝ≥0∞ := ⟨rfl⟩
 
+instance ereal.measurable_space : measurable_space ereal := borel ereal
+instance ereal.borel_space : borel_space ereal := ⟨rfl⟩
+
 instance complex.measurable_space : measurable_space ℂ := borel ℂ
 instance complex.borel_space : borel_space ℂ := ⟨rfl⟩
 
@@ -1049,37 +1062,45 @@ end real
 
 variable [measurable_space α]
 
+@[measurability]
+lemma measurable_real_to_nnreal : measurable (real.to_nnreal) :=
+nnreal.continuous_of_real.measurable
+
 @[measurability]
 lemma measurable.real_to_nnreal {f : α → ℝ} (hf : measurable f) :
   measurable (λ x, real.to_nnreal (f x)) :=
-nnreal.continuous_of_real.measurable.comp hf
+measurable_real_to_nnreal.comp hf
 
 @[measurability]
 lemma ae_measurable.real_to_nnreal {f : α → ℝ} {μ : measure α} (hf : ae_measurable f μ) :
   ae_measurable (λ x, real.to_nnreal (f x)) μ :=
-nnreal.continuous_of_real.measurable.comp_ae_measurable hf
+measurable_real_to_nnreal.comp_ae_measurable hf
 
 @[measurability]
-lemma nnreal.measurable_coe : measurable (coe : ℝ≥0 → ℝ) :=
+lemma measurable_coe_nnreal_real : measurable (coe : ℝ≥0 → ℝ) :=
 nnreal.continuous_coe.measurable
 
 @[measurability]
-lemma measurable.nnreal_coe {f : α → ℝ≥0} (hf : measurable f) :
+lemma measurable.coe_nnreal_real {f : α → ℝ≥0} (hf : measurable f) :
   measurable (λ x, (f x : ℝ)) :=
-nnreal.measurable_coe.comp hf
+measurable_coe_nnreal_real.comp hf
 
 @[measurability]
-lemma ae_measurable.nnreal_coe {f : α → ℝ≥0} {μ : measure α} (hf : ae_measurable f μ) :
+lemma ae_measurable.coe_nnreal_real {f : α → ℝ≥0} {μ : measure α} (hf : ae_measurable f μ) :
   ae_measurable (λ x, (f x : ℝ)) μ :=
-nnreal.measurable_coe.comp_ae_measurable hf
+measurable_coe_nnreal_real.comp_ae_measurable hf
+
+@[measurability]
+lemma measurable_coe_nnreal_ennreal : measurable (coe : ℝ≥0 → ℝ≥0∞) :=
+ennreal.continuous_coe.measurable
 
 @[measurability]
-lemma measurable.ennreal_coe {f : α → ℝ≥0} (hf : measurable f) :
+lemma measurable.coe_nnreal_ennreal {f : α → ℝ≥0} (hf : measurable f) :
   measurable (λ x, (f x : ℝ≥0∞)) :=
 ennreal.continuous_coe.measurable.comp hf
 
 @[measurability]
-lemma ae_measurable.ennreal_coe {f : α → ℝ≥0} {μ : measure α} (hf :  ae_measurable f μ) :
+lemma ae_measurable.coe_nnreal_ennreal {f : α → ℝ≥0} {μ : measure α} (hf : ae_measurable f μ) :
   ae_measurable (λ x, (f x : ℝ≥0∞)) μ :=
 ennreal.continuous_coe.measurable.comp_ae_measurable hf
 
@@ -1094,10 +1115,6 @@ ennreal.ne_top_homeomorph_nnreal.to_measurable_equiv
 
 namespace ennreal
 
-@[measurability]
-lemma measurable_coe : measurable (coe : ℝ≥0 → ℝ≥0∞) :=
-measurable_id.ennreal_coe
-
 lemma measurable_of_measurable_nnreal {f : ℝ≥0∞ → α}
   (h : measurable (λ p : ℝ≥0, f p)) : measurable f :=
 measurable_of_measurable_on_compl_singleton ∞
@@ -1106,7 +1123,8 @@ measurable_of_measurable_on_compl_singleton ∞
 /-- `ℝ≥0∞` is `measurable_equiv` to `ℝ≥0 ⊕ unit`. -/
 def ennreal_equiv_sum : ℝ≥0∞ ≃ᵐ ℝ≥0 ⊕ unit :=
 { measurable_to_fun  := measurable_of_measurable_nnreal measurable_inl,
-  measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ℝ≥0∞ unit _ _ ∞),
+  measurable_inv_fun := measurable_sum measurable_coe_nnreal_ennreal
+    (@measurable_const ℝ≥0∞ unit _ _ ∞),
   .. equiv.option_equiv_sum_punit ℝ≥0 }
 
 open function (uncurry)
@@ -1134,7 +1152,7 @@ ennreal.continuous_of_real.measurable
 
 @[measurability]
 lemma measurable_to_real : measurable ennreal.to_real :=
-ennreal.measurable_of_measurable_nnreal nnreal.measurable_coe
+ennreal.measurable_of_measurable_nnreal measurable_coe_nnreal_real
 
 @[measurability]
 lemma measurable_to_nnreal : measurable ennreal.to_nnreal :=
@@ -1143,7 +1161,7 @@ ennreal.measurable_of_measurable_nnreal measurable_id
 instance : has_measurable_mul₂ ℝ≥0∞ :=
 begin
   refine ⟨measurable_of_measurable_nnreal_nnreal _ _ _⟩,
-  { simp only [← ennreal.coe_mul, measurable_mul.ennreal_coe] },
+  { simp only [← ennreal.coe_mul, measurable_mul.coe_nnreal_ennreal] },
   { simp only [ennreal.top_mul, ennreal.coe_eq_zero],
     exact measurable_const.piecewise (measurable_set_singleton _) measurable_const },
   { simp only [ennreal.mul_top, ennreal.coe_eq_zero],
@@ -1152,28 +1170,33 @@ end
 
 instance : has_measurable_sub₂ ℝ≥0∞ :=
 ⟨by apply measurable_of_measurable_nnreal_nnreal;
-  simp [← ennreal.coe_sub, continuous_sub.measurable.ennreal_coe]⟩
+  simp [← ennreal.coe_sub, continuous_sub.measurable.coe_nnreal_ennreal]⟩
 
 instance : has_measurable_inv ℝ≥0∞ := ⟨ennreal.continuous_inv.measurable⟩
 
 end ennreal
 
 @[measurability]
-lemma measurable.to_nnreal {f : α → ℝ≥0∞} (hf : measurable f) :
+lemma measurable.ennreal_to_nnreal {f : α → ℝ≥0∞} (hf : measurable f) :
   measurable (λ x, (f x).to_nnreal) :=
 ennreal.measurable_to_nnreal.comp hf
 
-lemma measurable_ennreal_coe_iff {f : α → ℝ≥0} :
+@[measurability]
+lemma ae_measurable.ennreal_to_nnreal {f : α → ℝ≥0∞} {μ : measure α} (hf : ae_measurable f μ) :
+  ae_measurable (λ x, (f x).to_nnreal) μ :=
+ennreal.measurable_to_nnreal.comp_ae_measurable hf
+
+lemma measurable_coe_nnreal_ennreal_iff {f : α → ℝ≥0} :
   measurable (λ x, (f x : ℝ≥0∞)) ↔ measurable f :=
-⟨λ h, h.to_nnreal, λ h, h.ennreal_coe⟩
+⟨λ h, h.ennreal_to_nnreal, λ h, h.coe_nnreal_ennreal⟩
 
 @[measurability]
-lemma measurable.to_real {f : α → ℝ≥0∞} (hf : measurable f) :
+lemma measurable.ennreal_to_real {f : α → ℝ≥0∞} (hf : measurable f) :
   measurable (λ x, ennreal.to_real (f x)) :=
 ennreal.measurable_to_real.comp hf
 
 @[measurability]
-lemma ae_measurable.to_real {f : α → ℝ≥0∞} {μ : measure α} (hf : ae_measurable f μ) :
+lemma ae_measurable.ennreal_to_real {f : α → ℝ≥0∞} {μ : measure α} (hf : ae_measurable f μ) :
   ae_measurable (λ x, ennreal.to_real (f x)) μ :=
 ennreal.measurable_to_real.comp_ae_measurable hf
 
@@ -1189,7 +1212,7 @@ lemma measurable.nnreal_tsum {ι} [encodable ι] {f : ι → α → ℝ≥0} (h
   measurable (λ x, ∑' i, f i x) :=
 begin
   simp_rw [nnreal.tsum_eq_to_nnreal_tsum],
-  exact (measurable.ennreal_tsum (λ i, (h i).ennreal_coe)).to_nnreal,
+  exact (measurable.ennreal_tsum (λ i, (h i).coe_nnreal_ennreal)).ennreal_to_nnreal,
 end
 
 @[measurability]
@@ -1199,6 +1222,57 @@ lemma ae_measurable.ennreal_tsum {ι} [encodable ι] {f : ι → α → ℝ≥0
 by { simp_rw [ennreal.tsum_eq_supr_sum], apply ae_measurable_supr,
   exact λ s, finset.ae_measurable_sum s (λ i _, h i) }
 
+@[measurability]
+lemma measurable_coe_real_ereal : measurable (coe : ℝ → ereal) :=
+continuous_coe_real_ereal.measurable
+
+@[measurability]
+lemma measurable.coe_real_ereal {f : α → ℝ} (hf : measurable f) :
+  measurable (λ x, (f x : ereal)) :=
+measurable_coe_real_ereal.comp hf
+
+@[measurability]
+lemma ae_measurable.coe_real_ereal {f : α → ℝ} {μ : measure α} (hf : ae_measurable f μ) :
+  ae_measurable (λ x, (f x : ereal)) μ :=
+measurable_coe_real_ereal.comp_ae_measurable hf
+
+/-- The set of finite `ereal` numbers is `measurable_equiv` to `ℝ`. -/
+def measurable_equiv.ereal_equiv_real : ({⊥, ⊤} : set ereal).compl ≃ᵐ ℝ :=
+ereal.ne_bot_top_homeomorph_real.to_measurable_equiv
+
+lemma ereal.measurable_of_measurable_real {f : ereal → α}
+  (h : measurable (λ p : ℝ, f p)) : measurable f :=
+measurable_of_measurable_on_compl_finite {⊥, ⊤} (by simp)
+  (measurable_equiv.ereal_equiv_real.symm.measurable_coe_iff.1 h)
+
+@[measurability]
+lemma measurable_ereal_to_real : measurable ereal.to_real :=
+ereal.measurable_of_measurable_real (by simpa using measurable_id)
+
+@[measurability]
+lemma measurable.ereal_to_real {f : α → ereal} (hf : measurable f) :
+  measurable (λ x, (f x).to_real) :=
+measurable_ereal_to_real.comp hf
+
+@[measurability]
+lemma ae_measurable.ereal_to_real {f : α → ereal} {μ : measure α} (hf : ae_measurable f μ) :
+  ae_measurable (λ x, (f x).to_real) μ :=
+measurable_ereal_to_real.comp_ae_measurable hf
+
+@[measurability]
+lemma measurable_coe_ennreal_ereal : measurable (coe : ℝ≥0∞ → ereal) :=
+continuous_coe_ennreal_ereal.measurable
+
+@[measurability]
+lemma measurable.coe_ereal_ennreal {f : α → ℝ≥0∞} (hf : measurable f) :
+  measurable (λ x, (f x : ereal)) :=
+measurable_coe_ennreal_ereal.comp hf
+
+@[measurability]
+lemma ae_measurable.coe_ereal_ennreal {f : α → ℝ≥0∞} {μ : measure α} (hf : ae_measurable f μ) :
+  ae_measurable (λ x, (f x : ereal)) μ :=
+measurable_coe_ennreal_ereal.comp_ae_measurable hf
+
 section normed_group
 
 variables [normed_group α] [opens_measurable_space α] [measurable_space β]
@@ -1231,12 +1305,12 @@ measurable_nnnorm.comp_ae_measurable hf
 
 @[measurability]
 lemma measurable_ennnorm : measurable (λ x : α, (nnnorm x : ℝ≥0∞)) :=
-measurable_nnnorm.ennreal_coe
+measurable_nnnorm.coe_nnreal_ennreal
 
 @[measurability]
 lemma measurable.ennnorm {f : β → α} (hf : measurable f) :
   measurable (λ a, (nnnorm (f a) : ℝ≥0∞)) :=
-hf.nnnorm.ennreal_coe
+hf.nnnorm.coe_nnreal_ennreal
 
 @[measurability]
 lemma ae_measurable.ennnorm {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
@@ -1258,12 +1332,12 @@ lemma measurable_of_tendsto_nnreal' {ι ι'} {f : ι → α → ℝ≥0} {g : α
   [ne_bot u] (hf : ∀ i, measurable (f i)) (lim : tendsto f u (𝓝 g)) {p : ι' → Prop}
   {s : ι' → set ι} (hu : u.has_countable_basis p s) (hs : ∀ i, (s i).countable) : measurable g :=
 begin
-  rw [tendsto_pi] at lim, rw [← measurable_ennreal_coe_iff],
+  rw [tendsto_pi] at lim, rw [← measurable_coe_nnreal_ennreal_iff],
   have : ∀ x, liminf u (λ n, (f n x : ℝ≥0∞)) = (g x : ℝ≥0∞) :=
   λ x, ((ennreal.continuous_coe.tendsto (g x)).comp (lim x)).liminf_eq,
   simp_rw [← this],
   show measurable (λ x, liminf u (λ n, (f n x : ℝ≥0∞))),
-  exact measurable_liminf' (λ i, (hf i).ennreal_coe) hu hs,
+  exact measurable_liminf' (λ i, (hf i).coe_nnreal_ennreal) hu hs,
 end
 
 /-- A sequential limit of measurable `ℝ≥0` valued functions is measurable. -/

src/measure_theory/integration.lean

@@ -1912,7 +1912,7 @@ begin
         = ∫⁻ x, ∑' n, (((s n).indicator (λ x, ρ n) x : ℝ≥0) : ℝ≥0∞) ∂μ :
       by { apply lintegral_congr (λ x, _), simp_rw [g, ennreal.coe_tsum (B x)] }
     ... = ∑' n, ∫⁻ x, (((s n).indicator (λ x, ρ n) x : ℝ≥0) : ℝ≥0∞) ∂μ :
-      lintegral_tsum (λ n, (M n).ennreal_coe)
+      lintegral_tsum (λ n, (M n).coe_nnreal_ennreal)
     ... = ∑' n, μ (s n) * ρ n :
       by simp only [measurable_spanning_sets μ, lintegral_const, measurable_set.univ, mul_comm,
                     lintegral_indicator, univ_inter, coe_indicator, measure.restrict_apply]

src/measure_theory/l1_space.lean

@@ -540,6 +540,17 @@ lemma lipschitz_with.integrable_comp_iff_of_antilipschitz [complete_space β] [b
   integrable (g ∘ f) μ ↔ integrable f μ :=
 by simp [← mem_ℒp_one_iff_integrable, hg.mem_ℒp_comp_iff_of_antilipschitz hg' g0]
 
+lemma integrable.real_to_nnreal {f : α → ℝ} (hf : integrable f μ) :
+  integrable (λ x, ((f x).to_nnreal : ℝ)) μ :=
+begin
+  refine ⟨hf.ae_measurable.real_to_nnreal.coe_nnreal_real, _⟩,
+  rw has_finite_integral_iff_norm,
+  refine lt_of_le_of_lt _ ((has_finite_integral_iff_norm _).1 hf.has_finite_integral),
+  apply lintegral_mono,
+  assume x,
+  simp [real.norm_eq_abs, ennreal.of_real_le_of_real, abs_le, abs_nonneg, le_abs_self],
+end
+
 section pos_part
 /-! ### Lemmas used for defining the positive part of a `L¹` function -/