feat(measure_theory/lp_space): add mem_Lp and integrable lemmas for i…

…s_R_or_C.re/im and inner product with a constant (#8615)

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
 

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]

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
 
 /-!