Doob L² maximal inequalities and signed resolvent moments

• Doob's L² maximal inequality E max_{k ≤ n} Y_k² ≤ 4 E Y_n² for nonnegative submartingales (lintegral_sq_sup_le_four_mul_of_submartingale), for real martingales in ℝ≥0∞ and real form (lintegral_sq_sup_enorm_le_four_mul_of_martingale, integral_sq_sup_le_four_mul_of_martingale), and over a compact time interval for right-continuous ℝ≥0-indexed martingales (lintegral_sq_sup_Icc_le_four_mul_of_martingale). All ℝ≥0∞ forms need no integrability.
• For a process Z and bounded k, V with E[∫_s^∞ e^{-t} k(Z_t) dt | F_s] = e^{-s} V(Z_s) (ResolventMarkov): the martingale ∫_0^t e^{-s} k(Z_s) ds + e^{-t} V(Z_t) (martingale_discounted_resolvent) and the second-moment identity E B² = 2 E ∫_0^∞ e^{-2t} k(Z_t) V(Z_t) dt for B = ∫_0^∞ e^{-t} k(Z_t) dt (integral_sq_discountedOccupation), with the bound integral_sq_discountedOccupation_le.

References

• J. L. Doob, Stochastic Processes, Wiley, 1953, Chapter VII.
• O. Kallenberg, Foundations of Modern Probability, 2nd ed., Springer, 2002, Chapters 7 and 19.

theorem BGW.Probability.lintegral_sq_sup_le_four_mul_of_submartingale {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m} {Y : ℕ → Ω → ℝ} (hY : MeasureTheory.Submartingale Y ℱ μ) (hnn : ∀ (k : ℕ) (ω : Ω), 0 ≤ Y k ω) (n : ℕ) : ∫⁻ (ω : Ω), ((Finset.range (n + 1)).sup fun (k : ℕ) => ENNReal.ofReal (Y k ω)) ^ 2 ∂μ ≤ 4 * ∫⁻ (ω : Ω), ENNReal.ofReal (Y n ω) ^ 2 ∂μ

Doob L² maximal inequality, nonnegative submartingale, finite grid.

theorem BGW.Probability.lintegral_sq_sup_enorm_le_four_mul_of_martingale {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m} {M : ℕ → Ω → ℝ} (hM : MeasureTheory.Martingale M ℱ μ) (n : ℕ) : ∫⁻ (ω : Ω), ((Finset.range (n + 1)).sup fun (k : ℕ) => ‖M k ω‖ₑ) ^ 2 ∂μ ≤ 4 * ∫⁻ (ω : Ω), ‖M n ω‖ₑ ^ 2 ∂μ

Doob L² maximal inequality for a real martingale, finite grid.

theorem BGW.Probability.lintegral_sq_sup_finset_le_four_mul_of_martingale {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration NNReal m} {M : NNReal → Ω → ℝ} (hM : MeasureTheory.Martingale M ℱ μ) (T : NNReal) (s : Finset NNReal) (hT : T ∈ s) (hmax : ∀ t ∈ s, t ≤ T) : ∫⁻ (ω : Ω), (s.sup fun (t : NNReal) => ‖M t ω‖ₑ) ^ 2 ∂μ ≤ 4 * ∫⁻ (ω : Ω), ‖M T ω‖ₑ ^ 2 ∂μ

Doob's inequality on an arbitrary finite set with a prescribed upper endpoint.

theorem BGW.Probability.integral_sq_sup_le_four_mul_of_martingale {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m} {M : ℕ → Ω → ℝ} (hM : MeasureTheory.Martingale M ℱ μ) (n : ℕ) (h2 : MeasureTheory.MemLp (M n) 2 μ) : MeasureTheory.Integrable (fun (ω : Ω) => ((Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => |M k ω|) ^ 2) μ ∧ ∫ (ω : Ω), ((Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => |M k ω|) ^ 2 ∂μ ≤ 4 * ∫ (ω : Ω), M n ω ^ 2 ∂μ

Real-valued form when M n ∈ L²: E max_{k ≤ n} M_k² ≤ 4 E M_n².

theorem BGW.Probability.lintegral_sq_sup_Icc_le_four_mul_of_martingale {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration NNReal m} {M : NNReal → Ω → ℝ} (hM : MeasureTheory.Martingale M ℱ μ) (hrc : ∀ (ω : Ω) (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s ω) (Set.Ici t) t) (T : NNReal) : ∫⁻ (ω : Ω), (⨆ t ∈ Set.Icc 0 T, ‖M t ω‖ₑ) ^ 2 ∂μ ≤ 4 * ∫⁻ (ω : Ω), ‖M T ω‖ₑ ^ 2 ∂μ

Compact-time Doob L², right-continuous martingale. For an ℝ≥0-indexed martingale whose paths are right-continuous (every ω), E sup_{t ≤ T} |M_t|² ≤ 4 E |M_T|²; the supremum is a countable one (rationals and T), hence measurable.

noncomputable def BGW.Probability.discountedOccupation {Ω : Type u_1} {E : Type u_2} (Z : NNReal → Ω → E) (k : E → ℝ) (ω : Ω) : ℝ

The discounted occupation B = ∫_0^∞ e^{-t} k(Z_t) dt.

Equations

• BGW.Probability.discountedOccupation Z k ω = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * k (Z t.toNNReal ω)

def BGW.Probability.ResolventMarkov {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_2} (ℱ : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (Z : NNReal → Ω → E) (k V : E → ℝ) : Prop

Resolvent Markov hypothesis: given F_s, the discounted future of k(Z) after s is e^{-s} V(Z_s).

Equations

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

theorem BGW.Probability.martingale_discounted_resolvent {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [MeasurableSpace E] {ℱ : MeasureTheory.Filtration NNReal m} {Z : NNReal → Ω → E} {k V : E → ℝ} (hZ : Measurable fun (p : NNReal × Ω) => Z p.1 p.2) (hk : Measurable k) (hV : Measurable V) (hkb : ∃ (C : ℝ), ∀ (e : E), |k e| ≤ C) (hVb : ∃ (C : ℝ), ∀ (e : E), |V e| ≤ C) (hprogk : MeasureTheory.IsStronglyProgressive ℱ fun (t : NNReal) (ω : Ω) => k (Z t ω)) (hprogV : MeasureTheory.IsStronglyProgressive ℱ fun (t : NNReal) (ω : Ω) => V (Z t ω)) (hM : ResolventMarkov ℱ μ Z k V) : MeasureTheory.Martingale (fun (t : NNReal) (ω : Ω) => (∫ (s : ℝ) in Set.Ioc 0 ↑t, Real.exp (-s) * k (Z s.toNNReal ω)) + Real.exp (-↑t) * V (Z t ω)) ℱ μ

Explicit martingale. Under the resolvent Markov hypothesis, J_t = ∫_0^t e^{-s}k(Z_s)ds + e^{-t}V(Z_t) is a martingale.

theorem BGW.Probability.integral_sq_discountedOccupation {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [MeasurableSpace E] {ℱ : MeasureTheory.Filtration NNReal m} {Z : NNReal → Ω → E} {k V : E → ℝ} (hZ : Measurable fun (p : NNReal × Ω) => Z p.1 p.2) (hk : Measurable k) (hV : Measurable V) (hkb : ∃ (C : ℝ), ∀ (e : E), |k e| ≤ C) (hVb : ∃ (C : ℝ), ∀ (e : E), |V e| ≤ C) (hprogk : MeasureTheory.IsStronglyProgressive ℱ fun (t : NNReal) (ω : Ω) => k (Z t ω)) (hprogV : MeasureTheory.IsStronglyProgressive ℱ fun (t : NNReal) (ω : Ω) => V (Z t ω)) (hM : ResolventMarkov ℱ μ Z k V) : ∫ (ω : Ω), discountedOccupation Z k ω ^ 2 ∂μ = 2 * ∫ (ω : Ω), ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-2 * t) * (k (Z t.toNNReal ω) * V (Z t.toNNReal ω)) ∂μ

Signed second-moment identity: E B² = 2 E ∫_0^∞ e^{-2t} k(Z_t) V(Z_t) dt, with B = discountedOccupation Z k; both sides finite.

theorem BGW.Probability.integral_sq_discountedOccupation_le {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Type u_2} [MeasurableSpace E] {ℱ : MeasureTheory.Filtration NNReal m} {Z : NNReal → Ω → E} {k V : E → ℝ} (hZ : Measurable fun (p : NNReal × Ω) => Z p.1 p.2) (hk : Measurable k) (hV : Measurable V) (hkb : ∃ (C : ℝ), ∀ (e : E), |k e| ≤ C) {D : ℝ} (hD : ∀ (e : E), |V e| ≤ D) (hprogk : MeasureTheory.IsStronglyProgressive ℱ fun (t : NNReal) (ω : Ω) => k (Z t ω)) (hprogV : MeasureTheory.IsStronglyProgressive ℱ fun (t : NNReal) (ω : Ω) => V (Z t ω)) (hM : ResolventMarkov ℱ μ Z k V) : ∫ (ω : Ω), discountedOccupation Z k ω ^ 2 ∂μ ≤ 2 * D * ∫ (ω : Ω), ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-2 * t) * |k (Z t.toNNReal ω)| ∂μ

Cheap bound: if |V| ≤ D then E B² ≤ 2 D E ∫_0^∞ e^{-2t}|k(Z_t)| dt.