Prove that several processes are adapted/predictable

LeanBandits/ForMathlib/SubGaussian.lean

@@ -10,6 +10,49 @@ open scoped ENNReal NNReal
 
 namespace ProbabilityTheory
 
+namespace HasCondSubgaussianMGF
+
+variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω]
+  {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℝ} {c : ℝ≥0}
+
+lemma ae_trim_condExp_exp_sub_le_one (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
+    ∀ᵐ ω' ∂(μ.trim hm), (μ[fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)|m]) ω' ≤ 1 := by
+  have h_le : ∀ᵐ ω' ∂(μ.trim hm), μ[fun ω ↦ exp (t * X ω)|m] ω' ≤ exp (c * t ^ 2 / 2) :=
+    h.ae_trim_condExp_le t
+  have h_eq : μ[fun ω ↦ exp (t * X ω) / exp (c * t ^ 2 / 2)|m] =ᵐ[μ.trim hm]
+      fun ω ↦ μ[fun ω ↦ exp (t * X ω)|m] ω / exp (c * t ^ 2 / 2) := by
+    refine ae_eq_trim_of_measurable _ ?_ ?_ ?_
+    · exact stronglyMeasurable_condExp.measurable
+    · refine Measurable.div_const ?_ _
+      exact stronglyMeasurable_condExp.measurable
+    simp_rw [div_eq_inv_mul]
+    refine condExp_mul_of_stronglyMeasurable_left ?_ ?_ ?_
+    · fun_prop
+    · refine Integrable.const_mul ?_ _
+      exact h.integrable_exp_mul _
+    · exact h.integrable_exp_mul _
+  filter_upwards [h_le, h_eq] with ω hω_le hω_eq
+  simp_rw [exp_sub, hω_eq]
+  rwa [div_le_one (by positivity)]
+
+lemma ae_condExp_exp_sub_le_one (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
+    ∀ᵐ ω' ∂μ, (μ[fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)|m]) ω' ≤ 1 :=
+  ae_of_ae_trim hm (h.ae_trim_condExp_exp_sub_le_one t)
+
+lemma memLp_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) (p : ℝ≥0) :
+    MemLp (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) p μ := by
+  have h_lp := h.memLp_exp_mul t p
+  simp_rw [sub_eq_add_neg, exp_add]
+  exact h_lp.mul_const _
+
+lemma integrable_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
+    Integrable (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) μ := by
+  have h_int := h.integrable_exp_mul t
+  simp_rw [exp_sub]
+  exact h_int.div_const _
+
+end HasCondSubgaussianMGF
+
 namespace HasSubgaussianMGF
 
 variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X Y : Ω → ℝ} {c cX cY : ℝ≥0}

LeanBandits/SequentialLearning/Algorithm.lean

@@ -183,6 +183,36 @@ def IsAlgEnvSeq.filtration (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurab
     rw [← measurable_iff_comap_le]
     exact measurable_hist hA hR' i
 
+lemma IsAlgEnvSeq.measurable_hist_filtration
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
+    Measurable[IsAlgEnvSeq.filtration hA hR' n] (IsAlgEnvSeq.hist A R' n) :=
+  measurable_iff_comap_le.mpr le_rfl
+
+lemma IsAlgEnvSeq.adapted_hist [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α]
+    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
+    Adapted (filtration hA hR') (IsAlgEnvSeq.hist A R') :=
+  fun n ↦ (IsAlgEnvSeq.measurable_hist_filtration hA hR' n).stronglyMeasurable
+
+lemma IsAlgEnvSeq.measurable_step_filtration
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
+    Measurable[IsAlgEnvSeq.filtration hA hR' n] (IsAlgEnvSeq.step A R' n) := by
+  have : step A R' n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (hist A R' n) := by
+    ext ω : 1
+    simp [hist, step]
+  rw [this]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma IsAlgEnvSeq.adapted_step [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α]
+    [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
+    Adapted (filtration hA hR') (step A R') :=
+  fun n ↦ (IsAlgEnvSeq.measurable_step_filtration hA hR' n).stronglyMeasurable
+
 lemma IsAlgEnvSeq.measurable_action_filtration
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
     Measurable[IsAlgEnvSeq.filtration hA hR' n] (A n) := by
@@ -192,6 +222,27 @@ lemma IsAlgEnvSeq.measurable_action_filtration
   rw [this]
   exact measurable_comp_comap _ (by fun_prop)
 
+lemma IsAlgEnvSeq.adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
+    Adapted (filtration hA hR') A :=
+  fun n ↦ (IsAlgEnvSeq.measurable_action_filtration hA hR' n).stronglyMeasurable
+
+lemma IsAlgEnvSeq.measurable_reward_filtration
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) :
+    Measurable[IsAlgEnvSeq.filtration hA hR' n] (R' n) := by
+  have : R' n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (hist A R' n) := by
+    ext ω : 1
+    simp [IsAlgEnvSeq.hist]
+  rw [this]
+  exact measurable_comp_comap _ (by fun_prop)
+
+lemma IsAlgEnvSeq.adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R]
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :
+    Adapted (filtration hA hR') R' :=
+  fun n ↦ (IsAlgEnvSeq.measurable_reward_filtration hA hR' n).stronglyMeasurable
+
 /-- Filtration generated by the history at time `n-1` together with the action at time `n`. -/
 def IsAlgEnvSeq.filtrationAction
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) :

LeanBandits/SequentialLearning/FiniteActions.lean

@@ -767,6 +767,14 @@ noncomputable
 def empMean' (n : ℕ) (h : Iic n → α × ℝ) (a : α) :=
   (sumRewards' n h a) / (pullCount' n h a)
 
+@[simp]
+lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0 := by ext; simp [sumRewards]
+
+lemma sumRewards_add_one {R' : ℕ → Ω → ℝ} :
+    sumRewards A R' a (t + 1) ω = sumRewards A R' a t ω + if A t ω = a then R' t ω else 0 := by
+  unfold sumRewards
+  rw [sum_range_succ]
+
 lemma sumRewards_eq_pullCount_mul_empMean {R' : ℕ → Ω → ℝ} {ω : Ω}
     (h_pull : pullCount A a t ω ≠ 0) :
     sumRewards A R' a t ω = pullCount A a t ω * empMean A R' a t ω := by unfold empMean; field_simp
@@ -811,6 +819,25 @@ lemma empMean_eq_empMean' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hn : n
   unfold empMean empMean'
   rw [sumRewards_eq_sumRewards' hn, pullCount_eq_pullCount' hn]
 
+lemma sumRewards_sub_pullCount_mul_eq_sum {R' : ℕ → Ω → ℝ} (c : α → ℝ) :
+    sumRewards A R' a (n + 1) ω - pullCount A a (n + 1) ω * c a =
+      ∑ i ∈ range (n + 1), (if A i ω = a then R' i ω - c a else 0) := by
+  induction n with
+  | zero =>
+    simp_rw [sumRewards_add_one, pullCount_add_one]
+    simp only [sumRewards_zero, Pi.zero_apply, zero_add, pullCount_zero, Nat.cast_ite, Nat.cast_one,
+      CharP.cast_eq_zero, ite_mul, one_mul, zero_mul, range_one, sum_singleton]
+    grind
+  | succ n hn =>
+    simp_rw [sumRewards_add_one (t := n + 1), pullCount_add_one (t := n + 1)]
+    split_ifs with ha
+    · conv_rhs => rw [sum_range_succ]
+      simp only [Nat.cast_add, Nat.cast_one, ha, ↓reduceIte, add_mul, one_mul]
+      grind
+    · simp only [add_zero, hn]
+      conv_rhs => rw [sum_range_succ]
+      simp [ha]
+
 @[fun_prop]
 lemma measurable_sumRewards [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ}
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (t : ℕ) :
@@ -843,6 +870,76 @@ lemma measurable_empMean' [MeasurableSingletonClass α] (n : ℕ) (a : α) :
   unfold empMean'
   fun_prop
 
+lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm α ℝ} {env : Environment α ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : α) :
+    IsPredictable (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) (sumRewards A R' a) := by
+  rw [isPredictable_iff_measurable_add_one]
+  constructor
+  · simp only [sumRewards_zero]
+    fun_prop
+  refine fun n ↦ measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop)
+  · refine (measurableSet_singleton a).preimage ?_
+    have h_meas_i := IsAlgEnvSeq.measurable_action_filtration h.measurable_A h.measurable_R i
+    simp only [mem_range] at hi
+    exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_A h.measurable_R).mono (by lia))
+      le_rfl
+  · have h_meas_i := IsAlgEnvSeq.measurable_reward_filtration h.measurable_A h.measurable_R i
+    simp only [mem_range] at hi
+    exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_A h.measurable_R).mono (by lia))
+      le_rfl
+
+lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm α ℝ} {env : Environment α ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : α) :
+    Adapted (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R)
+      (fun n ↦ sumRewards A R' a (n + 1)) := by
+  have h_predictable := h.isPredictable_sumRewards a
+  rw [isPredictable_iff_measurable_add_one] at h_predictable
+  exact fun n ↦ Measurable.stronglyMeasurable (h_predictable.2 n)
+
+section CopiedFromPR
+
+open Set
+
+theorem _root_.MeasureTheory.StronglyMeasurable.div₀' {α β : Type*}
+    {mα : MeasurableSpace α} [TopologicalSpace β]
+    [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β]
+    [TopologicalSpace.PseudoMetrizableSpace β]
+    [MeasurableSpace β] [BorelSpace β] [MeasurableSingletonClass β]
+    {f g : α → β} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
+    StronglyMeasurable (f / g) := by
+  refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
+  have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
+  by_cases h : g x = 0
+  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_setOf_eq,
+      not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]
+    exact tendsto_const_nhds
+  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
+      Pi.div_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]
+    exact (hf.tendsto_approx x).div (hg.tendsto_approx x) h
+
+end CopiedFromPR
+
+lemma IsAlgEnvSeq.isPredictable_empMean [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm α ℝ} {env : Environment α ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : α) :
+    IsPredictable (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) (empMean A R' a) := by
+  unfold empMean
+  refine StronglyMeasurable.div₀' ?_ ?_
+  · exact h.isPredictable_sumRewards a
+  · have h_meas := (isPredictable_pullCount h.measurable_A h.measurable_R a).measurable
+    fun_prop
+
+lemma IsAlgEnvSeq.adapted_empMean_add_one [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ}
+    {alg : Algorithm α ℝ} {env : Environment α ℝ}
+    (h : IsAlgEnvSeq A R' alg env P) (a : α) :
+    Adapted (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R)
+      (fun n ↦ empMean A R' a (n + 1)) := by
+  have h_predictable := h.isPredictable_empMean a
+  rw [isPredictable_iff_measurable_add_one] at h_predictable
+  exact fun n ↦ Measurable.stronglyMeasurable (h_predictable.2 n)
+
 end SumRewards
 
 end Learning

blueprint/lean_decls

@@ -9,6 +9,10 @@ Learning.IsAlgEnvSeq.hasLaw_step_zero
 Learning.IsAlgEnvSeq.hasCondDistrib_step
 Learning.IsAlgEnvSeq.filtration
 Learning.IsAlgEnvSeq.filtrationAction
+Learning.IsAlgEnvSeq.adapted_step
+Learning.IsAlgEnvSeq.adapted_hist
+Learning.IsAlgEnvSeq.adapted_action
+Learning.IsAlgEnvSeq.adapted_reward
 Learning.isAlgEnvSeq_unique
 Learning.IsAlgEnvSeq.condDistrib_reward_stationaryEnv
 Learning.IsAlgEnvSeq.condIndepFun_reward_hist_action
@@ -50,6 +54,8 @@ Learning.rewardByCount
 Learning.rewardByCount_pullCount_add_one_eq_reward
 Learning.sumRewards
 Learning.empMean
+Learning.IsAlgEnvSeq.isPredictable_sumRewards
+Learning.IsAlgEnvSeq.isPredictable_empMean
 Learning.sum_rewardByCount_eq_sumRewards
 Bandits.ArrayModel.probSpace
 Bandits.ArrayModel.arrayMeasure

blueprint/src/chapters/algorithm.tex

@@ -130,6 +130,19 @@ \chapter{Iterative stochastic algorithms}
 \end{definition}
 
 
+\begin{lemma}\label{lem:IsAlgEnvSeq.adapted}
+  \uses{def:IsAlgEnvSeq.filtration,def:history}
+  \leanok
+  \lean{Learning.IsAlgEnvSeq.adapted_step, Learning.IsAlgEnvSeq.adapted_hist, Learning.IsAlgEnvSeq.adapted_action, Learning.IsAlgEnvSeq.adapted_reward}
+The history, step, action and observation processes are adapted to the filtration $(\mathcal{F}_t)_{t \in \mathbb{N}}$.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{def:history,def:IsAlgEnvSeq.filtration}
+By definition of the filtration.
+\end{proof}
+
+
 \begin{theorem}[\cite{lattimore2020bandit}, Proposition 4.8]\label{thm:isAlgEnvSeq_unique}
   \uses{def:environment,def:IsAlgEnvSeq,def:algorithm}
   \leanok
@@ -556,6 +569,19 @@ \section{Scalar rewards}
 Note: in bandit papers it is common to (implicitly) define the empirical mean as $+\infty$ when the action was never chosen, but in Lean it has to be a real number, and the Lean default value for division by zero is $0$.
 
 
+\begin{lemma}\label{lem:isPredictable_sumRewards}
+  \uses{def:IsAlgEnvSeq.filtration, def:sumRewards, def:empMean}
+  \leanok
+  \lean{Learning.IsAlgEnvSeq.isPredictable_sumRewards, Learning.IsAlgEnvSeq.isPredictable_empMean}
+The processes $(S_{t,a})_{t \in \mathbb{N}}$ and $(\hat{\mu}_{t,a})_{t \in \mathbb{N}}$ are predictable with respect to the filtration $\mathcal{F}$ of the algorithm-environment interaction.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:predictable_pullCount,def:sumRewards,def:empMean}
+
+\end{proof}
+
+
 The following lemma is very useful to relate the two ways of indexing the rewards: by time step and by pull count.
 
 \begin{lemma}\label{lem:sum_rewardByCount}