chore(analysis/special_functions/pow): review lemmas about measurabil…

…ity of `cpow`/`rpow` (#6209)

* prove that `complex.cpow` is measurable;
* deduce measurability of `real.rpow` from definition, not continuity.

src/analysis/special_functions/pow.lean

@@ -114,6 +114,12 @@ by rw [← cpow_nat_cast, ← cpow_mul _ h.1 h.2,
 
 end complex
 
+lemma measurable.cpow {α : Type*} [measurable_space α] {f g : α → ℂ}
+  (hf : measurable f) (hg : measurable g) : measurable (λ x, f x ^ g x) :=
+measurable.ite (hf $ measurable_set_singleton _)
+  (measurable_const.ite (hg $ measurable_set_singleton _) measurable_const)
+  (hf.clog.mul hg).cexp
+
 namespace real
 
 /-- The real power function `x^y`, defined as the real part of the complex power function.
@@ -601,59 +607,20 @@ end real
 
 section measurability_real
 
-lemma real.measurable_rpow : measurable (λ p : ℝ × ℝ, p.1 ^ p.2) :=
-begin
-  have h_meas : measurable_set {p : ℝ × ℝ | p.1 = 0} :=
-    (is_closed_singleton.preimage continuous_fst).measurable_set,
-  refine measurable_of_measurable_union_cover {p : ℝ × ℝ | p.1 = 0} {p : ℝ × ℝ | p.1 ≠ 0} h_meas
-    h_meas.compl _ _ _,
-  { intro x, simp [em (x.fst = 0)], },
-  { have h_eq_ite : (λ a : {p : ℝ × ℝ | p.fst = 0}, (a:ℝ×ℝ).fst ^ (a:ℝ×ℝ).snd) =
-      λ a : {p : ℝ × ℝ | p.fst = 0}, ite ((a:ℝ×ℝ).snd = 0) 1 0,
-    { ext1 a,
-      have h_fst_zero : (a:ℝ×ℝ).fst = 0, from a.prop,
-      rw h_fst_zero,
-      split_ifs with h_snd,
-      { rw h_snd,
-        exact real.rpow_zero _, },
-      exact real.zero_rpow h_snd, },
-    rw h_eq_ite,
-    change measurable ((λ x : ℝ, ite (x = 0) (1:ℝ) (0:ℝ))
-      ∘ (λ a : {p : ℝ × ℝ | p.fst = 0}, (a:ℝ×ℝ).snd)),
-    refine measurable.comp _ (measurable_snd.comp measurable_subtype_coe),
-    exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const, },
-  { refine continuous.measurable _,
-    rw continuous_iff_continuous_at,
-    intro x,
-    change continuous_at ((λ a : ℝ × ℝ, a.fst ^ a.snd)
-      ∘ (λ a : {p : ℝ × ℝ | p.fst ≠ 0}, (a:ℝ×ℝ))) x,
-    refine continuous_at.comp _ continuous_at_subtype_coe,
-    change continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) x.val,
-    have h_x : x.val = (x.val.fst, x.val.snd), by simp,
-    rw h_x,
-    exact real.continuous_at_rpow_of_ne_zero x.prop _, },
-end
+open complex
 
 lemma measurable.rpow {α} [measurable_space α] {f g : α → ℝ} (hf : measurable f)
   (hg : measurable g) :
   measurable (λ a : α, (f a) ^ (g a)) :=
-begin
-  change measurable ((λ p : ℝ × ℝ, p.1 ^ p.2) ∘ (λ a : α, (f a, g a))),
-  exact real.measurable_rpow.comp (measurable.prod hf hg),
-end
-
-lemma real.measurable_rpow_const {y : ℝ} : measurable (λ x : ℝ, x ^ y) :=
-begin
-  change measurable ((λ p : ℝ × ℝ, p.1 ^ p.2) ∘ (λ x : ℝ, (id x, (λ x, y) x))),
-  refine real.measurable_rpow.comp (measurable.prod measurable_id _),
-  change measurable (λ (a : ℝ), y),
-  exact measurable_const,
-end
+measurable_re.comp $ ((measurable_of_real.comp hf).cpow (measurable_of_real.comp hg))
 
 lemma measurable.rpow_const {α} [measurable_space α] {f : α → ℝ} (hf : measurable f) {y : ℝ} :
   measurable (λ a : α, (f a) ^ y) :=
 hf.rpow measurable_const
 
+lemma real.measurable_rpow_const {y : ℝ} : measurable (λ x : ℝ, x ^ y) :=
+measurable_id.rpow_const
+
 end measurability_real
 
 section differentiability
@@ -1008,40 +975,21 @@ end
 
 end nnreal
 
-section measurability_nnreal
+namespace measurable
 
-lemma nnreal.measurable_rpow : measurable (λ p : ℝ≥0 × ℝ, p.1 ^ p.2) :=
-begin
-  have h_rw : (λ p : ℝ≥0 × ℝ, p.1 ^ p.2) = (λ p : ℝ≥0 × ℝ, nnreal.of_real(↑(p.1) ^ p.2)),
-  { ext1 a,
-    rw [←nnreal.coe_rpow, nnreal.of_real_coe], },
-  rw h_rw,
-  exact (measurable_fst.nnreal_coe.rpow measurable_snd).nnreal_of_real,
-end
+variables {α : Type*} [measurable_space α]
 
-lemma measurable.nnreal_rpow {α} [measurable_space α] {f : α → ℝ≥0} (hf : measurable f)
+lemma nnreal_rpow {f : α → ℝ≥0} (hf : measurable f)
   {g : α → ℝ} (hg : measurable g) :
   measurable (λ a : α, (f a) ^ (g a)) :=
-begin
-  change measurable ((λ p : ℝ≥0 × ℝ, p.1 ^ p.2) ∘ (λ a : α, (f a, g a))),
-  exact nnreal.measurable_rpow.comp (measurable.prod hf hg),
-end
-
-lemma nnreal.measurable_rpow_const {y : ℝ} : measurable (λ a : ℝ≥0, a ^ y) :=
-begin
-  have h_rw : (λ a : ℝ≥0, a ^ y) = (λ a : ℝ≥0, nnreal.of_real(↑a ^ y)),
-  { ext1 a,
-    rw [←nnreal.coe_rpow, nnreal.of_real_coe], },
-  rw h_rw,
-  exact nnreal.measurable_coe.rpow_const.nnreal_of_real,
-end
+(hf.nnreal_coe.rpow hg).subtype_mk
 
-lemma measurable.nnreal_rpow_const {α} [measurable_space α] {f : α → ℝ≥0} (hf : measurable f)
+lemma nnreal_rpow_const {f : α → ℝ≥0} (hf : measurable f)
   {y : ℝ} :
   measurable (λ a : α, (f a) ^ y) :=
 hf.nnreal_rpow measurable_const
 
-end measurability_nnreal
+end measurable
 
 open filter
 
@@ -1553,39 +1501,35 @@ end ennreal
 
 section measurability_ennreal
 
+variables {α : Type*} [measurable_space α]
+
 lemma ennreal.measurable_rpow : measurable (λ p : ℝ≥0∞ × ℝ, p.1 ^ p.2) :=
 begin
   refine ennreal.measurable_of_measurable_nnreal_prod _ _,
   { simp_rw ennreal.coe_rpow_def,
-    refine measurable.ite _ measurable_const nnreal.measurable_rpow.ennreal_coe,
+    refine measurable.ite _ measurable_const 
+      (measurable_fst.nnreal_rpow measurable_snd).ennreal_coe,
     exact measurable_set.inter (measurable_fst (measurable_set_singleton 0))
       (measurable_snd measurable_set_Iio), },
   { simp_rw ennreal.top_rpow_def,
     refine measurable.ite measurable_set_Ioi measurable_const _,
     exact measurable.ite (measurable_set_singleton 0) measurable_const measurable_const, },
 end
 
-lemma measurable.ennreal_rpow {α} [measurable_space α] {f : α → ℝ≥0∞} (hf : measurable f)
-  {g : α → ℝ} (hg : measurable g) :
+lemma measurable.ennreal_rpow {f : α → ℝ≥0∞} (hf : measurable f) {g : α → ℝ} (hg : measurable g) :
   measurable (λ a : α, (f a) ^ (g a)) :=
 begin
   change measurable ((λ p : ℝ≥0∞ × ℝ, p.1 ^ p.2) ∘ (λ a, (f a, g a))),
   exact ennreal.measurable_rpow.comp (measurable.prod hf hg),
 end
 
-lemma ennreal.measurable_rpow_const {y : ℝ} : measurable (λ a : ℝ≥0∞, a ^ y) :=
-begin
-  change measurable ((λ p : ℝ≥0∞ × ℝ, p.1 ^ p.2) ∘ (λ a, (a, y))),
-  refine ennreal.measurable_rpow.comp (measurable.prod measurable_id _),
-  dsimp only,
-  exact measurable_const,
-end
-
-lemma measurable.ennreal_rpow_const {α} [measurable_space α] {f : α → ℝ≥0∞} (hf : measurable f)
-  {y : ℝ} :
+lemma measurable.ennreal_rpow_const {f : α → ℝ≥0∞} (hf : measurable f) {y : ℝ} :
   measurable (λ a : α, (f a) ^ y) :=
 hf.ennreal_rpow measurable_const
 
+lemma ennreal.measurable_rpow_const {y : ℝ} : measurable (λ a : ℝ≥0∞, a ^ y) :=
+measurable_id.ennreal_rpow_const
+
 lemma ae_measurable.ennreal_rpow_const {α} [measurable_space α] {f : α → ℝ≥0∞}
   {μ : measure_theory.measure α} (hf : ae_measurable f μ) {y : ℝ} :
   ae_measurable (λ a : α, (f a) ^ y) μ :=

src/analysis/special_functions/trigonometric.lean

@@ -2881,7 +2881,7 @@ end
 
 lemma tendsto_tan_pi_div_two : tendsto tan (𝓝[Iio (π/2)] (π/2)) at_top :=
 begin
-  convert (tendsto.inv_tendsto_zero tendsto_cos_pi_div_two).at_top_mul (by norm_num)
+  convert (tendsto.inv_tendsto_zero tendsto_cos_pi_div_two).at_top_mul zero_lt_one
             tendsto_sin_pi_div_two,
   simp only [pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
 end

src/measure_theory/borel_space.lean

@@ -924,8 +924,8 @@ instance rat.borel_space : borel_space ℚ := ⟨borel_eq_top_of_encodable.symm
 instance real.measurable_space : measurable_space ℝ := borel ℝ
 instance real.borel_space : borel_space ℝ := ⟨rfl⟩
 
-instance nnreal.measurable_space : measurable_space ℝ≥0 := borel ℝ≥0
-instance nnreal.borel_space : borel_space ℝ≥0 := ⟨rfl⟩
+instance nnreal.measurable_space : measurable_space ℝ≥0 := subtype.measurable_space
+instance nnreal.borel_space : borel_space ℝ≥0 := subtype.borel_space _
 
 instance ennreal.measurable_space : measurable_space ℝ≥0∞ := borel ℝ≥0∞
 instance ennreal.borel_space : borel_space ℝ≥0∞ := ⟨rfl⟩