From e17e9eaca0d36de0f1219ddcfe24f2a6bb2b7093 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <Remydegenne@gmail.com>
Date: Thu, 12 Aug 2021 15:02:54 +0000
Subject: [PATCH] feat(measure_theory/lp_space): add mem_Lp and integrable
 lemmas for is_R_or_C.re/im and inner product with a constant (#8615)

---
 src/data/complex/is_R_or_C.lean           |  6 ++++
 src/measure_theory/function/l1_space.lean | 27 ++++++++++++++++
 src/measure_theory/function/lp_space.lean | 38 +++++++++++++++++++++++
 3 files changed, 71 insertions(+)

diff --git a/src/data/complex/is_R_or_C.lean b/src/data/complex/is_R_or_C.lean
index 1c15c35e76cae..cb6e4ffa762f9 100644
--- a/src/data/complex/is_R_or_C.lean
+++ b/src/data/complex/is_R_or_C.lean
@@ -487,6 +487,12 @@ by rw [mul_self_le_mul_self_iff (_root_.abs_nonneg (im z)) (abs_nonneg _),
        abs_mul_abs_self, mul_self_abs];
    apply im_sq_le_norm_sq
 
+lemma norm_re_le_norm (z : K) : ∥re z∥ ≤ ∥z∥ :=
+by { rw [is_R_or_C.norm_eq_abs, real.norm_eq_abs], exact is_R_or_C.abs_re_le_abs _, }
+
+lemma norm_im_le_norm (z : K) : ∥im z∥ ≤ ∥z∥ :=
+by { rw [is_R_or_C.norm_eq_abs, real.norm_eq_abs], exact is_R_or_C.abs_im_le_abs _, }
+
 lemma re_le_abs (z : K) : re z ≤ abs z :=
 (abs_le.1 (abs_re_le_abs _)).2
 
diff --git a/src/measure_theory/function/l1_space.lean b/src/measure_theory/function/l1_space.lean
index 3ac6fb9076d4b..a97320ad8dbce 100644
--- a/src/measure_theory/function/l1_space.lean
+++ b/src/measure_theory/function/l1_space.lean
@@ -597,6 +597,33 @@ begin
 end
 end normed_space_over_complete_field
 
+section is_R_or_C
+variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜}
+
+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, }
+
+lemma integrable.im (hf : integrable f μ) : integrable (λ x, is_R_or_C.im (f x)) μ :=
+by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.im, }
+
+end is_R_or_C
+
+section inner_product
+variables {𝕜 E : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
+  [inner_product_space 𝕜 E]
+  [measurable_space E] [opens_measurable_space E] [second_countable_topology E]
+  {f : α → E}
+
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
+
+lemma integrable.const_inner (c : E) (hf : integrable f μ) : integrable (λ x, ⟪c, f x⟫) μ :=
+by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.const_inner c, }
+
+lemma integrable.inner_const (hf : integrable f μ) (c : E) : integrable (λ x, ⟪f x, c⟫) μ :=
+by { rw ← mem_ℒp_one_iff_integrable at hf ⊢, exact hf.inner_const c, }
+
+end inner_product
+
 section trim
 
 variables {H : Type*} [normed_group H] [measurable_space H] [opens_measurable_space H]
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
index dd56d771eddfd..4debb965e9664 100644
--- a/src/measure_theory/function/lp_space.lean
+++ b/src/measure_theory/function/lp_space.lean
@@ -984,6 +984,44 @@ end
 
 end monotonicity
 
+section is_R_or_C
+variables {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [opens_measurable_space 𝕜] {f : α → 𝕜}
+
+lemma mem_ℒp.re (hf : mem_ℒp f p μ) : mem_ℒp (λ x, is_R_or_C.re (f x)) p μ :=
+begin
+  have : ∀ x, ∥is_R_or_C.re (f x)∥ ≤ 1 * ∥f x∥,
+    by { intro x, rw one_mul, exact is_R_or_C.norm_re_le_norm (f x), },
+  exact hf.of_le_mul hf.1.re (eventually_of_forall this),
+end
+
+lemma mem_ℒp.im (hf : mem_ℒp f p μ) : mem_ℒp (λ x, is_R_or_C.im (f x)) p μ :=
+begin
+  have : ∀ x, ∥is_R_or_C.im (f x)∥ ≤ 1 * ∥f x∥,
+    by { intro x, rw one_mul, exact is_R_or_C.norm_im_le_norm (f x), },
+  exact hf.of_le_mul hf.1.im (eventually_of_forall this),
+end
+
+end is_R_or_C
+
+section inner_product
+variables {E' 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
+  [inner_product_space 𝕜 E']
+  [measurable_space E'] [opens_measurable_space E'] [second_countable_topology E']
+
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 E' _ x y
+
+lemma mem_ℒp.const_inner (c : E') {f : α → E'} (hf : mem_ℒp f p μ) :
+  mem_ℒp (λ a, ⟪c, f a⟫) p μ :=
+hf.of_le_mul (ae_measurable.inner ae_measurable_const hf.1)
+  (eventually_of_forall (λ x, norm_inner_le_norm _ _))
+
+lemma mem_ℒp.inner_const {f : α → E'} (hf : mem_ℒp f p μ) (c : E') :
+  mem_ℒp (λ a, ⟪f a, c⟫) p μ :=
+hf.of_le_mul (ae_measurable.inner hf.1 ae_measurable_const)
+  (eventually_of_forall (λ x, by { rw mul_comm, exact norm_inner_le_norm _ _, }))
+
+end inner_product
+
 end ℒp
 
 /-!