measurable equiv

src/analysis/measure_theory/borel_space.lean

@@ -14,7 +14,8 @@ We would like to have definitional equality for
 
 Unfortunately, this only holds if t₁ and t₂ are second-countable topologies.
 -/
-import analysis.measure_theory.measurable_space analysis.real
+import analysis.measure_theory.measurable_space analysis.ennreal
+noncomputable theory
 
 open classical set lattice real
 local attribute [instance] prop_decidable
@@ -143,6 +144,12 @@ is_measurable_of_is_closed is_closed_closure
 lemma measurable_of_continuous [topological_space β] {f : α → β} (h : continuous f) : measurable f :=
 measurable_generate_from $ assume t ht, is_measurable_of_is_open $ h t ht
 
+def measurablee_equiv.borel [topological_space α] [topological_space β] (h : α ≃ₜ β) :
+  measurable_equiv α β :=
+{ to_equiv := h.to_equiv,
+  measurable_to_fun := measurable_of_continuous h.continuous_to_fun,
+  measurable_inv_fun := measurable_of_continuous h.continuous_inv_fun }
+
 lemma borel_prod_le [topological_space β] :
   prod.measurable_space ≤ borel (α × β) :=
 sup_le
@@ -163,6 +170,18 @@ le_antisymm borel_prod_le begin
       eq.symm ▸ is_measurable_set_prod (is_measurable_of_is_open hu) (is_measurable_of_is_open hv))
 end
 
+lemma borel_eq_comap [t : topological_space β] (f : α → β) :
+  @borel α (t.induced f) = (borel β).comap f :=
+le_antisymm
+  (measurable_space.generate_from_le $ assume s ⟨t, ht, eq⟩,
+    eq.symm ▸ ⟨_, is_measurable_of_is_open ht, rfl⟩)
+  (measurable_space.comap_le_iff_le_map.2 $ measurable_space.generate_from_le $ assume s hs,
+    @is_measurable_of_is_open α (f ⁻¹' s) (t.induced f) ⟨_, hs, rfl⟩)
+
+lemma borel_eq_subtype [topological_space α] (s : set α) :
+  borel s = subtype.measurable_space :=
+borel_eq_comap coe
+
 lemma measurable_of_continuous2
   [topological_space α] [second_countable_topology α]
   [topological_space β] [second_countable_topology β]
@@ -319,3 +338,93 @@ begin
 end
 
 end real
+
+namespace ennreal
+open filter measure_theory
+
+lemma measurable_coe : measurable (coe : nnreal → ennreal) :=
+measurable_of_continuous (continuous_coe.2 continuous_id)
+
+def ennreal_equiv_nnreal : measurable_equiv {r : ennreal | r < ⊤} nnreal :=
+{ to_fun    := λr, ennreal.to_nnreal r.1,
+  inv_fun   := λr, ⟨r, coe_lt_top⟩,
+  left_inv  := assume ⟨r, hr⟩, by simp [coe_to_nnreal (ne_of_lt hr)],
+  right_inv := assume r, to_nnreal_coe,
+  measurable_to_fun  :=
+  begin
+    rw [← borel_eq_subtype],
+    refine measurable_of_continuous (continuous_iff_tendsto.2 _),
+    rintros ⟨r, hr⟩,
+    simp [nhds_subtype_eq_comap],
+    refine tendsto.comp tendsto_comap (tendsto_to_nnreal (ne_of_lt hr))
+  end,
+  measurable_inv_fun := measurable_subtype_mk measurable_coe }
+
+lemma measurable_of_measurable_nnreal [measurable_space α] {f : ennreal → α}
+  (h : measurable (λp:nnreal, f p)) : measurable f :=
+begin
+  refine measurable_of_measurable_union_cover {⊤} {r : ennreal | r < ⊤}
+    (is_measurable_of_is_closed $ is_closed_singleton)
+    (is_measurable_of_is_open $ is_open_gt' _)
+    (assume r _, by cases r; simp [ennreal.none_eq_top, ennreal.some_eq_coe])
+    _
+    _,
+  exact (measurable_equiv.set.singleton ⊤).symm.measurable_coe_iff.1 (measurable_unit _),
+  exact (ennreal_equiv_nnreal.symm.measurable_coe_iff.1 h)
+end
+
+def ennreal_equiv_sum :
+  @measurable_equiv ennreal (nnreal ⊕ unit) _ sum.measurable_space :=
+{ to_fun    :=
+    @option.rec nnreal (λ_, nnreal ⊕ unit) (sum.inr ()) (sum.inl : nnreal → nnreal ⊕ unit),
+  inv_fun   :=
+    @sum.rec nnreal unit (λ_, ennreal) (coe : nnreal → ennreal) (λ_, ⊤),
+  left_inv  := assume s, by cases s; refl,
+  right_inv := assume s, by rcases s with r | ⟨⟨⟩⟩; refl,
+  measurable_to_fun  := measurable_of_measurable_nnreal measurable_inl,
+  measurable_inv_fun := measurable_sum measurable_coe (@measurable_const ennreal unit _ _ ⊤) }
+
+lemma measurable_of_measurable_nnreal_nnreal [measurable_space α] [measurable_space β]
+  (f : ennreal → ennreal → β) {g : α → ennreal} {h : α → ennreal}
+  (h₁ : measurable (λp:nnreal × nnreal, f p.1 p.2))
+  (h₂ : measurable (λr:nnreal, f ⊤ r))
+  (h₃ : measurable (λr:nnreal, f r ⊤))
+  (hg : measurable g) (hh : measurable h) : measurable (λa, f (g a) (h a)) :=
+let e : measurable_equiv (ennreal × ennreal)
+  (((nnreal × nnreal) ⊕ (nnreal × unit)) ⊕ ((unit × nnreal) ⊕ (unit × unit))) :=
+  (measurable_equiv.prod_congr ennreal_equiv_sum ennreal_equiv_sum).trans
+    (measurable_equiv.sum_prod_sum _ _ _ _) in
+have measurable (λp:ennreal×ennreal, f p.1 p.2),
+begin
+  refine e.symm.measurable_coe_iff.1 (measurable_sum (measurable_sum _ _) (measurable_sum _ _)),
+  { show measurable (λp:nnreal × nnreal, f p.1 p.2),
+    exact h₁ },
+  { show measurable (λp:nnreal × unit, f p.1 ⊤),
+    exact (measurable_fst measurable_id).comp h₃ },
+  { show measurable ((λp:nnreal, f ⊤ p) ∘ (λp:unit × nnreal, p.2)),
+    exact measurable.comp (measurable_snd measurable_id) h₂ },
+  { show measurable (λp:unit × unit, f ⊤ ⊤),
+    exact measurable_const }
+end,
+(measurable_prod_mk hg hh).comp this
+
+lemma measurable_mul {α : Type*} [measurable_space α] {f g : α → ennreal} :
+  measurable f → measurable g → measurable (λa, f a * g a) :=
+begin
+  refine measurable_of_measurable_nnreal_nnreal (*) _ _ _,
+  { simp only [ennreal.coe_mul.symm],
+    exact (measurable_mul (measurable_fst measurable_id) (measurable_snd measurable_id)).comp
+      measurable_coe },
+  { simp [top_mul],
+    exact measurable.if
+      (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const)
+      measurable_const
+      measurable_const },
+  { simp [mul_top],
+    exact measurable.if
+      (is_measurable_of_is_closed $ is_closed_eq continuous_id continuous_const)
+      measurable_const
+      measurable_const }
+end
+
+end ennreal