feat(measure_theory): almost everywhere measurable functions (#5568)

This PR introduces a notion of almost everywhere measurable function, i.e., a function which coincides almost everywhere with a measurable function, and builds a basic API around the notion. It will then be used in #5510 to extend the Bochner integral. The main new definition in the PR is `h : ae_measurable f μ`. It comes with `h.mk f` building a measurable function that coincides almost everywhere with `f` (these assertions are respectively `h.measurable_mk` and `h.ae_eq_mk`).

Author: sgouezel

src/analysis/special_functions/pow.lean

@@ -1493,4 +1493,9 @@ lemma measurable.ennreal_rpow_const {α} [measurable_space α] {f : α → ennre
   measurable (λ a : α, (f a) ^ y) :=
 hf.ennreal_rpow measurable_const
 
+lemma ae_measurable.ennreal_rpow_const {α} [measurable_space α] {f : α → ennreal}
+  {μ : 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

src/measure_theory/borel_space.lean

@@ -30,12 +30,13 @@ import topology.G_delta
   is continuous, then `λ x, op (f x, g y)` is measurable;
 * `measurable.add` etc : dot notation for arithmetic operations on `measurable` predicates,
   and similarly for `dist` and `edist`;
+* `ae_measurable.add` : similar dot notation for almost everywhere measurable functions;
 * `measurable.ennreal*` : special cases for arithmetic operations on `ennreal`s.
 -/
 
 noncomputable theory
 
-open classical set filter
+open classical set filter measure_theory
 open_locale classical big_operators topological_space nnreal
 
 universes u v w x y
@@ -352,10 +353,20 @@ lemma measurable.max {f g : δ → α} (hf : measurable f) (hg : measurable g) :
   measurable (λ a, max (f a) (g a)) :=
 hf.piecewise (is_measurable_le hg hf) hg
 
+lemma ae_measurable.max {f g : δ → α} {μ : measure δ}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, max (f a) (g a)) μ :=
+⟨λ a, max (hf.mk f a) (hg.mk g a), hf.measurable_mk.max hg.measurable_mk,
+  eventually_eq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩
+
 lemma measurable.min {f g : δ → α} (hf : measurable f) (hg : measurable g) :
   measurable (λ a, min (f a) (g a)) :=
 hf.piecewise (is_measurable_le hf hg) hg
 
+lemma ae_measurable.min {f g : δ → α} {μ : measure δ}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, min (f a) (g a)) μ :=
+⟨λ a, min (hf.mk f a) (hg.mk g a), hf.measurable_mk.min hg.measurable_mk,
+  eventually_eq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩
+
 end linear_order
 
 /-- A continuous function from an `opens_measurable_space` to a `borel_space`
@@ -385,20 +396,40 @@ lemma continuous.measurable2 [second_countable_topology α] [second_countable_to
   measurable (λ a, c (f a) (g a)) :=
 h.measurable.comp (hf.prod_mk hg)
 
+lemma continuous.ae_measurable2 [second_countable_topology α] [second_countable_topology β]
+  {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : measure δ}
+  (h : continuous (λ p : α × β, c p.1 p.2)) (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (λ a, c (f a) (g a)) μ :=
+h.measurable.comp_ae_measurable (hf.prod_mk hg)
+
 lemma measurable.smul [semiring α] [second_countable_topology α]
   [add_comm_monoid γ] [second_countable_topology γ]
   [semimodule α γ] [topological_semimodule α γ]
   {f : δ → α} {g : δ → γ} (hf : measurable f) (hg : measurable g) :
   measurable (λ c, f c • g c) :=
 continuous_smul.measurable2 hf hg
 
+lemma ae_measurable.smul [semiring α] [second_countable_topology α]
+  [add_comm_monoid γ] [second_countable_topology γ]
+  [semimodule α γ] [topological_semimodule α γ]
+  {f : δ → α} {g : δ → γ} {μ : measure δ} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (λ c, f c • g c) μ :=
+continuous_smul.ae_measurable2 hf hg
+
 lemma measurable.const_smul {R M : Type*} [topological_space R] [semiring R]
   [add_comm_monoid M] [semimodule R M] [topological_space M] [topological_semimodule R M]
   [measurable_space M] [borel_space M]
   {f : δ → M} (hf : measurable f) (c : R) :
   measurable (λ x, c • f x) :=
 (continuous_const.smul continuous_id).measurable.comp hf
 
+lemma ae_measurable.const_smul {R M : Type*} [topological_space R] [semiring R]
+  [add_comm_monoid M] [semimodule R M] [topological_space M] [topological_semimodule R M]
+  [measurable_space M] [borel_space M]
+  {f : δ → M} {μ : measure δ} (hf : ae_measurable f μ) (c : R) :
+  ae_measurable (λ x, c • f x) μ :=
+(continuous_const.smul continuous_id).measurable.comp_ae_measurable hf
+
 lemma measurable_const_smul_iff {α : Type*} [topological_space α]
   [division_ring α] [add_comm_monoid γ]
   [semimodule α γ] [topological_semimodule α γ]
@@ -407,6 +438,14 @@ lemma measurable_const_smul_iff {α : Type*} [topological_space α]
 ⟨λ h, by simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.const_smul c⁻¹,
   λ h, h.const_smul c⟩
 
+lemma ae_measurable_const_smul_iff {α : Type*} [topological_space α]
+  [division_ring α] [add_comm_monoid γ]
+  [semimodule α γ] [topological_semimodule α γ]
+  {f : δ → γ} {μ : measure δ} {c : α} (hc : c ≠ 0) :
+  ae_measurable (λ x, c • f x) μ ↔ ae_measurable f μ :=
+⟨λ h, by simpa only [smul_smul, inv_mul_cancel hc, one_smul] using h.const_smul c⁻¹,
+  λ h, h.const_smul c⟩
+
 lemma measurable.const_mul {R : Type*} [topological_space R] [measurable_space R]
   [borel_space R] [semiring R] [topological_semiring R]
   {f : δ → R} (hf : measurable f) (c : R) :
@@ -466,6 +505,12 @@ lemma measurable.mul [has_mul α] [has_continuous_mul α] [second_countable_topo
   {f : δ → α} {g : δ → α} : measurable f → measurable g → measurable (λ a, f a * g a) :=
 (@continuous_mul α _ _ _).measurable2
 
+@[to_additive]
+lemma ae_measurable.mul [has_mul α] [has_continuous_mul α] [second_countable_topology α]
+  {f : δ → α} {g : δ → α} {μ : measure δ}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, f a * g a) μ :=
+(@continuous_mul α _ _ _).ae_measurable2 hf hg
+
 /-- A variant of `measurable.mul` that uses `*` on functions -/
 @[to_additive]
 lemma measurable.mul' [has_mul α] [has_continuous_mul α] [second_countable_topology α]
@@ -499,6 +544,11 @@ lemma measurable.inv [group α] [topological_group α] {f : δ → α} (hf : mea
   measurable (λ a, (f a)⁻¹) :=
 measurable_inv.comp hf
 
+@[to_additive]
+lemma ae_measurable.inv [group α] [topological_group α] {f : δ → α} {μ : measure δ}
+  (hf : ae_measurable f μ) : ae_measurable (λ a, (f a)⁻¹) μ :=
+measurable_inv.comp_ae_measurable hf
+
 lemma measurable_inv' {α : Type*} [normed_field α] [measurable_space α] [borel_space α] :
   measurable (has_inv.inv : α → α) :=
 measurable_of_continuous_on_compl_singleton 0 continuous_on_inv'
@@ -523,6 +573,11 @@ lemma measurable.sub [add_group α] [topological_add_group α] [second_countable
   measurable (λ x, f x - g x) :=
 by simpa only [sub_eq_add_neg] using hf.add hg.neg
 
+lemma ae_measurable.sub [add_group α] [topological_add_group α] [second_countable_topology α]
+  {f g : δ → α} {μ : measure δ}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ x, f x - g x) μ :=
+by simpa only [sub_eq_add_neg] using hf.add hg.neg
+
 lemma closed_embedding.measurable_inv_fun [n : nonempty β] {g : β → γ} (hg : closed_embedding g) :
   measurable (function.inv_fun g) :=
 begin
@@ -544,6 +599,20 @@ begin
   rw [@preimage_comp _ _ _ f g, preimage_image_eq _ hg.to_embedding.inj]
 end
 
+lemma ae_measurable_comp_iff_of_closed_embedding {f : δ → β} {μ : measure δ}
+  (g : β → γ) (hg : closed_embedding g) : ae_measurable (g ∘ f) μ ↔ ae_measurable f μ :=
+begin
+  by_cases h : nonempty β,
+  { resetI,
+    refine ⟨λ hf, _, λ hf, hg.continuous.measurable.comp_ae_measurable hf⟩,
+    convert hg.measurable_inv_fun.comp_ae_measurable hf,
+    ext x,
+    exact (function.left_inverse_inv_fun hg.to_embedding.inj (f x)).symm },
+  { have H : ¬ nonempty δ, by { contrapose! h, exact nonempty.map f h },
+    simp [(measurable_of_not_nonempty H (g ∘ f)).ae_measurable,
+          (measurable_of_not_nonempty H f).ae_measurable] }
+end
+
 section linear_order
 
 variables [linear_order α] [order_topology α] [second_countable_topology α]
@@ -795,6 +864,10 @@ lemma measurable.edist {f g : β → α} (hf : measurable f) (hg : measurable g)
   measurable (λ b, edist (f b) (g b)) :=
 (@continuous_edist α _).measurable2 hf hg
 
+lemma ae_measurable.edist {f g : β → α} {μ : measure β}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, edist (f a) (g a)) μ :=
+(@continuous_edist α _).ae_measurable2 hf hg
+
 end emetric_space
 
 namespace real
@@ -872,6 +945,10 @@ lemma measurable.ennreal_coe {f : α → ℝ≥0} (hf : measurable f) :
   measurable (λ x, (f x : ennreal)) :=
 ennreal.continuous_coe.measurable.comp hf
 
+lemma ae_measurable.ennreal_coe {f : α → ℝ≥0} {μ : measure α} (hf :  ae_measurable f μ) :
+  ae_measurable (λ x, (f x : ennreal)) μ :=
+ennreal.continuous_coe.measurable.comp_ae_measurable hf
+
 lemma measurable.ennreal_of_real {f : α → ℝ} (hf : measurable f) :
   measurable (λ x, ennreal.of_real (f x)) :=
 ennreal.continuous_of_real.measurable.comp hf
@@ -952,13 +1029,17 @@ lemma measurable.to_real {f : α → ennreal} (hf : measurable f) :
   measurable (λ x, ennreal.to_real (f x)) :=
 ennreal.measurable_to_real.comp hf
 
+lemma ae_measurable.to_real {f : α → ennreal} {μ : measure α} (hf : ae_measurable f μ) :
+  ae_measurable (λ x, ennreal.to_real (f x)) μ :=
+ennreal.measurable_to_real.comp_ae_measurable hf
+
 lemma measurable.ennreal_mul {f g : α → ennreal} (hf : measurable f) (hg : measurable g) :
   measurable (λ a, f a * g a) :=
 ennreal.measurable_mul.comp (hf.prod_mk hg)
 
-lemma measurable.ennreal_add {f g : α → ennreal}
-  (hf : measurable f) (hg : measurable g) : measurable (λ a, f a + g a) :=
-hf.add hg
+lemma ae_measurable.ennreal_mul {f g : α → ennreal} {μ : measure α}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, f a * g a) μ :=
+ennreal.measurable_mul.comp_ae_measurable (hf.prod_mk hg)
 
 lemma measurable.ennreal_sub {f g : α → ennreal} (hf : measurable f) (hg : measurable g) :
   measurable (λ a, f a - g a) :=
@@ -979,19 +1060,31 @@ continuous_norm.measurable
 lemma measurable.norm {f : β → α} (hf : measurable f) : measurable (λ a, norm (f a)) :=
 measurable_norm.comp hf
 
+lemma ae_measurable.norm {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
+  ae_measurable (λ a, norm (f a)) μ :=
+measurable_norm.comp_ae_measurable hf
+
 lemma measurable_nnnorm : measurable (nnnorm : α → ℝ≥0) :=
 continuous_nnnorm.measurable
 
 lemma measurable.nnnorm {f : β → α} (hf : measurable f) : measurable (λ a, nnnorm (f a)) :=
 measurable_nnnorm.comp hf
 
+lemma ae_measurable.nnnorm {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
+  ae_measurable (λ a, nnnorm (f a)) μ :=
+measurable_nnnorm.comp_ae_measurable hf
+
 lemma measurable_ennnorm : measurable (λ x : α, (nnnorm x : ennreal)) :=
 measurable_nnnorm.ennreal_coe
 
 lemma measurable.ennnorm {f : β → α} (hf : measurable f) :
   measurable (λ a, (nnnorm (f a) : ennreal)) :=
 hf.nnnorm.ennreal_coe
 
+lemma ae_measurable.ennnorm {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
+  ae_measurable (λ a, (nnnorm (f a) : ennreal)) μ :=
+measurable_ennnorm.comp_ae_measurable hf
+
 end normed_group
 
 section limits
@@ -1071,6 +1164,10 @@ lemma measurable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
   measurable (λ x, f x • c) ↔ measurable f :=
 measurable_comp_iff_of_closed_embedding (λ y : 𝕜, y • c) (closed_embedding_smul_left hc)
 
+lemma ae_measurable_smul_const {f : α → 𝕜} {μ : measure α} {c : E} (hc : c ≠ 0) :
+  ae_measurable (λ x, f x • c) μ ↔ ae_measurable f μ :=
+ae_measurable_comp_iff_of_closed_embedding (λ y : 𝕜, y • c) (closed_embedding_smul_left hc)
+
 end normed_space
 
 namespace measure_theory

src/measure_theory/measurable_space.lean

@@ -539,6 +539,13 @@ hf.piecewise hs measurable_const
 @[to_additive]
 lemma measurable_one [has_one α] : measurable (1 : β → α) := @measurable_const _ _ _ _ 1
 
+lemma measurable_of_not_nonempty  (h : ¬ nonempty α) (f : α → β) : measurable f :=
+begin
+  assume s hs,
+  convert is_measurable.empty,
+  exact eq_empty_of_not_nonempty h _,
+end
+
 end measurable_functions
 
 section constructions