Uniform integrability #
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 μ
theorem
MeasureTheory.uniformIntegrable_of_dominated
{ι : Type u_1}
{Ω : Type u_3}
{E : Type u_4}
{F : Type u_5}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{X : ι → Ω → E}
{Y : ι → Ω → F}
{p : ENNReal}
(hp : 1 ≤ p)
(hY : UniformIntegrable Y p μ)
(mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ)
(hX : ∀ (i : ι), ∃ (j : ι), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ ≤ ‖Y j ω‖)
:
UniformIntegrable X p μ
theorem
MeasureTheory.UniformIntegrable.norm
{ι : Type u_1}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
[NormedAddCommGroup E]
{X : ι → Ω → E}
{p : ENNReal}
(hp : 1 ≤ p)
(hY : UniformIntegrable X p μ)
:
UniformIntegrable (fun (t : ι) (ω : Ω) => ‖X t ω‖) p μ
theorem
MeasureTheory.uniformIntegrable_iff_norm
{ι : Type u_1}
{Ω : Type u_3}
{E : Type u_4}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
[NormedAddCommGroup E]
{X : ι → Ω → E}
{p : ENNReal}
(hp : 1 ≤ p)
(mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ)
:
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)
(hY : MemLp Y p μ)
(mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ)
(hX : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ ≤ Y ω)
:
UniformIntegrable X p μ
theorem
MeasureTheory.UniformIntegrable.condExp'
{ι : Type u_1}
{κ : Type u_2}
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{X : ι → Ω → ℝ}
(hX : UniformIntegrable X 1 μ)
{𝓕 : κ → MeasurableSpace Ω}
(h𝓕 : ∀ (i : κ), 𝓕 i ≤ mΩ)
:
UniformIntegrable (fun (p : ι × κ) => μ[X p.1|𝓕 p.2]) 1 μ
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 μ
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 μ
theorem
MeasureTheory.UniformIntegrable.condExp
{ι : Type u_1}
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{X : ι → Ω → ℝ}
(hX : UniformIntegrable X 1 μ)
{𝓕 : ι → MeasurableSpace Ω}
(h𝓕 : ∀ (i : ι), 𝓕 i ≤ mΩ)
:
UniformIntegrable (fun (i : ι) => μ[X i|𝓕 i]) 1 μ
theorem
MeasureTheory.Martingale.ae_eq_condExp_of_isStoppingTime
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{ι : Type u_6}
[LinearOrder ι]
[OrderBot ι]
[Countable ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{𝓕 : Filtration ι mΩ}
[SigmaFiniteFiltration μ 𝓕]
{X : ι → Ω → ℝ}
(hX : Martingale X 𝓕 μ)
{τ : Ω → WithTop ι}
(hτ : IsStoppingTime 𝓕 τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n)
:
theorem
MeasureTheory.Martingale.uniformIntegrable_stoppedValue
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{ι : Type u_6}
[LinearOrder ι]
[OrderBot ι]
[Countable ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{X : ι → Ω → ℝ}
{𝓕 : Filtration ι mΩ}
[SigmaFiniteFiltration μ 𝓕]
(hX : Martingale X 𝓕 μ)
(τ : ℕ → Ω → WithTop ι)
(hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i))
{n : ι}
(hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n)
:
UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ
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 μ
theorem
MeasureTheory.Martingale.uniformIntegrable_stoppedValue_of_countable_range
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{ι : Type u_6}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{X : ι → Ω → ℝ}
{𝓕 : Filtration ι mΩ}
[SigmaFiniteFiltration μ 𝓕]
(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 μ
theorem
MeasureTheory.Martingale.integrable_stoppedValue_of_countable_range
{Ω : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
{ι : Type u_6}
[LinearOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{X : ι → Ω → ℝ}
{𝓕 : Filtration ι mΩ}
[SigmaFiniteFiltration μ 𝓕]
(hX : Martingale X 𝓕 μ)
(τ : Ω → WithTop ι)
(hτ : IsStoppingTime 𝓕 τ)
{n : ι}
(hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n)
(hτ_countable : (Set.range τ).Countable)
:
Integrable (stoppedValue X τ) μ
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)
:
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) μ)
:
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) μ)
:
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 μ
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 μ
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 μ
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 μ