Documentation

Mathlib.MeasureTheory.SpecificCodomains.WithLp

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).

source
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 i) p μ
source
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 i) p μ

Alias of the forward direction of MeasureTheory.memLp_piLp_iff.

source
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 i) p μ) → MemLp f p μ

Alias of the reverse direction of MeasureTheory.memLp_piLp_iff.

source
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 i) μ
source
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 i) μ

Alias of the forward direction of MeasureTheory.integrable_piLp_iff.

source
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 i) μ) → Integrable f μ

Alias of the reverse direction of MeasureTheory.integrable_piLp_iff.

source
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 i) μ) (i : ι) :
(∫ (x : X), f x ∂μ) i = ∫ (x : X), f x i ∂μ
source
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).1) p μ ∧ MemLp (fun (x : X) => (f x).2) p μ
source
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).1) p μ
source
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).2) p μ
source
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).1) p μ ∧ MemLp (fun (x : X) => (f x).2) p μ → MemLp f p μ

Alias of the reverse direction of MeasureTheory.memLp_prodLp_iff.

source
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).1) μ ∧ Integrable (fun (x : X) => (f x).2) μ
source
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).1) μ
source
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).2) μ
source
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).1) μ ∧ Integrable (fun (x : X) => (f x).2) μ → Integrable f μ

Alias of the reverse direction of MeasureTheory.integrable_prodLp_iff.

source
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 ∂μ).1 = ∫ (x : X), (f x).1 ∂μ
source
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 ∂μ).2 = ∫ (x : X), (f x).2 ∂μ