feat(probability/martingale): the optional stopping theorem (#13630)

We prove the optional stopping theorem (also known as the fair game theorem). This is number 62 on Freek 100 theorems.

 

Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

docs/100.yaml

@@ -211,6 +211,8 @@
   title  : Theorem of Ceva
 62:
   title  : Fair Games Theorem
+  decl   : measure_theory.submartingale_iff_expected_stopped_value_mono
+  author : Kexing Ying
 63:
   title  : Cantor’s Theorem
   decl   : cardinal.cantor

src/algebra/indicator_function.lean

@@ -249,6 +249,19 @@ begin
   rw [pi.mul_apply, this, one_mul]
 end
 
+@[to_additive] lemma mul_indicator_mul_compl_eq_piecewise
+  [decidable_pred (∈ s)] (f g : α → M) :
+  s.mul_indicator f * sᶜ.mul_indicator g = s.piecewise f g :=
+begin
+  ext x,
+  by_cases h : x ∈ s,
+  { rw [piecewise_eq_of_mem _ _ _ h, pi.mul_apply, set.mul_indicator_of_mem h,
+      set.mul_indicator_of_not_mem (set.not_mem_compl_iff.2 h), mul_one] },
+  { rw [piecewise_eq_of_not_mem _ _ _ h, pi.mul_apply, set.mul_indicator_of_not_mem h,
+      set.mul_indicator_of_mem (set.mem_compl h), one_mul] },
+end
+
+
 /-- `set.mul_indicator` as a `monoid_hom`. -/
 @[to_additive "`set.indicator` as an `add_monoid_hom`."]
 def mul_indicator_hom {α} (M) [mul_one_class M] (s : set α) : (α → M) →* (α → M) :=

src/measure_theory/integral/bochner.lean

@@ -1456,14 +1456,30 @@ lemma ae_eq_trim_of_strongly_measurable
   f =ᵐ[μ.trim hm] g :=
 begin
   rwa [eventually_eq, ae_iff, trim_measurable_set_eq hm _],
-  exact measurable_set.compl (hf.measurable_set_eq_fun hg)
+  exact (hf.measurable_set_eq_fun hg).compl
 end
 
 lemma ae_eq_trim_iff [topological_space γ] [metrizable_space γ]
   (hm : m ≤ m0) {f g : β → γ} (hf : strongly_measurable[m] f) (hg : strongly_measurable[m] g) :
   f =ᵐ[μ.trim hm] g ↔ f =ᵐ[μ] g :=
 ⟨ae_eq_of_ae_eq_trim, ae_eq_trim_of_strongly_measurable hm hf hg⟩
 
+lemma ae_le_trim_of_strongly_measurable
+  [linear_order γ] [topological_space γ] [order_closed_topology γ] [metrizable_space γ]
+  (hm : m ≤ m0) {f g : β → γ} (hf : strongly_measurable[m] f) (hg : strongly_measurable[m] g)
+  (hfg : f ≤ᵐ[μ] g) :
+  f ≤ᵐ[μ.trim hm] g :=
+begin
+  rwa [eventually_le, ae_iff, trim_measurable_set_eq hm _],
+  exact (hf.measurable_set_le hg).compl,
+end
+
+lemma ae_le_trim_iff
+  [linear_order γ] [topological_space γ] [order_closed_topology γ] [metrizable_space γ]
+  (hm : m ≤ m0) {f g : β → γ} (hf : strongly_measurable[m] f) (hg : strongly_measurable[m] g) :
+  f ≤ᵐ[μ.trim hm] g ↔ f ≤ᵐ[μ] g :=
+⟨ae_le_of_ae_le_trim, ae_le_trim_of_strongly_measurable hm hf hg⟩
+
 end integral_trim
 
 end measure_theory

src/measure_theory/integral/set_integral.lean

@@ -141,6 +141,13 @@ begin
   ... = ∫ x in s, f x ∂μ : by simp
 end
 
+lemma integral_piecewise [decidable_pred (∈ s)] (hs : measurable_set s)
+  {f g : α → E} (hf : integrable_on f s μ) (hg : integrable_on g sᶜ μ) :
+  ∫ x, s.piecewise f g x ∂μ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, g x ∂μ :=
+by rw [← set.indicator_add_compl_eq_piecewise,
+  integral_add' (hf.indicator hs) (hg.indicator hs.compl),
+  integral_indicator hs, integral_indicator hs.compl]
+
 lemma tendsto_set_integral_of_monotone {ι : Type*} [encodable ι] [semilattice_sup ι]
   {s : ι → set α} {f : α → E} (hsm : ∀ i, measurable_set (s i))
   (h_mono : monotone s) (hfi : integrable_on f (⋃ n, s n) μ) :

src/measure_theory/measure/measure_space.lean

@@ -3095,11 +3095,20 @@ lemma measure_trim_to_measurable_eq_zero {hm : m ≤ m0} (hs : μ.trim hm s = 0)
   μ (@to_measurable α m (μ.trim hm) s) = 0 :=
 measure_eq_zero_of_trim_eq_zero hm (by rwa measure_to_measurable)
 
+lemma ae_of_ae_trim (hm : m ≤ m0) {μ : measure α} {P : α → Prop} (h : ∀ᵐ x ∂(μ.trim hm), P x) :
+  ∀ᵐ x ∂μ, P x :=
+measure_eq_zero_of_trim_eq_zero hm h
+
 lemma ae_eq_of_ae_eq_trim {E} {hm : m ≤ m0} {f₁ f₂ : α → E}
   (h12 : f₁ =ᶠ[@measure.ae α m (μ.trim hm)] f₂) :
   f₁ =ᵐ[μ] f₂ :=
 measure_eq_zero_of_trim_eq_zero hm h12
 
+lemma ae_le_of_ae_le_trim {E} [has_le E] {hm : m ≤ m0} {f₁ f₂ : α → E}
+  (h12 : f₁ ≤ᶠ[@measure.ae α m (μ.trim hm)] f₂) :
+  f₁ ≤ᵐ[μ] f₂ :=
+measure_eq_zero_of_trim_eq_zero hm h12
+
 lemma trim_trim {m₁ m₂ : measurable_space α} {hm₁₂ : m₁ ≤ m₂} {hm₂ : m₂ ≤ m0} :
   (μ.trim hm₂).trim hm₁₂ = μ.trim (hm₁₂.trans hm₂) :=
 begin

src/probability/martingale.lean

@@ -225,6 +225,7 @@ begin
   simpa,
 end
 
+/-- The converse of this lemma is `measure_theory.submartingale_of_set_integral_le`. -/
 lemma set_integral_le {f : ι → α → ℝ} (hf : submartingale f ℱ μ)
   {i j : ι} (hij : i ≤ j) {s : set α} (hs : measurable_set[ℱ i] s) :
   ∫ x in s, f i x ∂μ ≤ ∫ x in s, f j x ∂μ :=
@@ -243,6 +244,31 @@ hf.sub_supermartingale hg.supermartingale
 
 end submartingale
 
+section
+
+lemma submartingale_of_set_integral_le [is_finite_measure μ]
+  {f : ι → α → ℝ} (hadp : adapted ℱ f) (hint : ∀ i, integrable (f i) μ)
+  (hf : ∀ i j : ι, i ≤ j → ∀ s : set α, measurable_set[ℱ i] s →
+    ∫ x in s, f i x ∂μ ≤ ∫ x in s, f j x ∂μ) :
+  submartingale f ℱ μ :=
+begin
+  refine ⟨hadp, λ i j hij, _, hint⟩,
+  suffices : f i ≤ᵐ[μ.trim (ℱ.le i)] μ[f j| ℱ.le i],
+  { exact ae_le_of_ae_le_trim this },
+  suffices : 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j| ℱ.le i] - f i,
+  { filter_upwards [this] with x hx,
+    rwa ← sub_nonneg },
+  refine ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure
+    ((integrable_condexp.sub (hint i)).trim _ (strongly_measurable_condexp.sub $ hadp i))
+    (λ s hs, _),
+  specialize hf i j hij s hs,
+  rwa [← set_integral_trim _ (strongly_measurable_condexp.sub $ hadp i) hs,
+    integral_sub' integrable_condexp.integrable_on (hint i).integrable_on, sub_nonneg,
+    set_integral_condexp _ (hint j) hs],
+end
+
+end
+
 namespace supermartingale
 
 lemma sub_submartingale [preorder E] [covariant_class E E (+) (≤)]
@@ -353,6 +379,37 @@ end
 
 end submartingale
 
+/-- The converse direction of the optional stopping theorem, i.e. an adapted integrable process `f`
+is a submartingale if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the
+stopped value of `f` at `τ` has expectation smaller than its stopped value at `π`. -/
+lemma submartingale_of_expected_stopped_value_mono [is_finite_measure μ]
+  {f : ℕ → α → ℝ} (hadp : adapted 𝒢 f) (hint : ∀ i, integrable (f i) μ)
+  (hf : ∀ τ π : α → ℕ, is_stopping_time 𝒢 τ → is_stopping_time 𝒢 π → τ ≤ π → (∃ N, ∀ x, π x ≤ N) →
+    μ[stopped_value f τ] ≤ μ[stopped_value f π]) :
+  submartingale f 𝒢 μ :=
+begin
+  refine submartingale_of_set_integral_le hadp hint (λ i j hij s hs, _),
+  classical,
+  specialize hf (s.piecewise (λ _, i) (λ _, j)) _
+    (is_stopping_time_piecewise_const hij hs)
+    (is_stopping_time_const j) (λ x, (ite_le_sup _ _ _).trans (max_eq_right hij).le)
+    ⟨j, λ x, le_rfl⟩,
+  rwa [stopped_value_const, stopped_value_piecewise_const,
+    integral_piecewise (𝒢.le _ _ hs) (hint _).integrable_on (hint _).integrable_on,
+    ← integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf,
+end
+
+/-- **The optional stopping theorem** (fair game theorem): an adapted integrable process `f`
+is a submartingale if and only if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the
+stopped value of `f` at `τ` has expectation smaller than its stopped value at `π`. -/
+lemma submartingale_iff_expected_stopped_value_mono [is_finite_measure μ]
+  {f : ℕ → α → ℝ} (hadp : adapted 𝒢 f) (hint : ∀ i, integrable (f i) μ) :
+  submartingale f 𝒢 μ ↔
+  ∀ τ π : α → ℕ, is_stopping_time 𝒢 τ → is_stopping_time 𝒢 π → τ ≤ π → (∃ N, ∀ x, π x ≤ N) →
+    μ[stopped_value f τ] ≤ μ[stopped_value f π] :=
+⟨λ hf _ _ hτ hπ hle ⟨N, hN⟩, hf.expected_stopped_value_mono hτ hπ hle hN,
+ submartingale_of_expected_stopped_value_mono hadp hint⟩
+
 end nat
 
 end measure_theory

src/probability/stopping.lean

@@ -550,6 +550,38 @@ begin
   exact f.mono (sub_le_self j hi) _ (hτ (j - i)),
 end
 
+lemma add_const_nat
+  {f : filtration ℕ m} {τ : α → ℕ} (hτ : is_stopping_time f τ) {i : ℕ} :
+  is_stopping_time f (λ x, τ x + i) :=
+begin
+  refine is_stopping_time_of_measurable_set_eq (λ j, _),
+  by_cases hij : i ≤ j,
+  { simp_rw [eq_comm, ← nat.sub_eq_iff_eq_add hij, eq_comm],
+    exact f.mono (j.sub_le i) _ (hτ.measurable_set_eq (j - i)) },
+  { rw not_le at hij,
+    convert measurable_set.empty,
+    ext x,
+    simp only [set.mem_empty_eq, iff_false],
+    rintro (hx : τ x + i = j),
+    linarith },
+end
+
+-- generalize to certain encodable type?
+lemma add
+  {f : filtration ℕ m} {τ π : α → ℕ} (hτ : is_stopping_time f τ) (hπ : is_stopping_time f π) :
+  is_stopping_time f (τ + π) :=
+begin
+  intro i,
+  rw (_ : {x | (τ + π) x ≤ i} = ⋃ k ≤ i, {x | π x = k} ∩ {x | τ x + k ≤ i}),
+  { exact measurable_set.Union (λ k, measurable_set.Union_Prop
+      (λ hk, (hπ.measurable_set_eq_le hk).inter (hτ.add_const_nat i))) },
+  ext,
+  simp only [pi.add_apply, set.mem_set_of_eq, set.mem_Union, set.mem_inter_eq, exists_prop],
+  refine ⟨λ h, ⟨π x, by linarith, rfl, h⟩, _⟩,
+  rintro ⟨j, hj, rfl, h⟩,
+  assumption
+end
+
 section preorder
 
 variables [preorder ι] {f : filtration ι m}
@@ -667,6 +699,9 @@ time `τ` is the map `x ↦ u (τ x) x`. -/
 def stopped_value (u : ι → α → β) (τ : α → ι) : α → β :=
 λ x, u (τ x) x
 
+lemma stopped_value_const (u : ι → α → β) (i : ι) : stopped_value u (λ x, i) = u i :=
+rfl
+
 variable [linear_order ι]
 
 /-- Given a map `u : ι → α → E`, the stopped process with respect to `τ` is `u i x` if
@@ -897,4 +932,45 @@ end normed_group
 
 end nat
 
+section piecewise_const
+
+variables [preorder ι] {𝒢 : filtration ι m} {τ η : α → ι} {i j : ι} {s : set α}
+  [decidable_pred (∈ s)]
+
+/-- Given stopping times `τ` and `η` which are bounded below, `set.piecewise s τ η` is also
+a stopping time with respect to the same filtration. -/
+lemma is_stopping_time.piecewise_of_le (hτ_st : is_stopping_time 𝒢 τ)
+  (hη_st : is_stopping_time 𝒢 η) (hτ : ∀ x, i ≤ τ x) (hη : ∀ x, i ≤ η x)
+  (hs : measurable_set[𝒢 i] s) :
+  is_stopping_time 𝒢 (s.piecewise τ η) :=
+begin
+  intro n,
+  have : {x | s.piecewise τ η x ≤ n}
+    = (s ∩ {x | τ x ≤ n}) ∪ (sᶜ ∩ {x | η x ≤ n}),
+  { ext1 x,
+    simp only [set.piecewise, set.mem_inter_eq, set.mem_set_of_eq, and.congr_right_iff],
+    by_cases hx : x ∈ s; simp [hx], },
+  rw this,
+  by_cases hin : i ≤ n,
+  { have hs_n : measurable_set[𝒢 n] s, from 𝒢.mono hin _ hs,
+    exact (hs_n.inter (hτ_st n)).union (hs_n.compl.inter (hη_st n)), },
+  { have hτn : ∀ x, ¬ τ x ≤ n := λ x hτn, hin ((hτ x).trans hτn),
+    have hηn : ∀ x, ¬ η x ≤ n := λ x hηn, hin ((hη x).trans hηn),
+    simp [hτn, hηn], },
+end
+
+lemma is_stopping_time_piecewise_const (hij : i ≤ j) (hs : measurable_set[𝒢 i] s) :
+  is_stopping_time 𝒢 (s.piecewise (λ _, i) (λ _, j)) :=
+(is_stopping_time_const i).piecewise_of_le (is_stopping_time_const j) (λ x, le_rfl) (λ _, hij) hs
+
+lemma stopped_value_piecewise_const {ι' : Type*} {i j : ι'} {f : ι' → α → ℝ} :
+  stopped_value f (s.piecewise (λ _, i) (λ _, j)) = s.piecewise (f i) (f j) :=
+by { ext x, rw stopped_value, by_cases hx : x ∈ s; simp [hx] }
+
+lemma stopped_value_piecewise_const' {ι' : Type*} {i j : ι'} {f : ι' → α → ℝ} :
+  stopped_value f (s.piecewise (λ _, i) (λ _, j)) = s.indicator (f i) + sᶜ.indicator (f j) :=
+by { ext x, rw stopped_value, by_cases hx : x ∈ s; simp [hx] }
+
+end piecewise_const
+
 end measure_theory