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.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}
:
Alias of the reverse direction of MeasureTheory.memLp_piLp_iff.
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}
:
Alias of the forward 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}
:
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.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.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 : ι)
:
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)}
:
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 μ)
:
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 μ)
:
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)}
:
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)}
:
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 μ)
:
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 μ)
: