# Uniform integrability #

source
theorem MeasureTheory.UniformIntegrable.add {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X Y : ι → Ω → E} {p : ENNReal} (hp : 1 ≤ p) (hX : UniformIntegrable X p μ) (hY : UniformIntegrable Y p μ) :
UniformIntegrable (X + Y) p μ
source
theorem MeasureTheory.uniformIntegrable_of_dominated {ι : Type u_1} {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {F : Type u_5} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedAddCommGroup F] {X : ι → Ω → E} {Y : κ → Ω → F} {p : ENNReal} (hY : UniformIntegrable Y p μ) (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) (hX : ∀ (i : ι), ∃ (j : κ), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ ≤ ‖Y j ω‖) :
UniformIntegrable X p μ
source
theorem MeasureTheory.UniformIntegrable.norm {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (hY : UniformIntegrable X p μ) :
UniformIntegrable (fun (t : ι) (ω : Ω) => ‖X t ω‖) p μ
source
theorem MeasureTheory.uniformIntegrable_iff_norm {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) :
UniformIntegrable X p μ ↔ UniformIntegrable (fun (t : ι) (ω : Ω) => ‖X t ω‖) p μ
source
theorem MeasureTheory.uniformIntegrable_of_dominated_singleton {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {Y : Ω → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hp_ne_top : p ≠ ⊤) (hY : MemLp Y p μ) (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) (hX : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ ≤ Y ω) :
UniformIntegrable X p μ
source
theorem MeasureTheory.UniformIntegrable.condExp' {ι : Type u_1} {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [IsFiniteMeasure μ] (hX : UniformIntegrable X 1 μ) {𝓕 : κ → MeasurableSpace Ω} (h𝓕 : ∀ (i : κ), 𝓕 i ≤ mΩ) :
UniformIntegrable (fun (p : ι × κ) => μ[X p.1|𝓕 p.2]) 1 μ
source
theorem MeasureTheory.UnifIntegrable.comp {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {κ : Type u_6} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (hX : UnifIntegrable X p μ) (f : κ → ι) :
UnifIntegrable (X ∘ f) p μ
source
theorem MeasureTheory.UniformIntegrable.comp {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {κ : Type u_6} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (hX : UniformIntegrable X p μ) (f : κ → ι) :
UniformIntegrable (X ∘ f) p μ
source
theorem MeasureTheory.UniformIntegrable.condExp {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [IsFiniteMeasure μ] (hX : UniformIntegrable X 1 μ) {𝓕 : ι → MeasurableSpace Ω} (h𝓕 : ∀ (i : ι), 𝓕 i ≤ mΩ) :
UniformIntegrable (fun (i : ι) => μ[X i|𝓕 i]) 1 μ
source
theorem MeasureTheory.Martingale.ae_eq_condExp_of_isStoppingTime {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] {X : ι → Ω → E} (hX : Martingale X 𝓕 μ) {τ : Ω → WithTop ι} (hτ : IsStoppingTime 𝓕 τ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n) :
stoppedValue X τ =ᶠ[ae μ] μ[X n|hτ.measurableSpace]
source
theorem MeasureTheory.Martingale.uniformIntegrable_stoppedValue {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] [IsFiniteMeasure μ] (hX : Martingale X 𝓕 μ) (τ : ℕ → Ω → WithTop ι) (hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i)) {n : ι} (hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n) :
UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ
source
theorem MeasureTheory.Submartingale.uniformIntegrable_stoppedValue {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {X : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] (hX : Submartingale X 𝓕 μ) (τ : ℕ → Ω → WithTop ι) (hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i)) {n : ι} (hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n) :
UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ
source
theorem MeasureTheory.Martingale.uniformIntegrable_stoppedValue_of_countable_range {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] [IsFiniteMeasure μ] (hX : Martingale X 𝓕 μ) (τ : ℕ → Ω → WithTop ι) (hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i)) {n : ι} (hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n) (hτ_countable : ∀ (i : ℕ), (Set.range (τ i)).Countable) :
UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ
source
theorem MeasureTheory.Martingale.integrable_stoppedValue_of_countable_range {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] [IsFiniteMeasure μ] (hX : Martingale X 𝓕 μ) (τ : Ω → WithTop ι) (hτ : IsStoppingTime 𝓕 τ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n) (hτ_countable : (Set.range τ).Countable) :
Integrable (stoppedValue X τ) μ
source
theorem MeasureTheory.TendstoInMeasure.aestronglyMeasurable {α : Type u_7} {β : Type u_8} {ι : Type u_9} {m : MeasurableSpace α} {μ : Measure α} [PseudoEMetricSpace β] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → β} {g : α → β} (hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ) (h_tendsto : TendstoInMeasure μ f u g) :
AEStronglyMeasurable g μ
source
theorem MeasureTheory.seq_tendsto_ae_bounded {α : Type u_7} {β : Type u_8} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : ℕ → α → β} {g : α → β} {C : ENNReal} (p : ENNReal) (bound : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ C) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) :
eLpNorm g p μ ≤ C
source
theorem MeasureTheory.tendstoInMeasure_bounded {α : Type u_7} {β : Type u_8} {ι : Type u_9} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → β} {g : α → β} {C : ENNReal} (p : ENNReal) (bound : ∀ (i : ι), eLpNorm (f i) p μ ≤ C) (h_tendsto : TendstoInMeasure μ f u g) (hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ) :
eLpNorm g p μ ≤ C
source
theorem MeasureTheory.UniformIntegrable.memLp_of_tendstoInMeasure {α : Type u_7} {β : Type u_8} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {fn : ℕ → α → β} {f : α → β} (p : ENNReal) (hUI : UniformIntegrable fn p μ) (htends : TendstoInMeasure μ fn Filter.atTop f) :
MemLp f p μ
source
theorem MeasureTheory.UnifIntegrable.unifIntegrable_of_tendsto_ae {α : Type u_7} {β : Type u_8} {ι : Type u_9} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {fn : ι → α → β} (p : ENNReal) (hUI : UnifIntegrable fn p μ) (hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ) :
UnifIntegrable (fun (f : ↑{g : α → β | ∃ (ni : ℕ → ι), ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fn (ni n) x) Filter.atTop (nhds (g x))}) => ↑f) p μ
source
theorem MeasureTheory.UnifIntegrable.unifIntegrable_of_tendstoInMeasure {α : Type u_7} {β : Type u_8} {ι : Type u_9} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {fn : ι → α → β} (p : ENNReal) (hUI : UnifIntegrable fn p μ) (hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ) :
UnifIntegrable (fun (f : ↑{g : α → β | ∃ (ni : ℕ → ι), TendstoInMeasure μ (fn ∘ ni) Filter.atTop g}) => ↑f) p μ
source
theorem MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendsto_ae {α : Type u_7} {β : Type u_8} {ι : Type u_9} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {fn : ι → α → β} (p : ENNReal) (hUI : UniformIntegrable fn p μ) :
UniformIntegrable (fun (f : ↑{g : α → β | ∃ (ni : ℕ → ι), ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => fn (ni n) x) Filter.atTop (nhds (g x))}) => ↑f) p μ
source
theorem MeasureTheory.UniformIntegrable.uniformIntegrable_of_tendstoInMeasure {α : Type u_7} {β : Type u_8} {ι : Type u_9} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {fn : ι → α → β} (p : ENNReal) (hUI : UniformIntegrable fn p μ) :
UniformIntegrable (fun (f : ↑{g : α → β | ∃ (ni : ℕ → ι), TendstoInMeasure μ (fn ∘ ni) Filter.atTop g}) => ↑f) p μ
source
theorem MeasureTheory.UniformIntegrable.integrable_of_tendstoInMeasure {α : Type u_7} {β : Type u_8} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {fn : ℕ → α → β} {f : α → β} (hUI : UniformIntegrable fn 1 μ) (htends : TendstoInMeasure μ fn Filter.atTop f) :
Integrable f μ