Integrability in WithLp

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

theorem MeasureTheory.memLp_piLp_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} : MemLp f p μ ↔ ∀ (i : ι), MemLp (fun (x : X) => (f x).ofLp i) p μ

theorem MeasureTheory.MemLp.eval_piLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} : MemLp f p μ → ∀ (i : ι), MemLp (fun (x : X) => (f x).ofLp i) p μ

Alias of the forward direction of MeasureTheory.memLp_piLp_iff.

theorem MeasureTheory.MemLp.of_eval_piLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} : (∀ (i : ι), MemLp (fun (x : X) => (f x).ofLp i) p μ) → MemLp f p μ

Alias of the reverse direction of MeasureTheory.memLp_piLp_iff.

theorem MeasureTheory.integrable_piLp_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} : Integrable f μ ↔ ∀ (i : ι), Integrable (fun (x : X) => (f x).ofLp i) μ

theorem MeasureTheory.Integrable.eval_piLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} : Integrable f μ → ∀ (i : ι), Integrable (fun (x : X) => (f x).ofLp i) μ

Alias of the forward direction of MeasureTheory.integrable_piLp_iff.

theorem MeasureTheory.Integrable.of_eval_piLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} : (∀ (i : ι), Integrable (fun (x : X) => (f x).ofLp i) μ) → Integrable f μ

Alias of the reverse direction of MeasureTheory.integrable_piLp_iff.

theorem MeasureTheory.eval_integral_piLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] {f : X → PiLp q E} [(i : ι) → NormedSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)] (hf : ∀ (i : ι), Integrable (fun (x : X) => (f x).ofLp i) μ) (i : ι) : (∫ (x : X), f x ∂μ).ofLp i = ∫ (x : X), (f x).ofLp i ∂μ

theorem MeasureTheory.memLp_prodLp_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} : MemLp f p μ ↔ MemLp (fun (x : X) => (f x).fst) p μ ∧ MemLp (fun (x : X) => (f x).snd) p μ

theorem MeasureTheory.MemLp.prodLp_fst {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} (h : MemLp f p μ) : MemLp (fun (x : X) => (f x).fst) p μ

theorem MeasureTheory.MemLp.prodLp_snd {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} (h : MemLp f p μ) : MemLp (fun (x : X) => (f x).snd) p μ

theorem MeasureTheory.MemLp.of_fst_of_snd_prodLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {p q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} : MemLp (fun (x : X) => (f x).fst) p μ ∧ MemLp (fun (x : X) => (f x).snd) p μ → MemLp f p μ

Alias of the reverse direction of MeasureTheory.memLp_prodLp_iff.

theorem MeasureTheory.integrable_prodLp_iff {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} : Integrable f μ ↔ Integrable (fun (x : X) => (f x).fst) μ ∧ Integrable (fun (x : X) => (f x).snd) μ

theorem MeasureTheory.Integrable.prodLp_fst {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} (h : Integrable f μ) : Integrable (fun (x : X) => (f x).fst) μ

theorem MeasureTheory.Integrable.prodLp_snd {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} (h : Integrable f μ) : Integrable (fun (x : X) => (f x).snd) μ

theorem MeasureTheory.Integrable.of_fst_of_snd_prodLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} : Integrable (fun (x : X) => (f x).fst) μ ∧ Integrable (fun (x : X) => (f x).snd) μ → Integrable f μ

Alias of the reverse direction of MeasureTheory.integrable_prodLp_iff.

theorem MeasureTheory.fst_integral_withLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace F] (hf : Integrable f μ) : (∫ (x : X), f x ∂μ).fst = ∫ (x : X), (f x).fst ∂μ

theorem MeasureTheory.snd_integral_withLp {X : Type u_1} {mX : MeasurableSpace X} {μ : Measure X} {q : ENNReal} [Fact (1 ≤ q)] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : X → WithLp q (E × F)} [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace E] (hf : Integrable f μ) : (∫ (x : X), f x ∂μ).snd = ∫ (x : X), (f x).snd ∂μ