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 : ℕ) : ε • P.real {ω : Ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => f k ω} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => f k ω}, f n ω ∂P

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) : ε • P.real {ω : Ω | ↑ε ≤ J.sup' ⋯ fun (i : ι) => Y i ω} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ J.sup' ⋯ fun (i : ι) => Y i ω}, Y n ω ∂P

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 : ι) : ε • P.real {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), ENNReal.ofReal (Y i ω)} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), ENNReal.ofReal (Y i ω)}, Y n ω ∂P

theorem ENNReal.ofReal_smul {a : NNReal} {b : ℝ} : ENNReal.ofReal (a • b) = a • ENNReal.ofReal b

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 : ι) : ∀ᵐ (ω : Ω) ∂P, ⨆ (i : ι), ⨆ (_ : i ≤ n), ENNReal.ofReal (Y i ω) ≠ ⊤

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 : ι) : ∀ᵐ (ω : Ω) ∂P, BddAbove ((fun (i : ι) => Y i ω) '' Set.Iic 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 : ι) : ε • P.real {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), Y (↑i) ω} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), Y (↑i) ω}, Y n ω ∂P

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 : ι) : ε • P.real {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), ‖X (↑i) ω‖} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), ‖X (↑i) ω‖}, ‖X n ω‖ ∂P

@[simp]

theorem ProbabilityTheory.preimage_iSup {Ω : Type u_2} {ι : Type u_4} {β : Type u_5} [CompleteLinearOrder β] (f : ι → Ω → β) (b : β) : (⨆ (i : ι), f i) ⁻¹' Set.Ioi b = ⋃ (i : ι), f i ⁻¹' Set.Ioi b

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 : ∀ (ω : Ω), IsRightContinuous 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 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : ↑ε * P.real {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), ENNReal.ofReal (Y (↑i) ω)} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), ENNReal.ofReal (Y (↑i) ω)}, Y n ω ∂P

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 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : ∀ᵐ (ω : Ω) ∂P, ⨆ (i : ↑(Set.Iic n)), ENNReal.ofReal (Y (↑i) ω) ≠ ⊤

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 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : ↑ε * P.real {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), Y (↑i) ω} ≤ ∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ↑(Set.Iic n)), Y (↑i) ω}, Y n ω ∂P

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 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : ε * P.real {ω : Ω | ε ≤ ⨆ (i : ↑(Set.Iic n)), Y (↑i) ω} ≤ ∫ (ω : Ω) in {ω : Ω | ε ≤ ⨆ (i : ↑(Set.Iic n)), Y (↑i) ω}, Y n ω ∂P

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 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) : ε • P.real {ω : Ω | ε ≤ ⨆ (i : ↑(Set.Iic n)), ‖X (↑i) ω‖} ≤ ∫ (ω : Ω) in {ω : Ω | ε ≤ ⨆ (i : ↑(Set.Iic n)), ‖X (↑i) ω‖}, ‖X n ω‖ ∂P

theorem ProbabilityTheory.integral_iSup_le_norm_rpow_le {ι : 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) (T : ι) (hX_cont : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) {p : ℝ} (hp : 1 < p) : ∫⁻ (ω : Ω), (⨆ (t : ι), ⨆ (_ : t ≤ T), ‖X t ω‖ₑ) ^ p ∂P ≤ ENNReal.ofReal ((p / (p - 1)) ^ p) * ∫⁻ (ω : Ω), ‖X T ω‖ₑ ^ p ∂P

theorem ProbabilityTheory.integral_iSup_norm_rpow_le {ι : 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) (hX_cont : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) {p : ℝ} (hp : 1 < p) : ∫⁻ (ω : Ω), (⨆ (t : ι), ‖X t ω‖ₑ) ^ p ∂P ≤ ENNReal.ofReal ((p / (p - 1)) ^ p) * ⨆ (t : ι), ∫⁻ (ω : Ω), ‖X t ω‖ₑ ^ p ∂P