Maximal inequality for real quasimartingales

noncomputable def ProbabilityTheory.finIdx {ι : Type u_1} [LinearOrder ι] (F : Finset ι) (t : ι) : ℕ → ι

The monotone enumeration of a finite set of times, extended by the constant t at indices beyond #F.

Equations

• ProbabilityTheory.finIdx F t k = if h : k < F.card then ↑((F.orderIsoOfFin ⋯) ⟨k, h⟩) else t

theorem ProbabilityTheory.finIdx_mem {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} {k : ℕ} (h : k < F.card) : finIdx F t k ∈ F

theorem ProbabilityTheory.finIdx_eq_of_card_le {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} {k : ℕ} (h : F.card ≤ k) : finIdx F t k = t

theorem ProbabilityTheory.finIdx_le {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} (hF : ∀ s ∈ F, s ≤ t) (k : ℕ) : finIdx F t k ≤ t

theorem ProbabilityTheory.finIdx_lt_of_lt {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} {k l : ℕ} (hkl : k < l) (hl : l < F.card) : finIdx F t k < finIdx F t l

theorem ProbabilityTheory.finIdx_lt_finIdx_iff {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} {k l : ℕ} (hk : k < F.card) (hl : l < F.card) : finIdx F t k < finIdx F t l ↔ k < l

theorem ProbabilityTheory.finIdx_monotone {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} (hF : ∀ s ∈ F, s ≤ t) : Monotone (finIdx F t)

theorem ProbabilityTheory.exists_finIdx_eq {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t s : ι} (hs : s ∈ F) : ∃ k < F.card, finIdx F t k = s

theorem ProbabilityTheory.finIdx_zero_eq_bot {ι : Type u_1} [LinearOrder ι] {F : Finset ι} {t : ι} [OrderBot ι] (hbot : ⊥ ∈ F) : finIdx F t 0 = ⊥

noncomputable def ProbabilityTheory.elemPredSetOfSeq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [OrderBot ι] {idx : ℕ → ι} (hidx : Monotone idx) {W : ℕ → Ω → ℝ} (n : ℕ) (hWmeas : ∀ k < n, Measurable (W k)) : ElementaryPredictableSet 𝓕

Construct an elementary predictable set from a sequence of times and a sequence of measurable functions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ProbabilityTheory.elemPredSetOfSeq_I {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [OrderBot ι] {idx : ℕ → ι} (hidx : Monotone idx) {W : ℕ → Ω → ℝ} (n : ℕ) (hWmeas : ∀ k < n, Measurable (W k)) : (elemPredSetOfSeq hidx n hWmeas).I = Finset.image (fun (k : ℕ) => (idx k, idx (k + 1))) ({k ∈ Finset.range n | idx k < idx (k + 1)})

@[simp]

theorem ProbabilityTheory.elemPredSetOfSeq_set {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [OrderBot ι] {idx : ℕ → ι} (hidx : Monotone idx) {W : ℕ → Ω → ℝ} (n : ℕ) (hWmeas : ∀ k < n, Measurable (W k)) (p : ι × ι) : (elemPredSetOfSeq hidx n hWmeas).set p = if h : ∃ k ∈ {k ∈ Finset.range n | idx k < idx (k + 1)}, (idx k, idx (k + 1)) = p then W h.choose ⁻¹' {1} else ∅

@[simp]

theorem ProbabilityTheory.elemPredSetOfSeq_setBot {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [OrderBot ι] {idx : ℕ → ι} (hidx : Monotone idx) {W : ℕ → Ω → ℝ} (n : ℕ) (hWmeas : ∀ k < n, Measurable (W k)) : (elemPredSetOfSeq hidx n hWmeas).setBot = ∅

theorem ProbabilityTheory.integral_elemPredSetOfSeq {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → ℝ} [OrderBot ι] {t : ι} (n : ℕ) {idx : ℕ → ι} (hidx : Monotone idx) (hidxt : ∀ (k : ℕ), idx k ≤ t) {W : ℕ → Ω → ℝ} (hW01 : ∀ k < n, ∀ (ω : Ω), W k ω = 0 ∨ W k ω = 1) (hWmeas : ∀ k < n, Measurable (W k)) (ω : Ω) : SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) ((elemPredSetOfSeq hidx n hWmeas).indicator 1) X t ω = ∑ k ∈ Finset.range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω)

Upcrossing and alternation bounds along finite time sets

noncomputable def ProbabilityTheory.upcrossingWithinPredSet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → ℝ} {t : ι} [OrderBot ι] (a b : ℝ) (F : Finset ι) (hF : ∀ s ∈ F, s ≤ t) (hX : MeasureTheory.StronglyAdapted 𝓕 X) : ElementaryPredictableSet 𝓕

An elementary predictable set representing upcrossings within a given interval.

Equations

• ProbabilityTheory.upcrossingWithinPredSet a b F hF hX = ProbabilityTheory.elemPredSetOfSeq ⋯ F.card ⋯

theorem ProbabilityTheory.mul_upcrossingsBefore_le_integral_add_posPart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → ℝ} {a b : ℝ} {t : ι} {F : Finset ι} [OrderBot ι] (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hab : a < b) (hF : ∀ s ∈ F, s ≤ t) (ω : Ω) : (b - a) * ↑(MeasureTheory.upcrossingsBefore a b (fun (k : ℕ) (ω : Ω) => X (finIdx F t k) ω) F.card ω) ≤ SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) ((elemPredSetOfSeq ⋯ F.card ⋯).indicator 1) X t ω + (a - X t ω)⁺

theorem ProbabilityTheory.mul_integral_upcrossingsBefore_finIdx_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {a b : ℝ} {t : ι} {F : Finset ι} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Adapted 𝓕 X) (hXint : ∀ (s : ι), MeasureTheory.Integrable (X s) μ) {C : ℝ} (hC : ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ C) (hab : a < b) (hF : ∀ s ∈ F, s ≤ t) : (b - a) * ∫ (ω : Ω), ↑(MeasureTheory.upcrossingsBefore a b (fun (k : ℕ) => X (finIdx F t k)) F.card ω) ∂μ ≤ C + ∫ (ω : Ω), (a - X t ω)⁺ ∂μ

Expectation bound on the number of upcrossings along a finite set of times F ⊆ Iic t, from the boundedness of elementary stochastic integrals at time t.

def ProbabilityTheory.altSet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] (X : ι → Ω → ℝ) (F : Finset ι) (a b : ℝ) (m : ℕ) : Set Ω

The event that X makes m alternations from at most a to at least b at increasing times inside the finite time set F. The levels are non-strict (X ≤ a, b ≤ X) to match the Set.Iic a / Set.Ici b hitting conditions of MeasureTheory.upcrossingsBefore; with this convention altSet coincides with the event of at least m upcrossings (see altSet_eq_upcrossingsBefore).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.altSet_mono {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} {a b : ℝ} {m : ℕ} {F G : Finset ι} (h : F ⊆ G) : altSet X F a b m ⊆ altSet X G a b m

theorem ProbabilityTheory.altSet_mono' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} {a b : ℝ} {F : Finset ι} {m : ℕ} {a' b' : ℝ} (hab : a ≤ a') (hba : b' ≤ b) : altSet X F a b m ⊆ altSet X F a' b' m

theorem ProbabilityTheory.altSet_eq_upcrossingsBefore {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} {a b : ℝ} {t : ι} {F : Finset ι} {m : ℕ} (hab : a < b) : altSet X F a b m = {ω : Ω | m ≤ MeasureTheory.upcrossingsBefore a b (fun (k : ℕ) => X (finIdx F t k)) F.card ω}

altSet X F a b m is exactly the event of at least m upcrossings of [a, b] by the monotone enumeration finIdx F t of F.

theorem ProbabilityTheory.measureReal_altSet_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {a b : ℝ} {t : ι} {F : Finset ι} {m : ℕ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Adapted 𝓕 X) (hXint : ∀ (s : ι), MeasureTheory.Integrable (X s) μ) {C : ℝ} (hC : ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ C) (hab : a < b) (hm : 0 < m) (hF : ∀ s ∈ F, s ≤ t) : μ.real (altSet X F a b m) ≤ (C + ∫ (ω : Ω), (a - X t ω)⁺ ∂μ) / (b - a) / ↑m

Quantitative alternation bound: the probability of m alternations along any finite F ⊆ Iic t is at most K / m with K independent of F and m.

def ProbabilityTheory.infiniteAlt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] (T : Set ι) (t : ι) (X : ι → Ω → ℝ) (a b : ℝ) : Set Ω

The set of outcomes where there are infinitely many alternations of X from below a to above b at times in a set T below t.

Equations

• ProbabilityTheory.infiniteAlt T t X a b = ⋂ (m : ℕ), ⋃ F ∈ {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t}, ProbabilityTheory.altSet X F a b m

theorem ProbabilityTheory.infiniteAlt_mono' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} {a b : ℝ} {t : ι} {T : Set ι} {a' b' : ℝ} (h : a ≤ a') (h' : b' ≤ b) : infiniteAlt T t X a b ⊆ infiniteAlt T t X a' b'

theorem ProbabilityTheory.infiniteAlt_mono'' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} {a b : ℝ} {T : Set ι} {s t : ι} (h : s ≤ t) : infiniteAlt T s X a b ⊆ infiniteAlt T t X a b

Selection of alternating tuples from frequent oscillation

theorem ProbabilityTheory.Ioo_inter_mem_nhdsWithin_inter_Ioi {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} {x d : ι} (hxd : x < d) : Set.Ioo x d ∩ T ∈ nhdsWithin x (T ∩ Set.Ioi x)

theorem ProbabilityTheory.Ioo_inter_mem_nhdsWithin_inter_Iio {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} {x d : ι} (hxd : d < x) : Set.Ioo d x ∩ T ∈ nhdsWithin x (T ∩ Set.Iio x)

theorem ProbabilityTheory.exists_finset_altSet_of_frequently_right {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} {x d : ι} {a b : ℝ} {ω : Ω} (hxd : x < d) (hfa : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Ioi x), X s ω < a) (hfb : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Ioi x), b < X s ω) (m : ℕ) : ∃ (F : Finset ι), ↑F ⊆ T ∩ Set.Ioo x d ∧ ω ∈ altSet X F a b m

theorem ProbabilityTheory.mem_infiniteAlt_of_frequently_right {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} {x d : ι} {a b : ℝ} {ω : Ω} (hxd : x < d) (hfa : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Ioi x), X s ω < a) (hfb : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Ioi x), b < X s ω) : ω ∈ infiniteAlt T d X a b

theorem ProbabilityTheory.exists_finset_altSet_of_frequently_left {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} {x : ι} {a b : ℝ} {ω : Ω} (hfa : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Iio x), X s ω < a) (hfb : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Iio x), b < X s ω) (m : ℕ) : ∃ (F : Finset ι), ↑F ⊆ T ∩ Set.Iio x ∧ ω ∈ altSet X F a b m

theorem ProbabilityTheory.mem_infiniteAlt_of_frequently_left {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {X : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι] {T : Set ι} {x d : ι} {a b : ℝ} {ω : Ω} (hxd : x ≤ d) (hfa : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Iio x), X s ω < a) (hfb : ∃ᶠ (s : ι) in nhdsWithin x (T ∩ Set.Iio x), b < X s ω) : ω ∈ infiniteAlt T d X a b

Maximal inequality along finite time sets

theorem ProbabilityTheory.sum_indicator_mul_sub_eq_stopped'' {Ω : Type u_2} (f : ℕ → Ω → ℝ) (s : Set ℝ) (n : ℕ) (ω : Ω) : ∑ k ∈ Finset.range n, {ω' : Ω | ∀ j ≤ k, f j ω' ∉ s}.indicator 1 ω * (f (k + 1) ω - f k ω) = f (MeasureTheory.hittingBtwn f s 0 n ω) ω - f 0 ω

theorem ProbabilityTheory.sum_indicator_mul_sub_eq_stopped {Ω : Type u_2} (f : ℕ → Ω → ℝ) (lam : ℝ) (n : ℕ) (ω : Ω) : ∑ k ∈ Finset.range n, {ω' : Ω | ∀ j ≤ k, f j ω' ≤ lam}.indicator 1 ω * (f (k + 1) ω - f k ω) = f (MeasureTheory.hittingBtwn f (Set.Ioi lam) 0 n ω) ω - f 0 ω

Discrete stopped telescoping identity: weighting the increments of f by the indicator of "not yet above lam" telescopes to the value at the first time f exceeds lam.

theorem ProbabilityTheory.integrable_sum_weight_increments {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {g : ι → Ω → ℝ} (hgint : ∀ (s : ι), MeasureTheory.Integrable (g s) μ) {n : ℕ} {idx : ℕ → ι} {W : ℕ → Ω → ℝ} (hWmeas : ∀ k < n, MeasureTheory.AEStronglyMeasurable (W k) μ) (hWb : ∀ k < n, ∀ (ω : Ω), ‖W k ω‖ ≤ 1) : MeasureTheory.Integrable (fun (ω : Ω) => ∑ k ∈ Finset.range n, W k ω * (g (idx (k + 1)) ω - g (idx k) ω)) μ

Integrability of bounded-weight increment sums.

theorem ProbabilityTheory.integral_sum_weight_increments_mem_Icc {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {t : ι} [OrderBot ι] (hXint : ∀ (s : ι), MeasureTheory.Integrable (X s) μ) {C : ℝ} (hC : ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ C) {n : ℕ} {idx : ℕ → ι} (hidx : Monotone idx) (hidxt : ∀ (k : ℕ), idx k ≤ t) {W : ℕ → Ω → ℝ} (hW01 : ∀ k < n, ∀ (ω : Ω), W k ω = 0 ∨ W k ω = 1) (hWmeas : ∀ k < n, Measurable (W k)) : ∫ (ω : Ω), ∑ k ∈ Finset.range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω) ∂μ ∈ Set.Icc (-(C + ∫ (ω : Ω), |X (idx n) ω - X (idx 0) ω| ∂μ)) C

Two-sided expectation bound for adapted {0,1}-weighted increment sums of X, from the boundedness of elementary stochastic integrals at time t. The lower bound uses the complementary weights 1 - W.

theorem ProbabilityTheory.mul_measureReal_exists_lt_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {lam : ℝ} [MeasureTheory.IsFiniteMeasure μ] {g : ι → Ω → ℝ} (hg : MeasureTheory.StronglyAdapted 𝓕 g) (hgint : ∀ (s : ι), MeasureTheory.Integrable (g s) μ) {n : ℕ} {idx : ℕ → ι} (hidx : Monotone idx) {K : ℝ} (hK : ∀ (W : ℕ → Ω → ℝ), (∀ k < n, ∀ (ω : Ω), W k ω = 0 ∨ W k ω = 1) → (∀ k < n, Measurable (W k)) → ∫ (ω : Ω), ∑ k ∈ Finset.range n, W k ω * (g (idx (k + 1)) ω - g (idx k) ω) ∂μ ≤ K) : lam * μ.real {ω : Ω | ∃ k ≤ n, lam < g (idx k) ω} ≤ K + ∫ (ω : Ω), |g (idx 0) ω| ∂μ + ∫ (ω : Ω), |g (idx n) ω| ∂μ

One-sided maximal inequality along a finite skeleton for an adapted, integrable process g whose adapted {0,1}-weighted increment sums along idx have expectation at most K.

theorem ProbabilityTheory.measureReal_exists_abs_lt_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {t : ι} {F : Finset ι} {lam : ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hXint : ∀ (s : ι), MeasureTheory.Integrable (X s) μ) {C : ℝ} (hC : ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ C) (hlam : 0 < lam) (hF : ∀ s ∈ F, s ≤ t) : μ.real {ω : Ω | ∃ s ∈ F, lam < |X s ω|} ≤ 2 * (C + ∫ (ω : Ω), |X t ω - X ⊥ ω| ∂μ + ∫ (ω : Ω), |X ⊥ ω| ∂μ + ∫ (ω : Ω), |X t ω| ∂μ) / lam

Maximal inequality: the probability that |X| exceeds lam somewhere on a finite set F ⊆ Iic t is at most K / lam, with K independent of F.

Maximal inequality for countable sets

theorem ProbabilityTheory.countable_setOf_finset_coe_subset {ι : Type u_1} {T : Set ι} (hT : T.Countable) : {F : Finset ι | ↑F ⊆ T}.Countable

theorem ProbabilityTheory.measure_biUnion_altSet_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {T : Set ι} {a b : ℝ} {m : ℕ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hab : a < b) (hm : 0 < m) (hT : T.Countable) (t : ι) : μ (⋃ F ∈ {F : Finset ι | ↑F ⊆ T ∩ Set.Iic t}, altSet X F a b m) ≤ ENNReal.ofReal ((variationBound X 𝓕 μ t + ∫ (ω : Ω), (a - X t ω)⁺ ∂μ) / (b - a) / ↑m)

The union of the alternation events over all finite subsets of a countable set of times below t has measure at most K / ((b - a) * m).

theorem ProbabilityTheory.measure_infiniteAlt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {T : Set ι} {t : ι} {a b : ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hab : a < b) (hT : T.Countable) : μ (infiniteAlt T t X a b) = 0

Almost surely, there is no infinite family of alternations of X from below a to above b at times in a countable set T below t.

theorem ProbabilityTheory.measure_all_infiniteAlt'' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {t : ι} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (T : Set ι) (hT : T.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ (q r : ℝ), q < r → ω ∉ infiniteAlt T t X q r

theorem ProbabilityTheory.measure_all_infiniteAlt {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) {T T' : Set ι} (hT : T.Countable) (hT' : T'.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ d ∈ T', ∀ (q r : ℝ), q < r → ω ∉ infiniteAlt T d X q r

theorem ProbabilityTheory.measure_all_infiniteAlt' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] [Filter.atTop.IsCountablyGenerated] (hX : IsRealQuasimartingale 𝓕 X μ) (T : Set ι) (hT : T.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ (d : ι) (q r : ℝ), q < r → ω ∉ infiniteAlt T d X q r

theorem ProbabilityTheory.measure_exists_abs_gt_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {T : Set ι} {t : ι} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] {ε : ℝ} (hX : IsRealQuasimartingale 𝓕 X μ) (hε : 0 < ε) (hT : T.Countable) : μ {ω : Ω | ∃ s ∈ T ∩ Set.Iic t, ε < |X s ω|} ≤ ENNReal.ofReal (2 * (variationBound X 𝓕 μ t + ∫ (ω : Ω), |X t ω - X ⊥ ω| ∂μ + ∫ (ω : Ω), |X ⊥ ω| ∂μ + ∫ (ω : Ω), |X t ω| ∂μ) / ε)

theorem ProbabilityTheory.ae_exists_bound'' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {T : Set ι} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hT : T.Countable) (t : ι) : ∀ᵐ (ω : Ω) ∂μ, ∃ (M : ℕ), ∀ s' ∈ T ∩ Set.Iic t, |X s' ω| ≤ ↑M + 1

theorem ProbabilityTheory.ae_exists_bound {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {T : Set ι} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] (hX : IsRealQuasimartingale 𝓕 X μ) (hT : T.Countable) {T' : Set ι} (hT' : T'.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ d ∈ T', ∃ (M : ℕ), ∀ s' ∈ T ∩ Set.Iic d, |X s' ω| ≤ ↑M + 1

theorem ProbabilityTheory.ae_exists_bound' {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {T : Set ι} [OrderBot ι] [MeasureTheory.IsFiniteMeasure μ] [Filter.atTop.IsCountablyGenerated] (hX : IsRealQuasimartingale 𝓕 X μ) (hT : T.Countable) : ∀ᵐ (ω : Ω) ∂μ, ∀ (d : ι), ∃ (M : ℕ), ∀ s ∈ T ∩ Set.Iic d, |X s ω| ≤ ↑M + 1