feat(measure_theory/lp_space): add snorm_norm_rpow (#6619)

The lemma `snorm_norm_rpow` states `snorm (λ x, ∥f x∥ ^ q) p μ = (snorm f (p * ennreal.of_real q) μ) ^ q`.

Also add measurability lemmas about pow/rpow.

src/analysis/special_functions/pow.lean

@@ -428,6 +428,15 @@ begin
     exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _) }
 end
 
+lemma abs_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) : abs (x ^ y) = (abs x) ^ y :=
+begin
+  have h_rpow_nonneg : 0 ≤ x ^ y, from real.rpow_nonneg_of_nonneg hx_nonneg _,
+  rw [abs_eq_self.mpr hx_nonneg, abs_eq_self.mpr h_rpow_nonneg],
+end
+
+lemma norm_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) : ∥x ^ y∥ = ∥x∥ ^ y :=
+by { simp_rw real.norm_eq_abs, exact abs_rpow_of_nonneg hx_nonneg, }
+
 end real
 
 namespace complex
@@ -841,6 +850,11 @@ lemma measurable.rpow_const {α} [measurable_space α] {f : α → ℝ} (hf : me
   measurable (λ a : α, (f a) ^ y) :=
 hf.rpow measurable_const
 
+lemma ae_measurable.rpow_const {α} [measurable_space α] {f : α → ℝ}
+  {μ : measure_theory.measure α} (hf : ae_measurable f μ) {y : ℝ} :
+  ae_measurable (λ a : α, (f a) ^ y) μ :=
+measurable.comp_ae_measurable (measurable.rpow_const measurable_id) hf
+
 lemma real.measurable_rpow_const {y : ℝ} : measurable (λ x : ℝ, x ^ y) :=
 measurable_id.rpow_const
 
@@ -1635,6 +1649,27 @@ end
 lemma to_real_rpow (x : ℝ≥0∞) (z : ℝ) : (x.to_real) ^ z = (x ^ z).to_real :=
 by rw [ennreal.to_real, ennreal.to_real, ←nnreal.coe_rpow, ennreal.to_nnreal_rpow]
 
+lemma of_real_rpow_of_pos {x p : ℝ} (hx_pos : 0 < x) :
+  ennreal.of_real x ^ p = ennreal.of_real (x ^ p) :=
+begin
+  simp_rw ennreal.of_real,
+  rw [coe_rpow_of_ne_zero, coe_eq_coe, nnreal.of_real_rpow_of_nonneg hx_pos.le],
+  simp [hx_pos],
+end
+
+lemma of_real_rpow_of_nonneg {x p : ℝ} (hx_nonneg : 0 ≤ x) (hp_nonneg : 0 ≤ p) :
+  ennreal.of_real x ^ p = ennreal.of_real (x ^ p) :=
+begin
+  by_cases hp0 : p = 0,
+  { simp [hp0], },
+  by_cases hx0 : x = 0,
+  { rw ← ne.def at hp0,
+    have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm,
+    simp [hx0, hp_pos, hp_pos.ne.symm], },
+  rw ← ne.def at hx0,
+  exact of_real_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm),
+end
+
 lemma rpow_left_injective {x : ℝ} (hx : x ≠ 0) :
   function.injective (λ y : ℝ≥0∞, y^x) :=
 begin

src/measure_theory/borel_space.lean

@@ -573,6 +573,26 @@ begin
     (λ i _, hf i),
 end
 
+lemma measurable.pow {β} [comm_monoid α] [has_continuous_mul α] [second_countable_topology α]
+  [measurable_space β] {n : ℕ} {f : β → α} (hf : measurable f) :
+  measurable (λ x : β, (f x) ^ n) :=
+begin
+  simp_rw finset.pow_eq_prod_const,
+  exact finset.measurable_prod _ (λ _, hf),
+end
+
+lemma measurable_pow [comm_monoid α] [has_continuous_mul α] [second_countable_topology α] {n : ℕ} :
+  measurable (λ x : α, x ^ n) :=
+measurable_id.pow
+
+lemma ae_measurable.pow {β} [comm_monoid α] [has_continuous_mul α] [second_countable_topology α]
+  [measurable_space β] {n : ℕ} {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
+  ae_measurable (λ x : β, (f x) ^ n) μ :=
+begin
+  simp_rw finset.pow_eq_prod_const,
+  exact finset.ae_measurable_prod _ (λ _, hf),
+end
+
 @[to_additive]
 lemma measurable_inv [group α] [topological_group α] : measurable (has_inv.inv : α → α) :=
 continuous_inv.measurable

src/measure_theory/lp_space.lean

@@ -324,9 +324,55 @@ le_antisymm (snorm_mono_ae $ eventually_eq.le hfg)
 @[simp] lemma snorm'_norm {f : α → G} : snorm' (λ a, ∥f a∥) q μ = snorm' f q μ :=
 by simp [snorm']
 
+@[simp] lemma snorm'_norm {f : α → F} : snorm' (λ a, ∥f a∥) q μ = snorm' f q μ :=
+by simp [snorm']
+
 @[simp] lemma snorm_norm (f : α → F) : snorm (λ x, ∥f x∥) p μ = snorm f p μ :=
 snorm_congr_norm_ae $ eventually_of_forall $ λ x, norm_norm _
 
+lemma snorm'_norm_rpow (f : α → F) (p q : ℝ) (hq_pos : 0 < q) :
+  snorm' (λ x, ∥f x∥ ^ q) p μ = (snorm' f (p * q) μ) ^ q :=
+begin
+  simp_rw snorm',
+  rw [← ennreal.rpow_mul, ←one_div_mul_one_div],
+  simp_rw one_div,
+  rw [mul_assoc, inv_mul_cancel hq_pos.ne.symm, mul_one],
+  congr,
+  ext1 x,
+  simp_rw ← of_real_norm_eq_coe_nnnorm,
+  rw [real.norm_eq_abs, abs_eq_self.mpr (real.rpow_nonneg_of_nonneg (norm_nonneg _) _),
+    mul_comm, ← ennreal.of_real_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ennreal.rpow_mul],
+end
+
+lemma snorm_norm_rpow (f : α → F) (hq_pos : 0 < q) :
+  snorm (λ x, ∥f x∥ ^ q) p μ = (snorm f (p * ennreal.of_real q) μ) ^ q :=
+begin
+  by_cases h0 : p = 0,
+  { simp [h0, ennreal.zero_rpow_of_pos hq_pos], },
+  by_cases hp_top : p = ∞,
+  { simp only [hp_top, snorm_exponent_top, ennreal.top_mul, hq_pos.not_le, ennreal.of_real_eq_zero,
+      if_false, snorm_exponent_top, snorm_ess_sup],
+    have h_rpow : ess_sup (λ (x : α), (nnnorm (∥f x∥ ^ q) : ℝ≥0∞)) μ
+      = ess_sup (λ (x : α), (↑(nnnorm (f x))) ^ q) μ,
+    { congr,
+      ext1 x,
+      nth_rewrite 1 ← nnnorm_norm,
+      rw [ennreal.coe_rpow_of_nonneg _ hq_pos.le, ennreal.coe_eq_coe],
+      ext,
+      push_cast,
+      rw real.norm_rpow_of_nonneg (norm_nonneg _), },
+    rw h_rpow,
+    have h_rpow_mono := ennreal.rpow_left_strict_mono_of_pos hq_pos,
+    have h_rpow_surj := (ennreal.rpow_left_bijective hq_pos.ne.symm).2,
+    let iso := h_rpow_mono.order_iso_of_surjective _ h_rpow_surj,
+    exact (iso.ess_sup_apply (λ x, ((nnnorm (f x)) : ℝ≥0∞)) μ).symm, },
+  rw [snorm_eq_snorm' h0 hp_top, snorm_eq_snorm' _ _],
+  swap, { refine mul_ne_zero h0 _, rwa [ne.def, ennreal.of_real_eq_zero, not_le], },
+  swap, { exact ennreal.mul_ne_top hp_top ennreal.of_real_ne_top, },
+  rw [ennreal.to_real_mul, ennreal.to_real_of_real hq_pos.le],
+  exact snorm'_norm_rpow f p.to_real q hq_pos,
+end
+
 lemma snorm_congr_ae {f g : α → F} (hfg : f =ᵐ[μ] g) : snorm f p μ = snorm g p μ :=
 snorm_congr_norm_ae $ hfg.mono (λ x hx, hx ▸ rfl)