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

src/measure_theory/borel_space.lean

@@ -248,7 +248,7 @@ begin
   rw [borel_eq_generate_from_of_subbasis this],
   apply generate_from_le,
   rintros _ ⟨s, i, hi, rfl⟩,
-  refine is_measurable_pi i.countable_to_set (λ a ha, is_open.is_measurable _),
+  refine is_measurable.pi i.countable_to_set (λ a ha, is_open.is_measurable _),
   rw [hinst],
   exact generate_open.basic _ (hi a ha)
 end

src/measure_theory/measurable_space.lean

@@ -67,7 +67,7 @@ measurable space, σ-algebra, measurable function, measurable equivalence, dynki
 π-λ theorem, π-system
 -/
 
-open set encodable function
+open set encodable function equiv
 open_locale classical filter
 
 
@@ -121,6 +121,14 @@ begin
   exact ‹measurable_space α›.is_measurable_Union _ (is_measurable.bUnion_decode2 h)
 end
 
+lemma is_measurable.Union_fintype [fintype β] {f : β → set α} (h : ∀ b, is_measurable (f b)) :
+  is_measurable (⋃ b, f b) :=
+begin
+  have := encodable.trunc_encodable_of_fintype β,
+  induction this using trunc.rec_on_subsingleton,
+  exactI is_measurable.Union h
+end
+
 lemma is_measurable.bUnion {f : β → set α} {s : set β} (hs : countable s)
   (h : ∀ b ∈ s, is_measurable (f b)) : is_measurable (⋃ b ∈ s, f b) :=
 begin
@@ -157,6 +165,11 @@ lemma is_measurable.Inter [encodable β] {f : β → set α} (h : ∀ b, is_meas
 is_measurable.compl_iff.1 $
 by { rw compl_Inter, exact is_measurable.Union (λ b, (h b).compl) }
 
+lemma is_measurable.Inter_fintype [fintype β] {f : β → set α} (h : ∀ b, is_measurable (f b)) :
+  is_measurable (⋂ b, f b) :=
+is_measurable.compl_iff.1 $
+  by { rw compl_Inter, exact is_measurable.Union_fintype (λ b, (h b).compl) }
+
 lemma is_measurable.bInter {f : β → set α} {s : set β} (hs : countable s)
   (h : ∀ b ∈ s, is_measurable (f b)) : is_measurable (⋂ b ∈ s, f b) :=
 is_measurable.compl_iff.1 $
@@ -201,6 +214,10 @@ disjointed_induct (h n) (assume t i ht, is_measurable.diff ht $ h _)
 @[simp] lemma is_measurable.const (p : Prop) : is_measurable {a : α | p} :=
 by { by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ }
 
+/-- Every set has a measurable superset. Declare this as local instance as needed. -/
+lemma nonempty_measurable_superset (s : set α) : nonempty { t // s ⊆ t ∧ is_measurable t} :=
+⟨⟨univ, subset_univ s, is_measurable.univ⟩⟩
+
 end
 
 @[ext] lemma measurable_space.ext : ∀ {m₁ m₂ : measurable_space α},
@@ -527,7 +544,7 @@ section constructions
 variables [measurable_space α] [measurable_space β] [measurable_space γ]
 
 instance : measurable_space empty := ⊤
-instance : measurable_space unit := ⊤
+instance : measurable_space punit := ⊤ -- this also works for `unit`
 instance : measurable_space bool := ⊤
 instance : measurable_space ℕ := ⊤
 instance : measurable_space ℤ := ⊤
@@ -716,19 +733,65 @@ instance measurable_space.pi [m : Π a, measurable_space (π a)] : measurable_sp
 
 variables [Π a, measurable_space (π a)] [measurable_space γ]
 
+lemma measurable_pi_iff {g : α → Π a, π a} :
+  measurable g ↔ ∀ a, measurable (λ x, g x a) :=
+by simp_rw [measurable_iff_comap_le, measurable_space.pi, measurable_space.comap_supr,
+    measurable_space.comap_comp, function.comp, supr_le_iff]
+
 lemma measurable_pi_apply (a : δ) : measurable (λ f : Π a, π a, f a) :=
 measurable.of_comap_le $ le_supr _ a
 
+lemma measurable.eval {a : δ} {g : α → Π a, π a}
+  (hg : measurable g) : measurable (λ x, g x a) :=
+(measurable_pi_apply a).comp hg
+
 lemma measurable_pi_lambda (f : α → Π a, π a) (hf : ∀ a, measurable (λ c, f c a)) :
   measurable f :=
-measurable.of_le_map $ supr_le $ assume a, measurable_space.comap_le_iff_le_map.2 (hf a)
+measurable_pi_iff.mpr hf
 
-lemma is_measurable_pi {s : set δ} {t : Π i : δ, set (π i)} (hs : countable s)
+/-- The function `update f a : π a → Π a, π a` is always measurable.
+  This doesn't require `f` to be measurable.
+  This should not be confused with the statement that `update f a x` is measurable. -/
+lemma measurable_update (f : Π (a : δ), π a) {a : δ} : measurable (update f a) :=
+begin
+  apply measurable_pi_lambda,
+  intro x, by_cases hx : x = a,
+  { cases hx, convert measurable_id, ext, simp },
+  simp_rw [update_noteq hx], apply measurable_const,
+end
+
+/- Even though we cannot use projection notation, we still keep a dot to be consistent with similar
+  lemmas, like `is_measurable.prod`. -/
+lemma is_measurable.pi {s : set δ} {t : Π i : δ, set (π i)} (hs : countable s)
   (ht : ∀ i ∈ s, is_measurable (t i)) :
   is_measurable (s.pi t) :=
+by { rw [pi_def], exact is_measurable.bInter hs (λ i hi, measurable_pi_apply _ (ht i hi)) }
+
+lemma is_measurable.pi_univ [encodable δ] {t : Π i : δ, set (π i)}
+  (ht : ∀ i, is_measurable (t i)) : is_measurable (pi univ t) :=
+is_measurable.pi (countable_encodable _) (λ i _, ht i)
+
+lemma is_measurable.pi_fintype [fintype δ] {s : set δ} {t : Π i, set (π i)}
+  (ht : ∀ i ∈ s, is_measurable (t i)) : is_measurable (pi s t) :=
+begin
+  have := encodable.trunc_encodable_of_fintype δ,
+  induction this using trunc.rec_on_subsingleton,
+  exactI is_measurable.pi (countable_encodable _) ht
+end
+
+lemma is_measurable_pi_of_nonempty {s : set δ} {t : Π i, set (π i)} (hs : countable s)
+  (h : (pi s t).nonempty) : is_measurable (pi s t) ↔ ∀ i ∈ s, is_measurable (t i) :=
+begin
+  rcases h with ⟨f, hf⟩, refine ⟨λ hst i hi, _, is_measurable.pi hs⟩,
+  convert measurable_update f hst, rw [update_preimage_pi hi], exact λ j hj _, hf j hj
+end
+
+lemma is_measurable_pi {s : set δ} {t : Π i, set (π i)} (hs : countable s) :
+  is_measurable (pi s t) ↔ (∀ i ∈ s, is_measurable (t i)) ∨ pi s t = ∅ :=
 begin
-  rw [pi_def],
-  exact is_measurable.bInter hs (λ i hi, measurable_pi_apply _ (ht i hi))
+  cases (pi s t).eq_empty_or_nonempty with h h,
+  { simp [h] },
+  { simp [is_measurable_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty] }
 end
 
 end pi
@@ -801,6 +864,9 @@ lemma coe_eq (e : α ≃ᵐ β) : (e : α → β) = e.to_equiv := rfl
 protected lemma measurable (e : α ≃ᵐ β) : measurable (e : α → β) :=
 e.measurable_to_fun
 
+@[simp] lemma coe_mk (e : α ≃ β) (h1 : measurable e) (h2 : measurable e.symm) :
+  ((⟨e, h1, h2⟩ : α ≃ᵐ β) : α → β) = e := rfl
+
 /-- Any measurable space is equivalent to itself. -/
 def refl (α : Type*) [measurable_space α] : α ≃ᵐ α :=
 { to_equiv := equiv.refl α,
@@ -821,6 +887,9 @@ instance : inhabited (α ≃ᵐ α) := ⟨refl α⟩
   measurable_to_fun := ab.measurable_inv_fun,
   measurable_inv_fun := ab.measurable_to_fun }
 
+@[simp] lemma coe_symm_mk (e : α ≃ β) (h1 : measurable e) (h2 : measurable e.symm) :
+  ((⟨e, h1, h2⟩ : α ≃ᵐ β).symm : β → α) = e.symm := rfl
+
 /-- Equal measurable spaces are equivalent. -/
 protected def cast {α β} [i₁ : measurable_space α] [i₂ : measurable_space β]
   (h : α = β) (hi : i₁ == i₂) : α ≃ᵐ β :=
@@ -838,27 +907,27 @@ iff.intro
 
 /-- Products of equivalent measurable spaces are equivalent. -/
 def prod_congr (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) : α × γ ≃ᵐ β × δ :=
-{ to_equiv := equiv.prod_congr ab.to_equiv cd.to_equiv,
+{ to_equiv := prod_congr ab.to_equiv cd.to_equiv,
   measurable_to_fun := (ab.measurable_to_fun.comp measurable_id.fst).prod_mk
     (cd.measurable_to_fun.comp measurable_id.snd),
   measurable_inv_fun := (ab.measurable_inv_fun.comp measurable_id.fst).prod_mk
     (cd.measurable_inv_fun.comp measurable_id.snd) }
 
 /-- Products of measurable spaces are symmetric. -/
 def prod_comm : α × β ≃ᵐ β × α :=
-{ to_equiv := equiv.prod_comm α β,
+{ to_equiv := prod_comm α β,
   measurable_to_fun  := measurable_id.snd.prod_mk measurable_id.fst,
   measurable_inv_fun := measurable_id.snd.prod_mk measurable_id.fst }
 
 /-- Products of measurable spaces are associative. -/
 def prod_assoc : (α × β) × γ ≃ᵐ α × (β × γ) :=
-{ to_equiv := equiv.prod_assoc α β γ,
+{ to_equiv := prod_assoc α β γ,
   measurable_to_fun  := measurable_fst.fst.prod_mk $ measurable_fst.snd.prod_mk measurable_snd,
   measurable_inv_fun := (measurable_fst.prod_mk measurable_snd.fst).prod_mk measurable_snd.snd }
 
 /-- Sums of measurable spaces are symmetric. -/
 def sum_congr (ab : α ≃ᵐ β) (cd : γ ≃ᵐ δ) : α ⊕ γ ≃ᵐ β ⊕ δ :=
-{ to_equiv := equiv.sum_congr ab.to_equiv cd.to_equiv,
+{ to_equiv := sum_congr ab.to_equiv cd.to_equiv,
   measurable_to_fun :=
     begin
       cases ab with ab' abm, cases ab', cases cd with cd' cdm, cases cd',
@@ -898,7 +967,7 @@ noncomputable def set.image (f : α → β) (s : set α) (hf : injective f)
   measurable_to_fun  := (hfm.comp measurable_id.subtype_coe).subtype_mk,
   measurable_inv_fun :=
     begin
-      rintro t ⟨u, hu, rfl⟩, simp [preimage_preimage, equiv.set.image_symm_preimage hf],
+      rintro t ⟨u, hu, rfl⟩, simp [preimage_preimage, set.image_symm_preimage hf],
       exact measurable_subtype_coe (hfi u hu)
     end }
 
@@ -948,7 +1017,7 @@ def set.range_inr : (range sum.inr : set (α ⊕ β)) ≃ᵐ β :=
 /-- Products distribute over sums (on the right) as measurable spaces. -/
 def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
   (α ⊕ β) × γ ≃ᵐ (α × γ) ⊕ (β × γ) :=
-{ to_equiv := equiv.sum_prod_distrib α β γ,
+{ to_equiv := sum_prod_distrib α β γ,
   measurable_to_fun  :=
   begin
     refine measurable_of_measurable_union_cover
@@ -986,6 +1055,17 @@ def sum_prod_sum (α β γ δ)
   (α ⊕ β) × (γ ⊕ δ) ≃ᵐ ((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ)) :=
 (sum_prod_distrib _ _ _).trans $ sum_congr (prod_sum_distrib _ _ _) (prod_sum_distrib _ _ _)
 
+variables {π π' : δ' → Type*} [∀ x, measurable_space (π x)] [∀ x, measurable_space (π' x)]
+
+/-- A family of measurable equivalences `Π a, β₁ a ≃ᵐ β₂ a` generates a measurable equivalence
+  between  `Π a, β₁ a` and `Π a, β₂ a`. -/
+def Pi_congr_right (e : Π a, π a ≃ᵐ π' a) : (Π a, π a) ≃ᵐ (Π a, π' a) :=
+{ to_equiv := Pi_congr_right (λ a, (e a).to_equiv),
+  measurable_to_fun :=
+    measurable_pi_lambda _ (λ i, (e i).measurable_to_fun.comp (measurable_pi_apply i)),
+  measurable_inv_fun :=
+    measurable_pi_lambda _ (λ i, (e i).measurable_inv_fun.comp (measurable_pi_apply i)) }
+
 end measurable_equiv
 
 /-- A pi-system is a collection of subsets of `α` that is closed under intersections of sets that

src/measure_theory/measure_space.lean

@@ -172,6 +172,13 @@ by rw μ.trimmed; refl
 lemma measure_eq_infi (s) : μ s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), μ t :=
 by rw [measure_eq_trim, outer_measure.trim_eq_infi]; refl
 
+/-- A variant of `measure_eq_infi` which has a single `infi`. This is useful when applying a
+  lemma next that only works for non-empty infima, in which case you can use
+  `nonempty_measurable_superset`. -/
+lemma measure_eq_infi' (μ : measure α) (s : set α) :
+  μ s = ⨅ t : { t // s ⊆ t ∧ is_measurable t}, μ t :=
+by simp_rw [infi_subtype, infi_and, subtype.coe_mk, ← measure_eq_infi]
+
 lemma measure_eq_induced_outer_measure :
   μ s = induced_outer_measure (λ s _, μ s) is_measurable.empty μ.empty s :=
 measure_eq_trim _
@@ -491,6 +498,10 @@ begin
   exact λ x ⟨⟨_, h₁⟩, _, h₂⟩, h₂ h₁
 end
 
+protected lemma caratheodory (μ : measure α) {s t : set α} (hs : is_measurable s) :
+  μ (t ∩ s) + μ (t \ s) = μ t :=
+(le_to_outer_measure_caratheodory μ s hs t).symm
+
 @[simp] lemma to_measure_to_outer_measure {α} (m : outer_measure α)
   [ms : measurable_space α] (h : ms ≤ m.caratheodory) :
   (m.to_measure h).to_outer_measure = m.trim := rfl
@@ -699,6 +710,8 @@ if hf : measurable f then
     le_to_outer_measure_caratheodory μ _ (hf hs) (f ⁻¹' t)
 else 0
 
+/-- We can evaluate the pushforward on measurable sets. For non-measurable sets, see
+  `measure_theory.measure.le_map_apply` and `measurable_equiv.map_apply`. -/
 @[simp] theorem map_apply {f : α → β} (hf : measurable f) {s : set β} (hs : is_measurable s) :
   map f μ s = μ (f ⁻¹' s) :=
 by simp [map, dif_pos hf, hs]
@@ -711,6 +724,15 @@ lemma map_map {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurab
 ext $ λ s hs,
 by simp [hf, hg, hs, hg hs, hg.comp hf, ← preimage_comp]
 
+/-- Even if `s` is not measurable, we can bound `map f μ s` from below.
+  See also `measurable_equiv.map_apply`. -/
+theorem le_map_apply {f : α → β} (hf : measurable f) (s : set β) : μ (f ⁻¹' s) ≤ map f μ s :=
+begin
+  rw [measure_eq_infi' (map f μ)], refine le_infi _, rintro ⟨t, hst, ht⟩,
+  convert measure_mono (preimage_mono hst),
+  exact map_apply hf ht
+end
+
 /-- Pullback of a `measure`. If `f` sends each `measurable` set to a `measurable` set, then for each
 measurable set `s` we have `comap f μ s = μ (f '' s)`. -/
 def comap (f : α → β) : measure β →ₗ[ennreal] measure α :=
@@ -1740,6 +1762,32 @@ end measure_theory
 
 open measure_theory measure_theory.measure
 
+namespace measurable_equiv
+
+open equiv
+
+variables {α β : Type*} [measurable_space α] [measurable_space β]
+variables {μ : measure α} {ν : measure β}
+
+/-- If we map a measure along a measurable equivalence, we can compute the measure on all sets
+  (not just the measurable ones). -/
+protected theorem map_apply (f : α ≃ᵐ β) (s : set β) : measure.map f μ s = μ (f ⁻¹' s) :=
+begin
+  refine le_antisymm _ (le_map_apply f.measurable s),
+  rw [measure_eq_infi' μ],
+  refine le_infi _, rintro ⟨t, hst, ht⟩,
+  rw [subtype.coe_mk],
+  have := f.symm.to_equiv.image_eq_preimage,
+  simp only [←coe_eq, symm_symm, symm_to_equiv] at this,
+  rw [← this, image_subset_iff] at hst,
+  convert measure_mono hst,
+  rw [map_apply, preimage_preimage],
+  { refine congr_arg μ (eq.symm _), convert preimage_id, exact funext f.left_inv },
+  exacts [f.measurable, f.measurable_inv_fun ht]
+end
+
+end measurable_equiv
+
 section is_complete
 
 /-- A measure is complete if every null set is also measurable.

src/measure_theory/prod.lean

@@ -333,6 +333,31 @@ by simp_rw [prod_apply (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
   lintegral_indicator _ hs, lintegral_const, restrict_apply is_measurable.univ,
   univ_inter, mul_comm]
 
+local attribute [instance] nonempty_measurable_superset
+/-- If we don't assume measurability of `s` and `t`, we can bound the measure of their product. -/
+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'⟩,
+    convert measure_mono (prod_mono hs' (subset_univ _)),
+    simp_rw [hs0, prod_prod h2s' is_measurable.univ, h3s', zero_mul] },
+  by_cases hti : ν t = ⊤,
+  { convert le_top, simp_rw [hti, ennreal.mul_top, hs0, if_false] },
+  rw [measure_eq_infi' μ],
+  simp_rw [ennreal.infi_mul hti], refine le_infi _, 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'⟩,
+    convert measure_mono (prod_mono (subset_univ _) ht'),
+    simp_rw [ht0, prod_prod is_measurable.univ h2t', h3t', mul_zero] },
+  by_cases hsi : μ s' = ⊤,
+  { convert le_top, simp_rw [hsi, ennreal.top_mul, ht0, if_false] },
+  rw [measure_eq_infi' ν],
+  simp_rw [ennreal.mul_infi hsi], refine le_infi _, rintro ⟨t', h1t', h2t'⟩,
+  convert measure_mono (prod_mono h1s' h1t'),
+  simp [prod_prod h2s' h2t'],
+end
+
 lemma ae_measure_lt_top {s : set (α × β)} (hs : is_measurable s)
   (h2s : (μ.prod ν) s < ⊤) : ∀ᵐ x ∂μ, ν (prod.mk x ⁻¹' s) < ⊤ :=
 by { simp_rw [prod_apply hs] at h2s, refine ae_lt_top (measurable_measure_prod_mk_left hs) h2s }