feat(measure_theory/measurable_space): define measurable_embedding (#…

…10023)

This way we can generalize our theorems about `measurable_equiv` and `closed_embedding`s.

src/data/set/function.lean

@@ -87,6 +87,23 @@ by convert restrict_dite _ _
   restrict (extend f g g') (range f)ᶜ = g' ∘ coe :=
 by convert restrict_dite_compl _ _
 
+lemma range_extend_subset (f : α → β) (g : α → γ) (g' : β → γ) :
+  range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ :=
+begin
+  classical,
+  rintro _ ⟨y, rfl⟩,
+  rw extend_def, split_ifs,
+  exacts [or.inl (mem_range_self _), or.inr (mem_image_of_mem _ h)]
+end
+
+lemma range_extend {f : α → β} (hf : injective f) (g : α → γ) (g' : β → γ) :
+  range (extend f g g') = range g ∪ g' '' (range f)ᶜ :=
+begin
+  refine (range_extend_subset _ _ _).antisymm _,
+  rintro z (⟨x, rfl⟩|⟨y, hy, rfl⟩),
+  exacts [⟨f x, extend_apply hf _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
+end
+
 /-- Restrict codomain of a function `f` to a set `s`. Same as `subtype.coind` but this version
 has codomain `↥s` instead of `subtype s`. -/
 def cod_restrict (f : α → β) (s : set β) (h : ∀ x, f x ∈ s) : α → s :=

src/measure_theory/constructions/borel_space.lean

@@ -810,57 +810,18 @@ instance prod.borel_space [second_countable_topology α] [second_countable_topol
   borel_space (α × β) :=
 ⟨le_antisymm prod_le_borel_prod opens_measurable_space.borel_le⟩
 
-lemma closed_embedding.measurable_inv_fun [n : nonempty β] {g : β → γ} (hg : closed_embedding g) :
-  measurable (function.inv_fun g) :=
-begin
-  refine measurable_of_is_closed (λ s hs, _),
-  by_cases h : classical.choice n ∈ s,
-  { rw preimage_inv_fun_of_mem hg.to_embedding.inj h,
-    exact (hg.closed_iff_image_closed.mp hs).measurable_set.union
-      hg.closed_range.measurable_set.compl },
-  { rw preimage_inv_fun_of_not_mem hg.to_embedding.inj h,
-    exact (hg.closed_iff_image_closed.mp hs).measurable_set }
-end
-
-lemma measurable_comp_iff_of_closed_embedding {f : δ → β} (g : β → γ) (hg : closed_embedding g) :
-  measurable (g ∘ f) ↔ measurable f :=
-begin
-  refine ⟨λ hf, _, λ hf, hg.measurable.comp hf⟩,
-  apply measurable_of_is_closed, intros s hs,
-  convert hf (hg.is_closed_map s hs).measurable_set,
-  rw [@preimage_comp _ _ _ f g, preimage_image_eq _ hg.to_embedding.inj]
-end
+protected lemma embedding.measurable_embedding {f : α → β} (h₁ : embedding f)
+  (h₂ : measurable_set (range f)) : measurable_embedding f :=
+show measurable_embedding (coe ∘ (homeomorph.of_embedding f h₁).to_measurable_equiv),
+from (measurable_embedding.subtype_coe h₂).comp (measurable_equiv.measurable_embedding _)
 
-lemma ae_measurable_comp_iff_of_closed_embedding {f : δ → β} {μ : measure δ}
-  (g : β → γ) (hg : closed_embedding g) : ae_measurable (g ∘ f) μ ↔ ae_measurable f μ :=
-begin
-  casesI is_empty_or_nonempty β,
-  { haveI := function.is_empty f,
-    simp only [(measurable_of_empty (g ∘ f)).ae_measurable,
-      (measurable_of_empty f).ae_measurable] },
-  { refine ⟨λ hf, _, λ hf, hg.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 },
-end
+protected lemma closed_embedding.measurable_embedding {f : α → β} (h : closed_embedding f) :
+  measurable_embedding f :=
+h.to_embedding.measurable_embedding h.closed_range.measurable_set
 
-lemma ae_measurable_comp_right_iff_of_closed_embedding {g : α → β} {μ : measure α}
-  {f : β → δ} (hg : closed_embedding g) :
-  ae_measurable (f ∘ g) μ ↔ ae_measurable f (measure.map g μ) :=
-begin
-  refine ⟨λ h, _, λ h, h.comp_measurable hg.measurable⟩,
-  casesI is_empty_or_nonempty α, { simp [μ.eq_zero_of_is_empty] },
-  refine ⟨(h.mk _) ∘ (function.inv_fun g), h.measurable_mk.comp hg.measurable_inv_fun, _⟩,
-  have : μ = measure.map (function.inv_fun g) (measure.map g μ),
-    by rw [measure.map_map hg.measurable_inv_fun hg.measurable,
-           (function.left_inverse_inv_fun hg.to_embedding.inj).comp_eq_id, measure.map_id],
-  rw this at h,
-  filter_upwards [ae_of_ae_map hg.measurable_inv_fun h.ae_eq_mk,
-    ae_map_mem_range g hg.closed_range.measurable_set μ],
-  assume x hx₁ hx₂,
-  convert hx₁,
-  exact ((function.left_inverse_inv_fun hg.to_embedding.inj).right_inv_on_range hx₂).symm,
-end
+protected lemma open_embedding.measurable_embedding {f : α → β} (h : open_embedding f) :
+  measurable_embedding f :=
+h.to_embedding.measurable_embedding h.open_range.measurable_set
 
 section linear_order
 
@@ -1855,10 +1816,10 @@ variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [measurable_space E
 
 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)
+(closed_embedding_smul_left hc).measurable_embedding.measurable_comp_iff
 
 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)
+(closed_embedding_smul_left hc).measurable_embedding.ae_measurable_comp_iff
 
 end normed_space

src/measure_theory/function/l1_space.lean

@@ -457,9 +457,14 @@ lemma integrable_map_measure [opens_measurable_space β] {f : α → δ} {g : δ
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
 by simp [integrable, hg, hg.comp_measurable hf, has_finite_integral, lintegral_map' hg.ennnorm hf]
 
+lemma _root_.measurable_embedding.integrable_map_iff {f : α → δ} (hf : measurable_embedding f)
+  {g : δ → β} :
+  integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
+by simp only [integrable, hf.ae_measurable_map_iff, has_finite_integral, hf.lintegral_map]
+
 lemma integrable_map_equiv (f : α ≃ᵐ δ) (g : δ → β) :
   integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ :=
-by simp only [integrable, ae_measurable_map_equiv_iff, has_finite_integral, lintegral_map_equiv]
+f.measurable_embedding.integrable_map_iff
 
 lemma lintegral_edist_lt_top [second_countable_topology β] [opens_measurable_space β] {f g : α → β}
   (hf : integrable f μ) (hg : integrable g μ) :

src/measure_theory/function/lp_space.lean

@@ -1730,11 +1730,11 @@ lemma measure_theory.mem_ℒp.of_comp_antilipschitz_with {α E F} {K'}
   (hg : uniform_continuous g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) : mem_ℒp f p μ :=
 begin
   have : ∀ᵐ x ∂μ, ∥f x∥ ≤ K' * ∥g (f x)∥,
-    { apply filter.eventually_of_forall (λ x, _),
-      rw [← dist_zero_right, ← dist_zero_right, ← g0],
-      apply hg'.le_mul_dist },
-  exact hL.of_le_mul ((ae_measurable_comp_iff_of_closed_embedding g
-    (hg'.closed_embedding hg)).1 hL.1) this,
+  { apply filter.eventually_of_forall (λ x, _),
+    rw [← dist_zero_right, ← dist_zero_right, ← g0],
+    apply hg'.le_mul_dist },
+  exact hL.of_le_mul ((hg'.closed_embedding hg).measurable_embedding.ae_measurable_comp_iff.1
+    hL.1) this,
 end
 
 namespace lipschitz_with

src/measure_theory/integral/bochner.lean

@@ -1286,25 +1286,25 @@ let g := hfm.mk f in calc
 ... = ∫ x, g (φ x) ∂μ : integral_map_of_measurable hφ hfm.measurable_mk
 ... = ∫ x, f (φ x) ∂μ : integral_congr_ae $ ae_eq_comp hφ (hfm.ae_eq_mk).symm
 
-lemma integral_map_of_closed_embedding {β} [topological_space α] [borel_space α]
+lemma _root_.measurable_embedding.integral_map {β} {_ : measurable_space β} {f : α → β}
+  (hf : measurable_embedding f) (g : β → E) :
+  ∫ y, g y ∂(measure.map f μ) = ∫ x, g (f x) ∂μ :=
+begin
+  by_cases hgm : ae_measurable g (measure.map f μ),
+  { exact integral_map hf.measurable hgm },
+  { rw [integral_non_ae_measurable hgm, integral_non_ae_measurable],
+    rwa ← hf.ae_measurable_map_iff }
+end
+
+lemma _root_.closed_embedding.integral_map {β} [topological_space α] [borel_space α]
   [topological_space β] [measurable_space β] [borel_space β]
   {φ : α → β} (hφ : closed_embedding φ) (f : β → E) :
   ∫ y, f y ∂(measure.map φ μ) = ∫ x, f (φ x) ∂μ :=
-begin
-  by_cases hfm : ae_measurable f (measure.map φ μ),
-  { exact integral_map hφ.continuous.measurable hfm },
-  { rw [integral_non_ae_measurable hfm, integral_non_ae_measurable],
-    rwa ae_measurable_comp_right_iff_of_closed_embedding hφ }
-end
+hφ.measurable_embedding.integral_map _
 
 lemma integral_map_equiv {β} [measurable_space β] (e : α ≃ᵐ β) (f : β → E) :
   ∫ y, f y ∂(measure.map e μ) = ∫ x, f (e x) ∂μ :=
-begin
-  by_cases hfm : ae_measurable f (measure.map e μ),
-  { exact integral_map e.measurable hfm },
-  { rw [integral_non_ae_measurable hfm, integral_non_ae_measurable],
-    rwa ← ae_measurable_map_equiv_iff }
-end
+e.measurable_embedding.integral_map f
 
 @[simp] lemma integral_dirac' [measurable_space α] (f : α → E) (a : α) (hfm : measurable f) :
   ∫ x, f x ∂(measure.dirac a) = f a :=
@@ -1338,7 +1338,7 @@ begin
   { rw ← map_mul_left_eq_self at hμ,
     exact hμ g },
   have h_mul : closed_embedding (λ x, g * x) := (homeomorph.mul_left g).closed_embedding,
-  rw [← integral_map_of_closed_embedding h_mul, hgμ],
+  rw [← h_mul.integral_map, hgμ],
   apply_instance,
 end
 
@@ -1352,7 +1352,7 @@ begin
   { rw ← map_mul_right_eq_self at hμ,
     exact hμ g },
   have h_mul : closed_embedding (λ x, x * g) := (homeomorph.mul_right g).closed_embedding,
-  rw [← integral_map_of_closed_embedding h_mul, hgμ],
+  rw [← h_mul.integral_map, hgμ],
   apply_instance,
 end
 

src/measure_theory/integral/integrable_on.lean

@@ -171,6 +171,11 @@ by { delta integrable_on, rw measure.restrict_add, exact hμ.integrable.add_meas
   h.mono_measure (measure.le_add_left (le_refl _))⟩,
   λ h, h.1.add_measure h.2⟩
 
+lemma _root_.measurable_embedding.integrable_on_map_iff [measurable_space β] {e : α → β}
+  (he : measurable_embedding e) {f : β → E} {μ : measure α} {s : set β} :
+  integrable_on f s (measure.map e μ) ↔ integrable_on (f ∘ e) (e ⁻¹' s) μ :=
+by simp only [integrable_on, he.restrict_map, he.integrable_map_iff]
+
 lemma integrable_on_map_equiv [measurable_space β] (e : α ≃ᵐ β) {f : β → E} {μ : measure α}
   {s : set β} :
   integrable_on f s (measure.map e μ) ↔ integrable_on (f ∘ e) (e ⁻¹' s) μ :=

src/measure_theory/integral/interval_integral.lean

@@ -576,14 +576,14 @@ variables {a b c d : ℝ} (f : ℝ → E)
 @[simp] lemma integral_comp_mul_right (hc : c ≠ 0) :
   ∫ x in a..b, f (x * c) = c⁻¹ • ∫ x in a*c..b*c, f x :=
 begin
-  have A : closed_embedding (λ x, x * c) := (homeomorph.mul_right₀ c hc).closed_embedding,
+  have A : measurable_embedding (λ x, x * c) :=
+    (homeomorph.mul_right₀ c hc).closed_embedding.measurable_embedding,
   conv_rhs { rw [← real.smul_map_volume_mul_right hc] },
-  simp_rw [integral_smul_measure, interval_integral,
-          set_integral_map_of_closed_embedding measurable_set_Ioc A,
+  simp_rw [integral_smul_measure, interval_integral, A.set_integral_map,
           ennreal.to_real_of_real (abs_nonneg c)],
-  cases lt_or_gt_of_ne hc,
+  cases hc.lt_or_lt,
   { simp [h, mul_div_cancel, hc, abs_of_neg, restrict_congr_set Ico_ae_eq_Ioc] },
-  { simp [(show 0 < c, from h), mul_div_cancel, hc, abs_of_pos] }
+  { simp [h, mul_div_cancel, hc, abs_of_pos] }
 end
 
 @[simp] lemma smul_integral_comp_mul_right (c) :
@@ -608,10 +608,11 @@ by by_cases hc : c = 0; simp [hc]
 
 @[simp] lemma integral_comp_add_right (d) :
   ∫ x in a..b, f (x + d) = ∫ x in a+d..b+d, f x :=
-have A : closed_embedding (λ x, x + d) := (homeomorph.add_right d).closed_embedding,
+have A : measurable_embedding (λ x, x + d) :=
+  (homeomorph.add_right d).closed_embedding.measurable_embedding,
 calc  ∫ x in a..b, f (x + d)
     = ∫ x in a+d..b+d, f x ∂(measure.map (λ x, x + d) volume)
-                           : by simp [interval_integral, set_integral_map_of_closed_embedding _ A]
+                           : by simp [interval_integral, A.set_integral_map]
 ... = ∫ x in a+d..b+d, f x : by rw [real.map_volume_add_right]
 
 @[simp] lemma integral_comp_add_left (d) :

src/measure_theory/integral/lebesgue.lean

@@ -262,6 +262,31 @@ lemma range_comp_subset_range [measurable_space β] (f : β →ₛ γ) {g : α 
   (f.comp g hgm).range ⊆ f.range :=
 finset.coe_subset.1 $ by simp only [coe_range, coe_comp, set.range_comp_subset_range]
 
+/-- Extend a `simple_func` along a measurable embedding: `f₁.extend g hg f₂` is the function
+`F : β →ₛ γ` such that `F ∘ g = f₁` and `F y = f₂ y` whenever `y ∉ range g`. -/
+def extend [measurable_space β] (f₁ : α →ₛ γ) (g : α → β)
+  (hg : measurable_embedding g) (f₂ : β →ₛ γ) : β →ₛ γ :=
+{ to_fun := function.extend g f₁ f₂,
+  finite_range' := (f₁.finite_range.union $ f₂.finite_range.subset
+    (image_subset_range _ _)).subset (range_extend_subset _ _ _),
+  measurable_set_fiber' :=
+    begin
+      letI : measurable_space γ := ⊤, haveI : measurable_singleton_class γ := ⟨λ _, trivial⟩,
+      exact λ x, hg.measurable_extend f₁.measurable f₂.measurable (measurable_set_singleton _)
+    end }
+
+@[simp] lemma extend_apply [measurable_space β] (f₁ : α →ₛ γ) {g : α → β}
+  (hg : measurable_embedding g) (f₂ : β →ₛ γ) (x : α) : (f₁.extend g hg f₂) (g x) = f₁ x :=
+function.extend_apply hg.injective _ _ _
+
+@[simp] lemma extend_comp_eq' [measurable_space β] (f₁ : α →ₛ γ) {g : α → β}
+  (hg : measurable_embedding g) (f₂ : β →ₛ γ) : (f₁.extend g hg f₂) ∘ g = f₁ :=
+funext $ λ x, extend_apply _ _ _ _
+
+@[simp] lemma extend_comp_eq [measurable_space β] (f₁ : α →ₛ γ) {g : α → β}
+  (hg : measurable_embedding g) (f₂ : β →ₛ γ) : (f₁.extend g hg f₂).comp g hg.measurable = f₁ :=
+coe_injective $ extend_comp_eq' _ _ _
+
 /-- If `f` is a simple function taking values in `β → γ` and `g` is another simple function
 with the same domain and codomain `β`, then `f.seq g = f a (g a)`. -/
 def seq (f : α →ₛ (β → γ)) (g : α →ₛ β) : α →ₛ γ := f.bind (λf, g.map f)
@@ -787,32 +812,15 @@ lemma lintegral_congr {f g : α →ₛ ℝ≥0∞} (h : f =ᵐ[μ] g) :
 lintegral_eq_of_measure_preimage $ λ y, measure_congr $
   eventually.set_eq $ h.mono $ λ x hx, by simp [hx]
 
-lemma lintegral_map {β} [measurable_space β] {μ' : measure β} (f : α →ₛ ℝ≥0∞) (g : β →ₛ ℝ≥0∞)
+lemma lintegral_map' {β} [measurable_space β] {μ' : measure β} (f : α →ₛ ℝ≥0∞) (g : β →ₛ ℝ≥0∞)
   (m' : α → β) (eq : ∀ a, f a = g (m' a)) (h : ∀s, measurable_set s → μ' s = μ (m' ⁻¹' s)) :
   f.lintegral μ = g.lintegral μ' :=
 lintegral_eq_of_measure_preimage $ λ y,
 by { simp only [preimage, eq], exact (h (g ⁻¹' {y}) (g.measurable_set_preimage _)).symm }
 
-/-- The `lintegral` of simple functions transforms appropriately under a measurable equivalence.
-(Compare `lintegral_map`, which applies to a broader class of transformations of the domain, but
-requires measurability of the function being integrated.) -/
-lemma lintegral_map_equiv {β} [measurable_space β] (g : β →ₛ ℝ≥0∞) (m' : α ≃ᵐ β) :
-  (g.comp m' m'.measurable).lintegral μ = g.lintegral (measure.map m' μ) :=
-begin
-  simp [simple_func.lintegral],
-  have : (g.comp m' m'.measurable).range = g.range,
-  { refine le_antisymm _ _,
-    { exact g.range_comp_subset_range m'.measurable },
-    convert (g.comp m' m'.measurable).range_comp_subset_range m'.symm.measurable,
-    apply simple_func.ext,
-    intros a,
-    exact congr_arg g (congr_fun m'.self_comp_symm.symm a) },
-  rw this,
-  congr' 1,
-  funext,
-  rw [m'.map_apply (g ⁻¹' {x})],
-  refl,
-end
+lemma lintegral_map {β} [measurable_space β] (g : β →ₛ ℝ≥0∞) {f : α → β} (hf : measurable f) :
+  g.lintegral (measure.map f μ) = (g.comp f hf).lintegral μ :=
+eq.symm $ lintegral_map' _ _ f (λ a, rfl) (λ s hs, measure.map_apply hf hs)
 
 end measure
 
@@ -1864,10 +1872,9 @@ lemma lintegral_map [measurable_space β] {f : β → ℝ≥0∞} {g : α → β
   (hf : measurable f) (hg : measurable g) : ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ :=
 begin
   simp only [lintegral_eq_supr_eapprox_lintegral, hf, hf.comp hg],
-  { congr, funext n, symmetry,
-    apply simple_func.lintegral_map,
-    { assume a, exact congr_fun (simple_func.eapprox_comp hf hg) a },
-    { assume s hs, exact map_apply hg hs } },
+  congr' with n : 1,
+  convert simple_func.lintegral_map _ hg,
+  ext1 x, simp only [eapprox_comp hf hg, coe_comp]
 end
 
 lemma lintegral_map' [measurable_space β] {f : β → ℝ≥0∞} {g : α → β}
@@ -1887,35 +1894,29 @@ lemma set_lintegral_map [measurable_space β] {f : β → ℝ≥0∞} {g : α 
   ∫⁻ y in s, f y ∂(map g μ) = ∫⁻ x in g ⁻¹' s, f (g x) ∂μ :=
 by rw [restrict_map hg hs, lintegral_map hf hg]
 
+/-- If `g : α → β` is a measurable embedding and `f : β → ℝ≥0∞` is any function (not necessarily
+measurable), then `∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ`. Compare with `lintegral_map` wich
+applies to any measurable `g : α → β` but requires that `f` is measurable as well. -/
+lemma _root_.measurable_embedding.lintegral_map [measurable_space β] {g : α → β}
+  (hg : measurable_embedding g) (f : β → ℝ≥0∞) :
+  ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ :=
+begin
+  refine le_antisymm (bsupr_le $ λ f₀ hf₀, _) (bsupr_le $ λ f₀ hf₀, _),
+  { rw [simple_func.lintegral_map _ hg.measurable, lintegral],
+    have : (f₀.comp g hg.measurable : α → ℝ≥0∞) ≤ f ∘ g, from λ x, hf₀ (g x),
+    exact le_supr_of_le (comp f₀ g hg.measurable) (le_supr _ this) },
+  { rw [← f₀.extend_comp_eq hg (const _ 0), ← simple_func.lintegral_map,
+      ← simple_func.lintegral_eq_lintegral],
+    refine lintegral_mono_ae (hg.ae_map_iff.2 $ eventually_of_forall $ λ x, _),
+    exact (extend_apply _ _ _ _).trans_le (hf₀ _) }
+end
+
 /-- The `lintegral` transforms appropriately under a measurable equivalence `g : α ≃ᵐ β`.
 (Compare `lintegral_map`, which applies to a wider class of functions `g : α → β`, but requires
 measurability of the function being integrated.) -/
 lemma lintegral_map_equiv [measurable_space β] (f : β → ℝ≥0∞) (g : α ≃ᵐ β) :
   ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ :=
-begin
-  refine le_antisymm _ _,
-  { refine supr_le_supr2 _,
-    intros f₀,
-    use f₀.comp g g.measurable,
-    refine supr_le_supr2 _,
-    intros hf₀,
-    use λ x, hf₀ (g x),
-    exact (lintegral_map_equiv f₀ g).symm.le },
-  { refine supr_le_supr2 _,
-    intros f₀,
-    use f₀.comp g.symm g.symm.measurable,
-    refine supr_le_supr2 _,
-    intros hf₀,
-    have : (λ a, (f₀.comp (g.symm) g.symm.measurable) a) ≤ λ (a : β), f a,
-    { convert λ x, hf₀ (g.symm x),
-      funext,
-      simp [congr_arg f (congr_fun g.self_comp_symm a)] },
-    use this,
-    convert (lintegral_map_equiv (f₀.comp g.symm g.symm.measurable) g).le,
-    apply simple_func.ext,
-    intros a,
-    convert congr_arg f₀ (congr_fun g.symm_comp_self a).symm using 1 }
-end
+g.measurable_embedding.lintegral_map f 
 
 section dirac_and_count
 variable [measurable_space α]