feat(probability/martingale): optional sampling theorem (#14065)

We prove the optional sampling theorem: if `τ` is a bounded stopping time and `σ` is another stopping time, then the value of a martingale `f` at the stopping time `min τ σ` is almost everywhere equal to `μ[stopped_value f τ | hσ.measurable_space]`.



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

src/probability/martingale/basic.lean

@@ -352,7 +352,7 @@ begin
   refine ⟨hf.1.smul c, λ i j hij, _, λ i, (hf.2.2 i).smul c⟩,
   refine (condexp_smul c (f j)).le.trans _,
   filter_upwards [hf.2.1 i j hij] with _ hle,
-  simp,
+  simp_rw [pi.smul_apply],
   exact smul_le_smul_of_nonneg hle hc,
 end
 

src/probability/martingale/optional_sampling.lean

@@ -0,0 +1,236 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+
+import order.succ_pred.linear_locally_finite
+import probability.martingale.basic
+
+/-!
+# Optional sampling theorem
+
+If `τ` is a bounded stopping time and `σ` is another stopping time, then the value of a martingale
+`f` at the stopping time `min τ σ` is almost everywhere equal to
+`μ[stopped_value f τ | hσ.measurable_space]`.
+
+## Main results
+
+* `stopped_value_ae_eq_condexp_of_le_const`: the value of a martingale `f` at a stopping time `τ`
+  bounded by `n` is the conditional expectation of `f n` with respect to the σ-algebra generated by
+  `τ`.
+* `stopped_value_ae_eq_condexp_of_le`: if `τ` and `σ` are two stopping times with `σ ≤ τ` and `τ` is
+  bounded, then the value of a martingale `f` at `σ` is the conditional expectation of its value at
+  `τ` with respect to the σ-algebra generated by `σ`.
+* `stopped_value_min_ae_eq_condexp`: the optional sampling theorem. If `τ` is a bounded stopping
+  time and `σ` is another stopping time, then the value of a martingale `f` at the stopping time
+  `min τ σ` is almost everywhere equal to the conditional expectation of `f` stopped at `τ`
+  with respect to the σ-algebra generated by `σ`.
+
+-/
+
+open_locale measure_theory big_operators ennreal
+open topological_space
+
+-- TODO after the port: move to topology/instances/discrete
+@[priority 100]
+instance discrete_topology.second_countable_topology_of_countable {α : Type*} [topological_space α]
+  [discrete_topology α] [countable α] :
+  second_countable_topology α :=
+@discrete_topology.second_countable_topology_of_encodable _ _ _ (encodable.of_countable _)
+
+namespace measure_theory
+
+namespace martingale
+
+variables {Ω E : Type*} {m : measurable_space Ω} {μ : measure Ω}
+  [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
+
+section first_countable_topology
+
+variables {ι : Type*} [linear_order ι] [topological_space ι] [order_topology ι]
+  [first_countable_topology ι]
+  {ℱ : filtration ι m} [sigma_finite_filtration μ ℱ] {τ σ : Ω → ι} {f : ι → Ω → E}  {i n : ι}
+
+lemma condexp_stopping_time_ae_eq_restrict_eq_const
+  [(filter.at_top : filter ι).is_countably_generated]
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) [sigma_finite (μ.trim hτ.measurable_space_le)]
+  (hin : i ≤ n) :
+  μ[f n | hτ.measurable_space] =ᵐ[μ.restrict {x | τ x = i}] f i :=
+begin
+  refine filter.eventually_eq.trans _ (ae_restrict_of_ae (h.condexp_ae_eq hin)),
+  refine condexp_ae_eq_restrict_of_measurable_space_eq_on hτ.measurable_space_le (ℱ.le i)
+    (hτ.measurable_set_eq' i) (λ t, _),
+  rw [set.inter_comm _ t, is_stopping_time.measurable_set_inter_eq_iff],
+end
+
+lemma condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hτ_le : ∀ x, τ x ≤ n)
+  [sigma_finite (μ.trim (hτ.measurable_space_le_of_le hτ_le))] (i : ι) :
+  μ[f n | hτ.measurable_space] =ᵐ[μ.restrict {x | τ x = i}] f i :=
+begin
+  by_cases hin : i ≤ n,
+  { refine filter.eventually_eq.trans _ (ae_restrict_of_ae (h.condexp_ae_eq hin)),
+    refine condexp_ae_eq_restrict_of_measurable_space_eq_on (hτ.measurable_space_le_of_le hτ_le)
+      (ℱ.le i) (hτ.measurable_set_eq' i) (λ t, _),
+    rw [set.inter_comm _ t, is_stopping_time.measurable_set_inter_eq_iff], },
+  { suffices : {x : Ω | τ x = i} = ∅, by simp [this],
+    ext1 x,
+    simp only [set.mem_set_of_eq, set.mem_empty_iff_false, iff_false],
+    rintro rfl,
+    exact hin (hτ_le x), },
+end
+
+lemma stopped_value_ae_eq_restrict_eq
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hτ_le : ∀ x, τ x ≤ n)
+  [sigma_finite (μ.trim ((hτ.measurable_space_le_of_le hτ_le)))] (i : ι) :
+  stopped_value f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurable_space] :=
+begin
+  refine filter.eventually_eq.trans _
+    (condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm,
+  rw [filter.eventually_eq, ae_restrict_iff' (ℱ.le _ _ (hτ.measurable_set_eq i))],
+  refine filter.eventually_of_forall (λ x hx, _),
+  rw set.mem_set_of_eq at hx,
+  simp_rw [stopped_value, hx],
+end
+
+/-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
+expectation of `f n` with respect to the σ-algebra generated by `τ`. -/
+lemma stopped_value_ae_eq_condexp_of_le_const_of_countable_range
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ)
+  (hτ_le : ∀ x, τ x ≤ n) (h_countable_range : (set.range τ).countable)
+  [sigma_finite (μ.trim (hτ.measurable_space_le_of_le hτ_le))] :
+  stopped_value f τ =ᵐ[μ] μ[f n | hτ.measurable_space] :=
+begin
+  have : set.univ = ⋃ i ∈ (set.range τ), {x | τ x = i},
+  { ext1 x,
+    simp only [set.mem_univ, set.mem_range, true_and, set.Union_exists, set.Union_Union_eq',
+      set.mem_Union, set.mem_set_of_eq, exists_apply_eq_apply'], },
+  nth_rewrite 0 ← @measure.restrict_univ Ω _ μ,
+  rw [this, ae_eq_restrict_bUnion_iff _ h_countable_range],
+  exact λ i hi, stopped_value_ae_eq_restrict_eq h _ hτ_le i,
+end
+
+/-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
+expectation of `f n` with respect to the σ-algebra generated by `τ`. -/
+lemma stopped_value_ae_eq_condexp_of_le_const [countable ι]
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hτ_le : ∀ x, τ x ≤ n)
+  [sigma_finite (μ.trim (hτ.measurable_space_le_of_le hτ_le))] :
+  stopped_value f τ =ᵐ[μ] μ[f n | hτ.measurable_space] :=
+h.stopped_value_ae_eq_condexp_of_le_const_of_countable_range hτ hτ_le (set.to_countable _)
+
+/-- If `τ` and `σ` are two stopping times with `σ ≤ τ` and `τ` is bounded, then the value of a
+martingale `f` at `σ` is the conditional expectation of its value at `τ` with respect to the
+σ-algebra generated by `σ`. -/
+lemma stopped_value_ae_eq_condexp_of_le_of_countable_range
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hσ : is_stopping_time ℱ σ)
+  (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ x, τ x ≤ n)
+  (hτ_countable_range : (set.range τ).countable) (hσ_countable_range : (set.range σ).countable)
+  [sigma_finite (μ.trim (hσ.measurable_space_le_of_le (λ x, (hσ_le_τ x).trans (hτ_le x))))] :
+  stopped_value f σ =ᵐ[μ] μ[stopped_value f τ | hσ.measurable_space] :=
+begin
+  haveI : sigma_finite (μ.trim (hτ.measurable_space_le_of_le hτ_le)),
+  { exact sigma_finite_trim_mono _ (is_stopping_time.measurable_space_mono hσ hτ hσ_le_τ), },
+  have : μ[stopped_value f τ|hσ.measurable_space]
+      =ᵐ[μ] μ[μ[f n|hτ.measurable_space] | hσ.measurable_space],
+    from condexp_congr_ae (h.stopped_value_ae_eq_condexp_of_le_const_of_countable_range hτ hτ_le
+      hτ_countable_range),
+  refine (filter.eventually_eq.trans _
+    (condexp_condexp_of_le _ (hτ.measurable_space_le_of_le hτ_le)).symm).trans this.symm,
+  { exact h.stopped_value_ae_eq_condexp_of_le_const_of_countable_range hσ
+      (λ x, (hσ_le_τ x).trans (hτ_le x)) hσ_countable_range, },
+  { exact hσ.measurable_space_mono hτ hσ_le_τ, },
+end
+
+/-- If `τ` and `σ` are two stopping times with `σ ≤ τ` and `τ` is bounded, then the value of a
+martingale `f` at `σ` is the conditional expectation of its value at `τ` with respect to the
+σ-algebra generated by `σ`. -/
+lemma stopped_value_ae_eq_condexp_of_le [countable ι]
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hσ : is_stopping_time ℱ σ)
+  (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ x, τ x ≤ n) [sigma_finite (μ.trim hσ.measurable_space_le)] :
+  stopped_value f σ =ᵐ[μ] μ[stopped_value f τ | hσ.measurable_space] :=
+h.stopped_value_ae_eq_condexp_of_le_of_countable_range hτ hσ hσ_le_τ hτ_le
+  (set.to_countable _) (set.to_countable _)
+
+end first_countable_topology
+
+section subset_of_nat
+
+/-! In the following results the index set verifies `[linear_order ι] [locally_finite_order ι]` and
+`[order_bot ι]`, which means that it is order-isomorphic to a subset of `ℕ`. `ι` is equipped with
+the discrete topology, which is also the order topology, and is a measurable space with the Borel
+σ-algebra. -/
+
+variables {ι : Type*} [linear_order ι] [locally_finite_order ι] [order_bot ι]
+  [topological_space ι] [discrete_topology ι] [measurable_space ι] [borel_space ι]
+  [measurable_space E] [borel_space E] [second_countable_topology E]
+  {ℱ : filtration ι m} {τ σ : Ω → ι} {f : ι → Ω → E} {i n : ι}
+
+lemma condexp_stopped_value_stopping_time_ae_eq_restrict_le
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hσ : is_stopping_time ℱ σ)
+  [sigma_finite (μ.trim hσ.measurable_space_le)] (hτ_le : ∀ x, τ x ≤ n) :
+  μ[stopped_value f τ | hσ.measurable_space] =ᵐ[μ.restrict {x : Ω | τ x ≤ σ x}] stopped_value f τ :=
+begin
+  rw ae_eq_restrict_iff_indicator_ae_eq
+    (hτ.measurable_space_le _ (hτ.measurable_set_le_stopping_time hσ)),
+  swap, apply_instance,
+  refine (condexp_indicator (integrable_stopped_value ι hτ h.integrable hτ_le)
+    (hτ.measurable_set_stopping_time_le hσ)).symm.trans _,
+  have h_int : integrable ({ω : Ω | τ ω ≤ σ ω}.indicator (stopped_value (λ (n : ι), f n) τ)) μ,
+  { refine (integrable_stopped_value ι hτ h.integrable hτ_le).indicator _,
+    exact hτ.measurable_space_le _ (hτ.measurable_set_le_stopping_time hσ), },
+  have h_meas : ae_strongly_measurable' hσ.measurable_space
+    ({ω : Ω | τ ω ≤ σ ω}.indicator (stopped_value (λ (n : ι), f n) τ)) μ,
+  { refine strongly_measurable.ae_strongly_measurable' _,
+    refine strongly_measurable.strongly_measurable_of_measurable_space_le_on
+      (hτ.measurable_set_le_stopping_time hσ) _ _ _,
+    { intros t ht,
+      rw set.inter_comm _ t at ht ⊢,
+      rw [hτ.measurable_set_inter_le_iff, is_stopping_time.measurable_set_min_iff hτ hσ] at ht,
+      exact ht.2, },
+    { refine strongly_measurable.indicator _ (hτ.measurable_set_le_stopping_time hσ),
+      refine measurable.strongly_measurable _,
+      exact measurable_stopped_value h.adapted.prog_measurable_of_discrete hτ, },
+    { intros x hx,
+      simp only [hx, set.indicator_of_not_mem, not_false_iff], }, },
+  exact condexp_of_ae_strongly_measurable' hσ.measurable_space_le h_meas h_int,
+end
+
+/-- **Optional Sampling theorem**. If `τ` is a bounded stopping time and `σ` is another stopping
+time, then the value of a martingale `f` at the stopping time `min τ σ` is almost everywhere equal
+to the conditional expectation of `f` stopped at `τ` with respect to the σ-algebra generated
+by `σ`. -/
+lemma stopped_value_min_ae_eq_condexp [sigma_finite_filtration μ ℱ]
+  (h : martingale f ℱ μ) (hτ : is_stopping_time ℱ τ) (hσ : is_stopping_time ℱ σ) {n : ι}
+  (hτ_le : ∀ x, τ x ≤ n) [h_sf_min : sigma_finite (μ.trim (hτ.min hσ).measurable_space_le)] :
+  stopped_value f (λ x, min (σ x) (τ x)) =ᵐ[μ] μ[stopped_value f τ | hσ.measurable_space] :=
+begin
+  refine (h.stopped_value_ae_eq_condexp_of_le hτ (hσ.min hτ) (λ x, min_le_right _ _) hτ_le).trans _,
+  refine ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} _ _,
+  { exact condexp_min_stopping_time_ae_eq_restrict_le hσ hτ, },
+  { suffices : μ[stopped_value f τ|(hσ.min hτ).measurable_space]
+      =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stopped_value f τ|hσ.measurable_space],
+    { rw ae_restrict_iff' (hσ.measurable_space_le _ (hσ.measurable_set_le_stopping_time hτ).compl),
+      rw [filter.eventually_eq, ae_restrict_iff'] at this,
+      swap, { exact hτ.measurable_space_le _ (hτ.measurable_set_le_stopping_time hσ), },
+      filter_upwards [this] with x hx hx_mem,
+      simp only [set.mem_compl_iff, set.mem_set_of_eq, not_le] at hx_mem,
+      exact hx hx_mem.le, },
+    refine filter.eventually_eq.trans _
+      ((condexp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _),
+    { exact stopped_value f τ, },
+    { rw [is_stopping_time.measurable_space_min, is_stopping_time.measurable_space_min, inf_comm] },
+    { have h1 : μ[stopped_value f τ|hτ.measurable_space] = stopped_value f τ,
+      { refine condexp_of_strongly_measurable hτ.measurable_space_le _ _,
+        { refine measurable.strongly_measurable _,
+          exact measurable_stopped_value h.adapted.prog_measurable_of_discrete hτ, },
+        { exact integrable_stopped_value ι hτ h.integrable hτ_le, }, },
+      rw h1,
+      exact (condexp_stopped_value_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm, }, },
+end
+
+end subset_of_nat
+
+end martingale
+
+end measure_theory

src/probability/process/stopping.lean

@@ -1216,4 +1216,74 @@ by { ext ω, rw stopped_value, by_cases hx : ω ∈ s; simp [hx] }
 
 end piecewise_const
 
+section condexp
+/-! ### Conditional expectation with respect to the σ-algebra generated by a stopping time -/
+
+variables [linear_order ι] {μ : measure Ω} {ℱ : filtration ι m} {τ σ : Ω → ι}
+  {E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : Ω → E}
+
+lemma condexp_stopping_time_ae_eq_restrict_eq_of_countable_range [sigma_finite_filtration μ ℱ]
+  (hτ : is_stopping_time ℱ τ) (h_countable : (set.range τ).countable)
+  [sigma_finite (μ.trim (hτ.measurable_space_le_of_countable_range h_countable))] (i : ι) :
+  μ[f | hτ.measurable_space] =ᵐ[μ.restrict {x | τ x = i}] μ[f | ℱ i] :=
+begin
+  refine condexp_ae_eq_restrict_of_measurable_space_eq_on
+    (hτ.measurable_space_le_of_countable_range h_countable) (ℱ.le i)
+    (hτ.measurable_set_eq_of_countable_range' h_countable i) (λ t, _),
+  rw [set.inter_comm _ t, is_stopping_time.measurable_set_inter_eq_iff],
+end
+
+lemma condexp_stopping_time_ae_eq_restrict_eq_of_countable [countable ι]
+  [sigma_finite_filtration μ ℱ]
+  (hτ : is_stopping_time ℱ τ) [sigma_finite (μ.trim hτ.measurable_space_le_of_countable)] (i : ι) :
+  μ[f | hτ.measurable_space] =ᵐ[μ.restrict {x | τ x = i}] μ[f | ℱ i] :=
+condexp_stopping_time_ae_eq_restrict_eq_of_countable_range hτ (set.to_countable _) i
+
+variables [(filter.at_top : filter ι).is_countably_generated]
+
+lemma condexp_min_stopping_time_ae_eq_restrict_le_const (hτ : is_stopping_time ℱ τ)
+  (i : ι) [sigma_finite (μ.trim (hτ.min_const i).measurable_space_le)] :
+  μ[f | (hτ.min_const i).measurable_space]
+    =ᵐ[μ.restrict {x | τ x ≤ i}] μ[f | hτ.measurable_space] :=
+begin
+  haveI : sigma_finite (μ.trim hτ.measurable_space_le),
+  { have h_le : (hτ.min_const i).measurable_space ≤ hτ.measurable_space,
+    { rw is_stopping_time.measurable_space_min_const,
+      exact inf_le_left, },
+    exact sigma_finite_trim_mono _ h_le, },
+  refine (condexp_ae_eq_restrict_of_measurable_space_eq_on hτ.measurable_space_le
+    (hτ.min_const i).measurable_space_le (hτ.measurable_set_le' i) (λ t, _)).symm,
+  rw [set.inter_comm _ t, hτ.measurable_set_inter_le_const_iff],
+end
+
+variables [topological_space ι] [order_topology ι]
+
+lemma condexp_stopping_time_ae_eq_restrict_eq
+  [first_countable_topology ι] [sigma_finite_filtration μ ℱ]
+  (hτ : is_stopping_time ℱ τ) [sigma_finite (μ.trim hτ.measurable_space_le)] (i : ι) :
+  μ[f | hτ.measurable_space] =ᵐ[μ.restrict {x | τ x = i}] μ[f | ℱ i] :=
+begin
+  refine condexp_ae_eq_restrict_of_measurable_space_eq_on
+    hτ.measurable_space_le (ℱ.le i) (hτ.measurable_set_eq' i) (λ t, _),
+  rw [set.inter_comm _ t, is_stopping_time.measurable_set_inter_eq_iff],
+end
+
+lemma condexp_min_stopping_time_ae_eq_restrict_le [measurable_space ι]
+  [second_countable_topology ι] [borel_space ι]
+  (hτ : is_stopping_time ℱ τ) (hσ : is_stopping_time ℱ σ)
+  [sigma_finite (μ.trim (hτ.min hσ).measurable_space_le)] :
+  μ[f | (hτ.min hσ).measurable_space] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f | hτ.measurable_space] :=
+begin
+  haveI : sigma_finite (μ.trim hτ.measurable_space_le),
+  { have h_le : (hτ.min hσ).measurable_space ≤ hτ.measurable_space,
+    { rw is_stopping_time.measurable_space_min,
+      exact inf_le_left, },
+    exact sigma_finite_trim_mono _ h_le, },
+  refine (condexp_ae_eq_restrict_of_measurable_space_eq_on hτ.measurable_space_le
+    (hτ.min hσ).measurable_space_le (hτ.measurable_set_le_stopping_time hσ) (λ t, _)).symm,
+  rw [set.inter_comm _ t, is_stopping_time.measurable_set_inter_le_iff],
+end
+
+end condexp
+
 end measure_theory