# Integrability in a product space #

We prove that `f : X → Π i, E i` is in `Lᵖ` if and only if for all `i`, `f · i` is in `Lᵖ`. We do the same for `f : X → (E × F)`.

source
theorem MeasureTheory.memLp_pi_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} :
MemLp f p μ ↔ ∀ (i : ι), MemLp (fun (x : X) => f x i) p μ
source
theorem MeasureTheory.MemLp.of_eval {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} :
(∀ (i : ι), MemLp (fun (x : X) => f x i) p μ) → MemLp f p μ

Alias of the reverse direction of `MeasureTheory.memLp_pi_iff`.

source
theorem MeasureTheory.MemLp.eval {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} :
MemLp f p μ → ∀ (i : ι), MemLp (fun (x : X) => f x i) p μ

Alias of the forward direction of `MeasureTheory.memLp_pi_iff`.

source
theorem MeasureTheory.integrable_pi_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} :
Integrable f μ ↔ ∀ (i : ι), Integrable (fun (x : X) => f x i) μ
source
theorem MeasureTheory.Integrable.of_eval {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} :
(∀ (i : ι), Integrable (fun (x : X) => f x i) μ) → Integrable f μ

Alias of the reverse direction of `MeasureTheory.integrable_pi_iff`.

source
theorem MeasureTheory.Integrable.eval {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} :
Integrable f μ → ∀ (i : ι), Integrable (fun (x : X) => f x i) μ

Alias of the forward direction of `MeasureTheory.integrable_pi_iff`.

source
theorem MeasureTheory.eval_integral {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i} [(i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)] (hf : ∀ (i : ι), Integrable (fun (x : X) => f x i) μ) (i : ι) :
(∫ (x : X), f x ∂μ) i = ∫ (x : X), f x i ∂μ
source
theorem MeasureTheory.memLp_prod_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → E × F} :
MemLp f p μ ↔ MemLp (fun (x : X) => (f x).1) p μ ∧ MemLp (fun (x : X) => (f x).2) p μ
source
theorem MeasureTheory.MemLp.fst {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → E × F} (h : MemLp f p μ) :
MemLp (fun (x : X) => (f x).1) p μ
source
theorem MeasureTheory.MemLp.snd {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → E × F} (h : MemLp f p μ) :
MemLp (fun (x : X) => (f x).2) p μ
source
theorem MeasureTheory.MemLp.of_fst_snd {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → E × F} :
MemLp (fun (x : X) => (f x).1) p μ ∧ MemLp (fun (x : X) => (f x).2) p μ → MemLp f p μ

Alias of the reverse direction of `MeasureTheory.memLp_prod_iff`.