[Merged by Bors] - feat(measure_theory): some additions

src/measure_theory/borel_space.lean

@@ -40,7 +40,7 @@ open classical set filter measure_theory
 open_locale classical big_operators topological_space nnreal
 
 universes u v w x y
-variables {α β γ δ : Type*} {ι : Sort y} {s t u : set α}
+variables {α β γ γ₂ δ : Type*} {ι : Sort y} {s t u : set α}
 
 open measurable_space topological_space
 
@@ -170,6 +170,7 @@ section
 variables [topological_space α] [measurable_space α] [opens_measurable_space α]
    [topological_space β] [measurable_space β] [opens_measurable_space β]
    [topological_space γ] [measurable_space γ] [borel_space γ]
+   [topological_space γ₂] [measurable_space γ₂] [borel_space γ₂]
    [measurable_space δ]
 
 lemma is_open.is_measurable (h : is_open s) : is_measurable s :=
@@ -376,14 +377,24 @@ lemma continuous.measurable {f : α → γ} (hf : continuous f) :
 hf.borel_measurable.mono opens_measurable_space.borel_le
   (le_of_eq $ borel_space.measurable_eq)
 
+section homeomorph
+
 /-- A homeomorphism between two Borel spaces is a measurable equivalence.-/
-def homeomorph.to_measurable_equiv {α : Type*} {β : Type*} [topological_space α]
-  [measurable_space α] [borel_space α] [topological_space β] [measurable_space β]
-  [borel_space β] (h : α ≃ₜ β) : α ≃ᵐ β :=
+def homeomorph.to_measurable_equiv (h : γ ≃ₜ γ₂) : γ ≃ᵐ γ₂ :=
 { measurable_to_fun := h.continuous_to_fun.measurable,
   measurable_inv_fun := h.continuous_inv_fun.measurable,
   .. h }
 
+@[simp]
+lemma homeomorph.to_measurable_equiv_coe (h : γ ≃ₜ γ₂) : (h.to_measurable_equiv : γ → γ₂) = h :=
+rfl
+
+@[simp] lemma homeomorph.to_measurable_equiv_symm_coe (h : γ ≃ₜ γ₂) :
+  (h.to_measurable_equiv.symm : γ₂ → γ) = h.symm :=
+rfl
+
+end homeomorph
+
 lemma measurable_of_continuous_on_compl_singleton [t1_space α] {f : α → γ} (a : α)
   (hf : continuous_on f {x | x ≠ a}) :
   measurable f :=
@@ -1015,6 +1026,12 @@ lemma measurable_sub : measurable (λ p : ennreal × ennreal, p.1 - p.2) :=
 by apply measurable_of_measurable_nnreal_nnreal;
   simp [← ennreal.coe_sub, continuous_sub.measurable.ennreal_coe]
 
+lemma measurable_inv : measurable (has_inv.inv : ennreal → ennreal) :=
+ennreal.continuous_inv.measurable
+
+lemma measurable_div : measurable (λ p : ennreal × ennreal, p.1 / p.2) :=
+ennreal.measurable_mul.comp $ measurable_fst.prod_mk $ ennreal.measurable_inv.comp measurable_snd
+
 end ennreal
 
 lemma measurable.to_nnreal {f : α → ennreal} (hf : measurable f) :
@@ -1050,6 +1067,13 @@ lemma measurable.ennreal_tsum {ι} [encodable ι] {f : ι → α → ennreal} (h
   measurable (λ x, ∑' i, f i x) :=
 by { simp_rw [ennreal.tsum_eq_supr_sum], apply measurable_supr, exact λ s, s.measurable_sum h }
 
+lemma measurable.ennreal_inv {f : α → ennreal} (hf : measurable f) : measurable (λ a, (f a)⁻¹) :=
+ennreal.measurable_inv.comp hf
+
+lemma measurable.ennreal_div {f g : α → ennreal} (hf : measurable f) (hg : measurable g) :
+  measurable (λ a, f a / g a) :=
+ennreal.measurable_div.comp $ hf.prod_mk hg
+
 section normed_group
 
 variables [normed_group α] [opens_measurable_space α] [measurable_space β]

src/measure_theory/integration.lean

@@ -878,8 +878,14 @@ lintegral_mono
 @[simp] lemma lintegral_const (c : ennreal) : ∫⁻ a, c ∂μ = c * μ univ :=
 by rw [← simple_func.const_lintegral, ← simple_func.lintegral_eq_lintegral, simple_func.coe_const]
 
+@[simp] lemma lintegral_one : ∫⁻ a, (1 : ennreal) ∂μ = μ univ :=
+by rw [lintegral_const, one_mul]
+
+lemma set_lintegral_const (s : set α) (c : ennreal) : ∫⁻ a in s, c ∂μ = c * μ s :=
+by rw [lintegral_const, measure.restrict_apply_univ]
+
 lemma set_lintegral_one (s) : ∫⁻ a in s, 1 ∂μ = μ s :=
-by rw [lintegral_const, one_mul, measure.restrict_apply_univ]
+by rw [set_lintegral_const, one_mul]
 
 /-- `∫⁻ a in s, f a ∂μ` is defined as the supremum of integrals of simple functions
 `φ : α →ₛ ennreal` such that `φ ≤ f`. This lemma says that it suffices to take
@@ -1023,7 +1029,7 @@ end
 lemma lintegral_mono_ae {f g : α → ennreal} (h : ∀ᵐ a ∂μ, f a ≤ g a) :
   (∫⁻ a, f a ∂μ) ≤ (∫⁻ a, g a ∂μ) :=
 begin
-  rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, hts, ht, ht0⟩,
+  rcases exists_is_measurable_superset_of_null h with ⟨t, hts, ht, ht0⟩,
   have : ∀ᵐ x ∂μ, x ∉ t := measure_zero_iff_ae_nmem.1 ht0,
   refine (supr_le $ assume s, supr_le $ assume hfs,
     le_supr_of_le (s.restrict tᶜ) $ le_supr_of_le _ _),
@@ -1193,6 +1199,13 @@ lemma lintegral_mul_const' (r : ennreal) (f : α → ennreal) (hr : r ≠ ⊤):
   ∫⁻ a, f a * r ∂μ = ∫⁻ a, f a ∂μ * r :=
 by simp_rw [mul_comm, lintegral_const_mul' r f hr]
 
+/- A double integral of a product where each factor contains only one variable
+  is a product of integrals -/
+lemma lintegral_lintegral_mul {β} [measurable_space β] {ν : measure β}
+  {f : α → ennreal} {g : β → ennreal} (hf : measurable f) (hg : measurable g) :
+  ∫⁻ x, ∫⁻ y, f x * g y ∂ν ∂μ = ∫⁻ x, f x ∂μ * ∫⁻ y, g y ∂ν :=
+by simp [lintegral_const_mul _ hg, lintegral_mul_const _ hf]
+
 -- TODO: Need a better way of rewriting inside of a integral
 lemma lintegral_rw₁ {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ennreal) :
   (∫⁻ a, g (f a) ∂μ) = (∫⁻ a, g (f' a) ∂μ) :=
@@ -1273,7 +1286,7 @@ by simp [zero_lt_iff_ne_zero, hf, filter.eventually_eq, ae_iff, function.support
 lemma lintegral_supr_ae {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n))
   (h_mono : ∀n, ∀ᵐ a ∂μ, f n a ≤ f n.succ a) :
   (∫⁻ a, ⨆n, f n a ∂μ) = (⨆n, ∫⁻ a, f n a ∂μ) :=
-let ⟨s, hs⟩ := exists_is_measurable_superset_of_measure_eq_zero
+let ⟨s, hs⟩ := exists_is_measurable_superset_of_null
                        (ae_iff.1 (ae_all_iff.2 h_mono)) in
 let g := λ n a, if a ∈ s then 0 else f n a in
 have g_eq_f : ∀ᵐ a ∂μ, ∀n, g n a = f n a,

src/measure_theory/measurable_space.lean

@@ -937,6 +937,10 @@ instance : inhabited (α ≃ᵐ α) := ⟨refl α⟩
 @[simp] lemma coe_symm_mk (e : α ≃ β) (h1 : measurable e) (h2 : measurable e.symm) :
   ((⟨e, h1, h2⟩ : α ≃ᵐ β).symm : β → α) = e.symm := rfl
 
+@[simp] theorem symm_comp_self (e : α ≃ᵐ β) : e.symm ∘ e = id := funext e.left_inv
+
+@[simp] theorem self_comp_symm (e : α ≃ᵐ β) : e ∘ e.symm = id := funext e.right_inv
+
 /-- Equal measurable spaces are equivalent. -/
 protected def cast {α β} [i₁ : measurable_space α] [i₂ : measurable_space β]
   (h : α = β) (hi : i₁ == i₂) : α ≃ᵐ β :=

src/measure_theory/measure_space.lean

@@ -197,13 +197,13 @@ le_zero_iff_eq.1 $ h₂ ▸ measure_mono h
 lemma measure_mono_top (h : s₁ ⊆ s₂) (h₁ : μ s₁ = ⊤) : μ s₂ = ⊤ :=
 top_unique $ h₁ ▸ measure_mono h
 
-lemma exists_is_measurable_superset_of_measure_eq_zero (h : μ s = 0) :
+lemma exists_is_measurable_superset_of_null (h : μ s = 0) :
   ∃ t, s ⊆ t ∧ is_measurable t ∧ μ t = 0 :=
 outer_measure.exists_is_measurable_superset_of_trim_eq_zero (by rw [← measure_eq_trim, h])
 
 lemma exists_is_measurable_superset_iff_measure_eq_zero :
   (∃ t, s ⊆ t ∧ is_measurable t ∧ μ t = 0) ↔ μ s = 0 :=
-⟨λ ⟨t, hst, _, ht⟩, measure_mono_null hst ht, exists_is_measurable_superset_of_measure_eq_zero⟩
+⟨λ ⟨t, hst, _, ht⟩, measure_mono_null hst ht, exists_is_measurable_superset_of_null⟩
 
 theorem measure_Union_le [encodable β] (s : β → set α) : μ (⋃ i, s i) ≤ (∑' i, μ (s i)) :=
 μ.to_outer_measure.Union _
@@ -791,7 +791,7 @@ by rw [restrict_apply ht]
 lemma restrict_apply_eq_zero' (hs : is_measurable s) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0 :=
 begin
   refine ⟨λ h, le_zero_iff_eq.1 (h ▸ le_restrict_apply _ _), λ h, _⟩,
-  rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t', htt', ht', ht'0⟩,
+  rcases exists_is_measurable_superset_of_null h with ⟨t', htt', ht', ht'0⟩,
   apply measure_mono_null ((inter_subset _ _ _).1 htt'),
   rw [restrict_apply (hs.compl.union ht'), union_inter_distrib_right, compl_inter_self,
     set.empty_union],
@@ -1212,7 +1212,7 @@ instance : countable_Inter_filter μ.ae :=
 end⟩
 
 instance ae_is_measurably_generated : is_measurably_generated μ.ae :=
-⟨λ s hs, let ⟨t, hst, htm, htμ⟩ := exists_is_measurable_superset_of_measure_eq_zero hs in
+⟨λ s hs, let ⟨t, hst, htm, htμ⟩ := exists_is_measurable_superset_of_null hs in
   ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩
 
 lemma ae_all_iff [encodable ι] {p : α → ι → Prop} :
@@ -1286,7 +1286,7 @@ add_eq_zero_iff
 lemma ae_eq_comp {f : α → β} {g g' : β → δ} (hf : measurable f)
   (h : g =ᵐ[measure.map f μ] g') : g ∘ f =ᵐ[μ] g' ∘ f :=
 begin
-  rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, ht, tmeas, tzero⟩,
+  rcases exists_is_measurable_superset_of_null h with ⟨t, ht, tmeas, tzero⟩,
   refine le_antisymm _ bot_le,
   calc μ {x | g (f x) ≠ g' (f x)} ≤ μ (f⁻¹' t) : measure_mono (λ x hx, ht hx)
   ... = 0 : by rwa ← measure.map_apply hf tmeas
@@ -2089,7 +2089,7 @@ begin
   let s := {x | f x ≠ hμ.mk f x},
   have : μ s = 0 := hμ.ae_eq_mk,
   obtain ⟨t, st, t_meas, μt⟩ : ∃ t, s ⊆ t ∧ is_measurable t ∧ μ t = 0 :=
-    exists_is_measurable_superset_of_measure_eq_zero this,
+    exists_is_measurable_superset_of_null this,
   let g : α → β := t.piecewise (hν.mk f) (hμ.mk f),
   refine ⟨g, measurable.piecewise t_meas hν.measurable_mk hμ.measurable_mk, _⟩,
   change μ {x | f x ≠ g x} + ν {x | f x ≠ g x} = 0,

src/measure_theory/pi.lean

@@ -209,7 +209,7 @@ end
 
 /-- `measure.pi μ` is the finite product of the measures `{μ i | i : ι}`.
   It is defined to be measure corresponding to `measure_theory.outer_measure.pi`. -/
-protected def pi : measure (Π i, α i) :=
+@[irreducible] protected def pi : measure (Π i, α i) :=
 to_measure (outer_measure.pi (λ i, (μ i).to_outer_measure)) (pi_caratheodory μ)
 
 local attribute [instance] encodable.fintype.encodable
@@ -236,7 +236,7 @@ lemma pi_eval_preimage_null [∀ i, sigma_finite (μ i)] {i : ι} {s : set (α i
   (hs : μ i s = 0) : measure.pi μ (eval i ⁻¹' s) = 0 :=
 begin
   /- WLOG, `s` is measurable -/
-  rcases exists_is_measurable_superset_of_measure_eq_zero hs with ⟨t, hst, htm, hμt⟩,
+  rcases exists_is_measurable_superset_of_null hs with ⟨t, hst, htm, hμt⟩,
   suffices : measure.pi μ (eval i ⁻¹' t) = 0,
     from measure_mono_null (preimage_mono hst) this,
   clear_dependent s,

src/measure_theory/prod.lean

@@ -314,7 +314,7 @@ namespace measure
 
 /-- The binary product of measures. They are defined for arbitrary measures, but we basically
   prove all properties under the assumption that at least one of them is σ-finite. -/
-protected def prod (μ : measure α) (ν : measure β) : measure (α × β) :=
+@[irreducible] protected def prod (μ : measure α) (ν : measure β) : measure (α × β) :=
 bind μ $ λ x : α, map (prod.mk x) ν
 
 instance prod.measure_space {α β} [measure_space α] [measure_space β] : measure_space (α × β) :=
@@ -338,7 +338,7 @@ local attribute [instance] nonempty_measurable_superset
 lemma prod_prod_le (s : set α) (t : set β) : μ.prod ν (s.prod t) ≤ μ s * ν t :=
 begin
   by_cases hs0 : μ s = 0,
-  { rcases (exists_is_measurable_superset_of_measure_eq_zero hs0) with ⟨s', hs', h2s', h3s'⟩,
+  { rcases (exists_is_measurable_superset_of_null hs0) with ⟨s', hs', h2s', h3s'⟩,
     convert measure_mono (prod_mono hs' (subset_univ _)),
     simp_rw [hs0, prod_prod h2s' is_measurable.univ, h3s', zero_mul] },
   by_cases hti : ν t = ⊤,
@@ -349,7 +349,7 @@ begin
   rintro ⟨s', h1s', h2s'⟩,
   rw [subtype.coe_mk],
   by_cases ht0 : ν t = 0,
-  { rcases (exists_is_measurable_superset_of_measure_eq_zero ht0) with ⟨t', ht', h2t', h3t'⟩,
+  { rcases (exists_is_measurable_superset_of_null ht0) with ⟨t', ht', h2t', h3t'⟩,
     convert measure_mono (prod_mono (subset_univ _) ht'),
     simp_rw [ht0, prod_prod is_measurable.univ h2t', h3t', mul_zero] },
   by_cases hsi : μ s' = ⊤,
@@ -388,7 +388,7 @@ by simp_rw [prod_apply hs, lintegral_eq_zero_iff (measurable_measure_prod_mk_lef
 lemma measure_ae_null_of_prod_null {s : set (α × β)}
   (h : μ.prod ν s = 0) : (λ x, ν (prod.mk x ⁻¹' s)) =ᵐ[μ] 0 :=
 begin
-  obtain ⟨t, hst, mt, ht⟩ := exists_is_measurable_superset_of_measure_eq_zero h,
+  obtain ⟨t, hst, mt, ht⟩ := exists_is_measurable_superset_of_null h,
   simp_rw [measure_prod_null mt] at ht,
   rw [eventually_le_antisymm_iff],
   exact ⟨eventually_le.trans_eq
@@ -638,6 +638,11 @@ lemma lintegral_lintegral_swap [sigma_finite μ] ⦃f : α → β → ennreal⦄
   ∫⁻ x, ∫⁻ y, f x y ∂ν ∂μ = ∫⁻ y, ∫⁻ x, f x y ∂μ ∂ν :=
 (lintegral_lintegral hf).trans (lintegral_prod_symm _ hf)
 
+lemma lintegral_prod_mul {f : α → ennreal} {g : β → ennreal} (hf : measurable f)
+  (hg : measurable g) : ∫⁻ z, f z.1 * g z.2 ∂(μ.prod ν) = ∫⁻ x, f x ∂μ * ∫⁻ y, g y ∂ν :=
+by simp [lintegral_prod _ ((hf.comp measurable_fst).ennreal_mul $ hg.comp measurable_snd),
+  lintegral_lintegral_mul hf hg]
+
 /-! ### Integrability on a product -/
 section