feat(measure_theory/integral/set_integral): integral of a is_R_or_C…

… function equals integral of real part + integral of imaginary part (#9735)




Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

src/data/complex/is_R_or_C.lean

@@ -422,6 +422,10 @@ by simp [abs, norm_sq, norm_sq_of_real, real.sqrt_mul_self_eq_abs]
 
 lemma norm_eq_abs (z : K) : ∥z∥ = absK z := by simp [abs, norm_sq_eq_def']
 
+@[norm_cast]
+lemma norm_of_real (z : ℝ) : ∥(z : K)∥ = ∥z∥ :=
+by { rw [is_R_or_C.norm_eq_abs, is_R_or_C.abs_of_real, real.norm_eq_abs] }
+
 lemma abs_of_nonneg {r : ℝ} (h : 0 ≤ r) : absK r = r :=
 (abs_of_real _).trans (abs_of_nonneg h)
 

src/measure_theory/function/conditional_expectation.lean

@@ -1811,8 +1811,8 @@ begin
     rw [with_densityᵥ_apply
         (signed_measure.integrable_rn_deriv ((μ.with_densityᵥ f).trim hm) (μ.trim hm)) hs,
       ← set_integral_trim hm _ hs],
-    measurability },
-  { exact measurable.ae_measurable' (by measurability), },
+    exact signed_measure.measurable_rn_deriv _ _ },
+  { exact measurable.ae_measurable' (signed_measure.measurable_rn_deriv _ _) },
 end
 
 end real

src/measure_theory/function/l1_space.lean

@@ -666,7 +666,18 @@ end
 end normed_space_over_complete_field
 
 section is_R_or_C
-variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜}
+variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] {f : α → 𝕜}
+
+lemma integrable.of_real [borel_space 𝕜] {f : α → ℝ} (hf : integrable f μ) :
+  integrable (λ x, (f x : 𝕜)) μ :=
+by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.of_real }
+
+lemma integrable.re_im_iff [borel_space 𝕜] :
+  integrable (λ x, is_R_or_C.re (f x)) μ ∧ integrable (λ x, is_R_or_C.im (f x)) μ ↔
+  integrable f μ :=
+by { simp_rw ← mem_ℒp_one_iff_integrable, exact mem_ℒp_re_im_iff }
+
+variable [opens_measurable_space 𝕜]
 
 lemma integrable.re (hf : integrable f μ) : integrable (λ x, is_R_or_C.re (f x)) μ :=
 by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.re, }

src/measure_theory/function/lp_space.lean

@@ -1711,29 +1711,40 @@ variables [second_countable_topology E] [borel_space E]
   [second_countable_topology F] [measurable_space F] [borel_space F]
   {g : E → F} {c : ℝ≥0}
 
+lemma lipschitz_with.comp_mem_ℒp {α E F} {K} [measurable_space α] {μ : measure α}
+  [measurable_space E] [measurable_space F] [normed_group E] [normed_group F] [borel_space E]
+  [borel_space F] {f : α → E} {g : E → F} (hg : lipschitz_with K g)
+  (g0 : g 0 = 0) (hL : mem_ℒp f p μ) : mem_ℒp (g ∘ f) p μ  :=
+begin
+  have : ∀ᵐ x ∂μ, ∥g (f x)∥ ≤ K * ∥f x∥,
+  { apply filter.eventually_of_forall (λ x, _),
+    rw [← dist_zero_right, ← dist_zero_right, ← g0],
+    apply hg.dist_le_mul },
+  exact hL.of_le_mul (hg.continuous.measurable.comp_ae_measurable hL.1) this,
+end
+
+lemma measure_theory.mem_ℒp.of_comp_antilipschitz_with {α E F} {K'}
+  [measurable_space α] {μ : measure α} [measurable_space E] [measurable_space F] [normed_group E]
+  [normed_group F] [borel_space E] [borel_space F] [complete_space E]
+  {f : α → E} {g : E → F} (hL : mem_ℒp (g ∘ f) p μ)
+  (hg : uniform_continuous g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) : mem_ℒp f p μ :=
+begin
+  have : ∀ᵐ x ∂μ, ∥f x∥ ≤ K' * ∥g (f x)∥,
+    { apply filter.eventually_of_forall (λ x, _),
+      rw [← dist_zero_right, ← dist_zero_right, ← g0],
+      apply hg'.le_mul_dist },
+  exact hL.of_le_mul ((ae_measurable_comp_iff_of_closed_embedding g
+    (hg'.closed_embedding hg)).1 hL.1) this,
+end
+
 namespace lipschitz_with
 
 lemma mem_ℒp_comp_iff_of_antilipschitz {α E F} {K K'} [measurable_space α] {μ : measure α}
   [measurable_space E] [measurable_space F] [normed_group E] [normed_group F] [borel_space E]
   [borel_space F] [complete_space E]
   {f : α → E} {g : E → F} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
   mem_ℒp (g ∘ f) p μ ↔ mem_ℒp f p μ :=
-begin
-  have := ae_measurable_comp_iff_of_closed_embedding g (hg'.closed_embedding hg.uniform_continuous),
-  split,
-  { assume H,
-    have A : ∀ᵐ x ∂μ, ∥f x∥ ≤ K' * ∥g (f x)∥,
-    { apply filter.eventually_of_forall (λ x, _),
-      rw [← dist_zero_right, ← dist_zero_right, ← g0],
-      apply hg'.le_mul_dist },
-    exact H.of_le_mul (this.1 H.ae_measurable) A },
-  { assume H,
-    have A : ∀ᵐ x ∂μ, ∥g (f x)∥ ≤ K * ∥f x∥,
-    { apply filter.eventually_of_forall (λ x, _),
-      rw [← dist_zero_right, ← dist_zero_right, ← g0],
-      apply hg.dist_le_mul },
-    exact H.of_le_mul (this.2 H.ae_measurable) A }
-end
+⟨λ h, h.of_comp_antilipschitz_with hg.uniform_continuous hg' g0, λ h, hg.comp_mem_ℒp g0 h⟩
 
 /-- When `g` is a Lipschitz function sending `0` to `0` and `f` is in `Lp`, then `g ∘ f` is well
 defined as an element of `Lp`. -/
@@ -1803,6 +1814,34 @@ lemma coe_fn_comp_Lp' (L : E →L[𝕜] F) (f : Lp E p μ) :
   L.comp_Lp f =ᵐ[μ] λ a, L (f a) :=
 L.coe_fn_comp_Lp f
 
+lemma comp_mem_ℒp (L : E →L[𝕜] F) (f : Lp E p μ) : mem_ℒp (L ∘ f) p μ :=
+(Lp.mem_ℒp (L.comp_Lp f)).ae_eq (L.coe_fn_comp_Lp' f)
+
+lemma comp_mem_ℒp' (L : E →L[𝕜] F) {f : α → E} (hf : mem_ℒp f p μ) : mem_ℒp (L ∘ f) p μ :=
+(L.comp_mem_ℒp (hf.to_Lp f)).ae_eq (eventually_eq.fun_comp (hf.coe_fn_to_Lp) _)
+
+section is_R_or_C
+
+variables {K : Type*} [is_R_or_C K] [measurable_space K] [borel_space K]
+
+lemma _root_.measure_theory.mem_ℒp.of_real
+  {f : α → ℝ} (hf : mem_ℒp f p μ) : mem_ℒp (λ x, (f x : K)) p μ :=
+(@is_R_or_C.of_real_clm K _).comp_mem_ℒp' hf
+
+lemma _root_.measure_theory.mem_ℒp_re_im_iff {f : α → K} :
+  mem_ℒp (λ x, is_R_or_C.re (f x)) p μ ∧ mem_ℒp (λ x, is_R_or_C.im (f x)) p μ ↔
+  mem_ℒp f p μ :=
+begin
+  refine ⟨_, λ hf, ⟨hf.re, hf.im⟩⟩,
+  rintro ⟨hre, him⟩,
+  convert hre.of_real.add (him.of_real.const_mul is_R_or_C.I),
+  { ext1 x,
+    rw [pi.add_apply, mul_comm, is_R_or_C.re_add_im] },
+  all_goals { apply_instance }
+end
+
+end is_R_or_C
+
 lemma add_comp_Lp (L L' : E →L[𝕜] F) (f : Lp E p μ) :
   (L + L').comp_Lp f = L.comp_Lp f + L'.comp_Lp f :=
 begin

src/measure_theory/function/special_functions.lean

@@ -165,6 +165,38 @@ is_R_or_C.measurable_im.comp_ae_measurable hf
 
 end is_R_or_C_composition
 
+section
+
+variables {α 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α] [measurable_space 𝕜]
+  [borel_space 𝕜] {f : α → 𝕜} {μ : measure_theory.measure α}
+
+@[measurability] lemma is_R_or_C.measurable_of_real : measurable (coe : ℝ → 𝕜) :=
+is_R_or_C.continuous_of_real.measurable
+
+lemma measurable_of_re_im
+  (hre : measurable (λ x, is_R_or_C.re (f x)))
+  (him : measurable (λ x, is_R_or_C.im (f x))) : measurable f :=
+begin
+  convert (is_R_or_C.measurable_of_real.comp hre).add
+    ((is_R_or_C.measurable_of_real.comp him).mul_const is_R_or_C.I),
+  { ext1 x,
+    exact (is_R_or_C.re_add_im _).symm },
+  all_goals { apply_instance },
+end
+
+lemma ae_measurable_of_re_im
+  (hre : ae_measurable (λ x, is_R_or_C.re (f x)) μ)
+  (him : ae_measurable (λ x, is_R_or_C.im (f x)) μ) : ae_measurable f μ :=
+begin
+  convert (is_R_or_C.measurable_of_real.comp_ae_measurable hre).add
+    ((is_R_or_C.measurable_of_real.comp_ae_measurable him).mul_const is_R_or_C.I),
+  { ext1 x,
+    exact (is_R_or_C.re_add_im _).symm },
+  all_goals { apply_instance },
+end
+
+end
+
 section pow_instances
 
 instance complex.has_measurable_pow : has_measurable_pow ℂ ℂ :=

src/measure_theory/integral/set_integral.lean

@@ -837,6 +837,27 @@ lemma integral_im {f : α → 𝕜} (hf : integrable f μ) :
 lemma integral_conj {f : α → 𝕜} : ∫ a, conj (f a) ∂μ = conj ∫ a, f a ∂μ :=
 (@is_R_or_C.conj_lie 𝕜 _).to_linear_isometry.integral_comp_comm f
 
+lemma integral_coe_re_add_coe_im {f : α → 𝕜} (hf : integrable f μ) :
+  ∫ x, (is_R_or_C.re (f x) : 𝕜) ∂μ + ∫ x, is_R_or_C.im (f x) ∂μ * is_R_or_C.I = ∫ x, f x ∂μ :=
+begin
+  rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add],
+  { congr,
+    ext1 x,
+    rw [smul_eq_mul, mul_comm, is_R_or_C.re_add_im] },
+  { exact hf.re.of_real },
+  { exact hf.im.of_real.smul is_R_or_C.I }
+end
+
+lemma integral_re_add_im {f : α → 𝕜} (hf : integrable f μ) :
+  ((∫ x, is_R_or_C.re (f x) ∂μ : ℝ) : 𝕜) + (∫ x, is_R_or_C.im (f x) ∂μ : ℝ) * is_R_or_C.I =
+  ∫ x, f x ∂μ :=
+by { rw [← integral_of_real, ← integral_of_real, integral_coe_re_add_coe_im hf] }
+
+lemma set_integral_re_add_im {f : α → 𝕜} {i : set α} (hf : integrable_on f i μ) :
+  ((∫ x in i, is_R_or_C.re (f x) ∂μ : ℝ) : 𝕜) +
+  (∫ x in i, is_R_or_C.im (f x) ∂μ : ℝ) * is_R_or_C.I = ∫ x in i, f x ∂μ :=
+integral_re_add_im hf
+
 lemma fst_integral {f : α → E × F} (hf : integrable f μ) :
   (∫ x, f x ∂μ).1 = ∫ x, (f x).1 ∂μ :=
 ((continuous_linear_map.fst ℝ E F).integral_comp_comm hf).symm

test/measurability.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import measure_theory.tactic
-import measure_theory.function.lp_space
+import measure_theory.function.special_functions
 
 open_locale big_operators ennreal
 
@@ -74,3 +74,6 @@ example [topological_space α] [borel_space α] [normed_group β] [borel_space 
   (hF : ∀ i, measurable (F i)) :
   ae_measurable (∑ i in s, (λ x, F (i+1) x - F i x)) μ :=
 by measurability
+
+example : measurable (λ x : ℝ, real.exp (2 * inner x 3)) :=
+by measurability