A supermartingale built from the sum of rewards

LeanBandits/Bandit/SumRewards.lean

@@ -455,6 +455,53 @@ lemma probReal_sumRewards_le_sumRewards_le [Fintype α] (h : IsAlgEnvSeq A R alg
 
 section Subgaussian
 
+open Real
+
+lemma superMartingale_exp_sumNoises (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {c : ℝ≥0}
+    (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (t : ℝ) :
+    Supermartingale (fun n ω ↦
+        exp (t * (sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω)
+          - t ^ 2 * c * pullCount A a (n + 1) ω / 2))
+      (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) P := by
+  refine supermartingale_nat (fun n ↦ ?_) (fun n ↦ ?_) (fun n ↦ ?_)
+  · have h1 := h.adapted_sumNoises_add_one a n (μ := fun a ↦ (ν a)[id])
+    have h2 := adapted_pullCount_add_one h.measurable_A h.measurable_R a n
+    fun_prop
+  · sorry
+  · simp_rw [sumNoises_add_one (t := n + 1), pullCount_add_one (t := n + 1)]
+    have h_ae_eq ω :
+        (t * (sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω +
+          if A (n + 1) ω = a then R (n + 1) ω - (ν a)[id] else 0)) -
+        t ^ 2 * c * ↑(pullCount A a (n + 1) ω + if A (n + 1) ω = a then 1 else 0) / 2 =
+        (t * sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω -
+          t ^ 2 * c * (pullCount A a (n + 1) ω) / 2) +
+          if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 else 0 := by
+      simp only [id_eq, Nat.cast_add, Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero]
+      split_ifs with hA <;> ring
+    simp_rw [h_ae_eq, exp_add]
+    calc P[fun ω ↦ exp (t * sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω -
+          t ^ 2 * c * (pullCount A a (n + 1) ω) / 2) *
+      exp (if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 else 0)|
+        IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n]
+    _ =ᵐ[P] (fun ω ↦ exp (t * (sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω) -
+          t ^ 2 * c * (pullCount A a (n + 1) ω) / 2)) *
+      P[fun ω ↦ exp (if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 else 0)|
+        IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] := by
+      apply condExp_mul_of_aestronglyMeasurable_left
+      · have h1 := h.adapted_sumNoises_add_one a n (μ := fun a ↦ (ν a)[id])
+        have h2 := adapted_pullCount_add_one h.measurable_A h.measurable_R a n
+        fun_prop
+      · sorry
+      · sorry
+    _ ≤ᵐ[P] fun ω ↦ exp (t * sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω -
+          t ^ 2 * c * (pullCount A a (n + 1) ω) / 2) := by
+      suffices P[fun ω ↦ exp (if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2
+          else 0) | IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] ≤ᵐ[P] 1 by
+        filter_upwards [this] with ω hω
+        simp only [id_eq, Pi.mul_apply, Pi.one_apply] at ⊢ hω
+        exact mul_le_of_le_one_right (by positivity) hω
+      sorry
+
 omit [DecidableEq α] [StandardBorelSpace α] in
 lemma probReal_sum_le_sum_streamMeasure [Fintype α] {c : ℝ≥0}
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (a : α) (m : ℕ) :

LeanBandits/ForMathlib/SubGaussian.lean

@@ -10,6 +10,25 @@ open scoped ENNReal NNReal
 
 namespace ProbabilityTheory
 
+namespace HasSubgaussianMGF
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω}
+  {μ : Measure Ω} {X : Ω → ℝ} {c : ℝ≥0}
+
+lemma memLp_exp_mul_sub (h : HasSubgaussianMGF 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 : HasSubgaussianMGF 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 HasSubgaussianMGF
+
 namespace HasCondSubgaussianMGF
 
 variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω]
@@ -51,6 +70,68 @@ lemma integrable_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
   simp_rw [exp_sub]
   exact h_int.div_const _
 
+lemma aux {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ mΩ}
+    {p : ℕ → Ω → Prop} [∀ n, DecidablePred (p n)]
+    (h0 : HasSubgaussianMGF (X 0) (c 0) μ)
+    (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ)
+    (hp : IsPredictable ℱ p) (t : ℝ) (n : ℕ) :
+    ∀ q, 1 < q → MemLp (fun ω ↦ exp (∑ i ∈ Finset.range n,
+      if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) q μ := by
+  induction n with
+  | zero =>
+    simp only [Finset.range_zero, Finset.sum_empty, exp_zero]
+    exact fun _ _ ↦ memLp_const _
+  | succ n hn =>
+    intro q hq
+    simp_rw [Finset.sum_range_succ, exp_add]
+    obtain ⟨p1, p2, hp1, hp2, h_triple⟩ :
+        ∃ p1 p2, 1 < p1 ∧ 1 < p2 ∧ ENNReal.HolderTriple p1 p2 q := by
+      refine ⟨2 * q, 2 * q, ?_, ?_, ?_⟩
+      · conv_lhs => rw [← one_mul 1]
+        gcongr
+        simp
+      · conv_lhs => rw [← one_mul 1]
+        gcongr
+        simp
+      · constructor
+        rw [ENNReal.mul_inv (by simp) (by simp), ← ENNReal.div_eq_inv_mul, ENNReal.add_halves]
+    refine MemLp.mul (q := p2) ?_ (hn p1 hp1)
+    cases n with
+    | zero =>
+      have h_Lp := h0.memLp_exp_mul_sub t p2.toNNReal
+      sorry
+    | succ n =>
+      have h_Lp := (h_subG n).memLp_exp_mul_sub t p2.toNNReal
+      sorry
+
+lemma todo_supermartingale_optional {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ mΩ}
+    {p : ℕ → Ω → Prop} [∀ n, DecidablePred (p n)] (hX : Adapted ℱ X)
+    (h0 : HasSubgaussianMGF (X 0) (c 0) μ)
+    (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ)
+    (hp : IsPredictable ℱ p) (t : ℝ) :
+    Supermartingale (fun n ω ↦ exp (∑ i ∈ Finset.range n,
+      if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) ℱ μ := by
+  refine supermartingale_nat (fun n ↦ ?_) (fun n ↦ ?_) (fun n ↦ ?_)
+  · sorry
+  · sorry
+  · simp_rw [Finset.sum_range_succ, exp_add]
+    calc μ[fun ω ↦ exp (∑ i ∈ Finset.range n, if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0) *
+      exp (if p n ω then t * X n ω - c n * t ^ 2 / 2 else 0) | ℱ n]
+    _ =ᵐ[μ] (fun ω ↦ exp (∑ i ∈ Finset.range n,
+        if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) *
+      μ[fun ω ↦ exp (if p n ω then t * X n ω - c n * t ^ 2 / 2 else 0) | ℱ n] := by
+      apply condExp_mul_of_aestronglyMeasurable_left
+      · sorry
+      · sorry
+      · sorry
+    _ ≤ᵐ[μ] fun ω ↦ exp (∑ i ∈ Finset.range n,
+        if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0) := by
+      suffices μ[fun ω ↦ exp (if p n ω then t * X n ω - c n * t ^ 2 / 2 else 0) | ℱ n] ≤ᵐ[μ] 1 by
+        filter_upwards [this] with ω hω
+        simp only [Pi.mul_apply, Pi.one_apply] at ⊢ hω
+        exact mul_le_of_le_one_right (by positivity) hω
+      sorry
+
 end HasCondSubgaussianMGF
 
 namespace HasSubgaussianMGF

LeanBandits/SequentialLearning/FiniteActions.lean

@@ -749,6 +749,9 @@ noncomputable
 def empMean' (n : ℕ) (h : Iic n → α × ℝ) (a : α) :=
   (sumRewards' n h a) / (pullCount' n h a)
 
+def sumNoises (A : ℕ → Ω → α) (R' : ℕ → Ω → ℝ) (μ : α → ℝ) (a : α) (t : ℕ) (ω : Ω) : ℝ :=
+  ∑ s ∈ range t, if A s ω = a then R' s ω - μ a else 0
+
 @[simp]
 lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0 := by ext; simp [sumRewards]
 
@@ -757,6 +760,12 @@ lemma sumRewards_add_one {R' : ℕ → Ω → ℝ} :
   unfold sumRewards
   rw [sum_range_succ]
 
+lemma sumNoises_add_one {R' : ℕ → Ω → ℝ} (μ : α → ℝ) :
+    sumNoises A R' μ a (t + 1) ω =
+      sumNoises A R' μ a t ω + if A t ω = a then R' t ω - μ a else 0 := by
+  unfold sumNoises
+  rw [sum_range_succ]
+
 lemma sumRewards_eq_of_pullCount_eq {R' : ℕ → Ω → ℝ} {s t : ℕ}
     (h_eq : pullCount A a s ω = pullCount A a t ω) :
     sumRewards A R' a s ω = sumRewards A R' a t ω := by
@@ -816,17 +825,13 @@ 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
+lemma sumRewards_sub_pullCount_mul_eq_sumNoises {R' : ℕ → Ω → ℝ} (c : α → ℝ) :
+    sumRewards A R' a n ω - pullCount A a n ω * c a = sumNoises A R' c a n ω := by
+  unfold sumNoises
   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
+  | zero => simp
   | succ n hn =>
-    simp_rw [sumRewards_add_one (t := n + 1), pullCount_add_one (t := n + 1)]
+    simp_rw [sumRewards_add_one (t := n), pullCount_add_one (t := n)]
     split_ifs with ha
     · conv_rhs => rw [sum_range_succ]
       simp only [Nat.cast_add, Nat.cast_one, ha, ↓reduceIte, add_mul, one_mul]
@@ -835,6 +840,12 @@ lemma sumRewards_sub_pullCount_mul_eq_sum {R' : ℕ → Ω → ℝ} (c : α →
       conv_rhs => rw [sum_range_succ]
       simp [ha]
 
+
+lemma sumRewards_sub_pullCount_mul_eq_sumNoises' {R' : ℕ → Ω → ℝ} (c : α → ℝ) :
+    (fun ω ↦ sumRewards A R' a n ω - pullCount A a n ω * c a) = sumNoises A R' c a n := by
+  ext ω
+  exact sumRewards_sub_pullCount_mul_eq_sumNoises c
+
 @[fun_prop]
 lemma measurable_sumRewards [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ}
     (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (t : ℕ) :
@@ -852,6 +863,13 @@ lemma measurable_empMean [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ}
   unfold empMean
   fun_prop
 
+@[fun_prop]
+lemma measurable_sumNoises [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ}
+    (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (μ : α → ℝ) (a : α) (n : ℕ) :
+    Measurable (sumNoises A R' μ a n) := by
+  simp_rw [← sumRewards_sub_pullCount_mul_eq_sumNoises']
+  fun_prop
+
 @[fun_prop]
 lemma measurable_sumRewards' [MeasurableSingletonClass α] (n : ℕ) (a : α) :
     Measurable (fun h ↦ sumRewards' n h a) := by
@@ -895,6 +913,19 @@ lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace α] [Nonempty 
   rw [isPredictable_iff_measurable_add_one] at h_predictable
   exact h_predictable.2
 
+lemma IsAlgEnvSeq.adapted_sumNoises_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 ↦ sumNoises A R' μ a (n + 1)) := by
+  simp_rw [← sumRewards_sub_pullCount_mul_eq_sumNoises']
+  have h1 := h.adapted_sumRewards_add_one a
+  have h2 := adapted_pullCount_add_one h.measurable_A h.measurable_R a
+  refine h1.sub (Adapted.mul ?_ (adapted_const _ _))
+  intro n
+  specialize h2 n
+  fun_prop
+
 section CopiedFromPR
 
 open Set