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