Doob's Lᵖ inequality #
theorem
ProbabilityTheory.maximal_ineq'
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{𝓕 : MeasureTheory.Filtration ℕ mΩ}
{f : ℕ → Ω → ℝ}
(hsub : MeasureTheory.Submartingale f 𝓕 P)
(hnonneg : 0 ≤ f)
(ε : NNReal)
(n : ℕ)
:
theorem
ProbabilityTheory.maximal_ineq_finset
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[MeasureTheory.IsFiniteMeasure P]
(hsub : MeasureTheory.Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(ε : NNReal)
{n : ι}
{J : Finset ι}
(hJn : ∀ i ∈ J, i ≤ n)
(hnJ : n ∈ J)
:
Auxiliary lemma for maximal_ineq_countable where the index set is a Finset.
theorem
tendsto_inv_add_atTop_nhds_zero_nat
{𝕜 : Type u_4}
[DivisionSemiring 𝕜]
[CharZero 𝕜]
[TopologicalSpace 𝕜]
[ContinuousSMul ℚ≥0 𝕜]
:
Filter.Tendsto (fun (n : ℕ) => (↑n + 1)⁻¹) Filter.atTop (nhds 0)
theorem
ProbabilityTheory.maximal_ineq_countable_ennreal
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[MeasureTheory.IsFiniteMeasure P]
[Countable ι]
(hsub : MeasureTheory.Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(ε : NNReal)
(n : ι)
:
theorem
MeasureTheory.Submartingale.iSup_ofReal_ne_top
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[IsFiniteMeasure P]
[Countable ι]
(hsub : Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(n : ι)
:
Alternative form of Submartingale.ae_bddAbove.
theorem
MeasureTheory.Submartingale.ae_bddAbove_Iic
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[IsFiniteMeasure P]
[Countable ι]
(hsub : Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(n : ι)
:
Doob's maximal inequality implies that the supremum process of a nonnegative submartingale is a.s. bounded.
theorem
ProbabilityTheory.maximal_ineq_countable
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[MeasureTheory.IsFiniteMeasure P]
[Countable ι]
(hsub : MeasureTheory.Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(ε : NNReal)
(n : ι)
:
Doob's maximal inequality for a countable index set.
theorem
ProbabilityTheory.maximal_ineq_norm_countable
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.IsFiniteMeasure P]
[Countable ι]
(hmar : MeasureTheory.Martingale X 𝓕 P)
(ε : NNReal)
(n : ι)
:
theorem
ProbabilityTheory.measurable_iSup_of_rightContinuous
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
{β : Type u_4}
{f : ι → Ω → β}
[TopologicalSpace β]
[MeasurableSpace β]
[BorelSpace β]
[CompleteLinearOrder β]
[OrderTopology β]
[SecondCountableTopology β]
(hX_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => f x ω)
(hm : ∀ (t : ι), Measurable (f t))
:
Measurable (⨆ (i : ι), f i)
theorem
ProbabilityTheory.maximal_ineq_ennreal
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[MeasureTheory.IsFiniteMeasure P]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hsub : MeasureTheory.Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(ε : NNReal)
(n : ι)
(hY_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => Y x ω)
:
theorem
MeasureTheory.Submartingale.rightCont_iSup_ofReal_ne_top
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : Measure Ω}
{𝓕 : Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[IsFiniteMeasure P]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hsub : Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(n : ι)
(hY_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => Y x ω)
:
theorem
ProbabilityTheory.maximal_ineq_nonneg
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[MeasureTheory.IsFiniteMeasure P]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hsub : MeasureTheory.Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(ε : NNReal)
(n : ι)
(hY_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => Y x ω)
:
theorem
ProbabilityTheory.maximal_ineq
{ι : Type u_1}
{Ω : Type u_2}
[LinearOrder ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓕 : MeasureTheory.Filtration ι mΩ}
{Y : ι → Ω → ℝ}
[MeasureTheory.IsFiniteMeasure P]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hsub : MeasureTheory.Submartingale Y 𝓕 P)
(hnonneg : 0 ≤ Y)
(ε : ℝ)
(n : ι)
(hY_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => Y x ω)
:
theorem
ProbabilityTheory.maximal_ineq_norm
{ι : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[LinearOrder ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → E}
{𝓕 : MeasureTheory.Filtration ι mΩ}
[MeasureTheory.IsFiniteMeasure P]
[TopologicalSpace ι]
[OrderTopology ι]
[SecondCountableTopology ι]
(hmar : MeasureTheory.Martingale X 𝓕 P)
(ε : ℝ)
(n : ι)
(hX_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω)
: