Doob's Lᵖ inequality

theorem ProbabilityTheory.maximal_ineq_countable {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {Y : ι → Ω → ℝ} [Countable ι] [MeasureTheory.IsFiniteMeasure P] (hsub : MeasureTheory.Submartingale Y 𝓕 P) (hnonneg : 0 ≤ Y) (ε : NNReal) (n : ι) : ε • P {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), Y i ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), Y i ω}, Y n ω ∂P)

theorem ProbabilityTheory.maximal_ineq_norm_countable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [Countable ι] [MeasureTheory.IsFiniteMeasure P] (hsub : MeasureTheory.Martingale X 𝓕 P) (ε : NNReal) (n : ι) : ε • P {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), ‖X i ω‖} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), ‖X i ω‖}, ‖X n ω‖ ∂P)

theorem ProbabilityTheory.maximal_ineq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {Y : ι → Ω → ℝ} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P] (hsub : MeasureTheory.Submartingale Y 𝓕 P) (hnonneg : 0 ≤ Y) (ε : NNReal) (n : ι) : ε • P {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), Y i ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), Y i ω}, Y n ω ∂P)

theorem ProbabilityTheory.maximal_ineq_norm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P] (hsub : MeasureTheory.Martingale X 𝓕 P) (ε : NNReal) (n : ι) : ε • P {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), ‖X i ω‖} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑ε ≤ ⨆ (i : ι), ⨆ (_ : i ≤ n), ‖X i ω‖}, ‖X n ω‖ ∂P)