use new subgaussian lemma

Author: RemyDegenne

LeanBandits/Bandit.lean

@@ -99,6 +99,28 @@ lemma identDistrib_eval_eval_id_streamMeasure (ν : Kernel α R) [IsMarkovKernel
       Measure.map_map (by fun_prop) (by fun_prop)]
     simp
 
+lemma Integrable.congr_identDistrib {Ω Ω' : Type*}
+    {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
+    {μ : Measure Ω} {μ' : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ}
+    (hX : Integrable X μ) (hXY : IdentDistrib X Y μ μ') :
+    Integrable Y μ' := by
+  have hX' : Integrable id (μ.map X) := by
+    rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_fst]
+  rw [hXY.map_eq] at hX'
+  rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_snd] at hX'
+
+lemma integrable_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n : ℕ) (a : α)
+    (h_int : Integrable id (ν a)) :
+    Integrable (fun h : ℕ → α → ℝ ↦ h n a) (Bandit.streamMeasure ν) :=
+  Integrable.congr_identDistrib h_int (identDistrib_eval_eval_id_streamMeasure ν n a).symm
+
+lemma integral_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n : ℕ) (a : α) :
+    ∫ h, h n a ∂(Bandit.streamMeasure ν) = (ν a)[id] := by
+  calc ∫ h, h n a ∂(Bandit.streamMeasure ν)
+  _ = ∫ x, x ∂((Bandit.streamMeasure ν).map (fun h ↦ h n a)) := by
+    rw [integral_map (Measurable.aemeasurable (by fun_prop)) (by fun_prop)]
+  _ = (ν a)[id] := by simp [(hasLaw_eval_eval_streamMeasure ν n a).map_eq]
+
 lemma iIndepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] :
     iIndepFun (fun (p : ℕ × α) ω ↦ ω p.1 p.2) (Bandit.streamMeasure ν) := by
   sorry
@@ -107,13 +129,21 @@ lemma iIndepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] :
     iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) := by
   sorry
 
+lemma iIndepFun_eval_streamMeasure'' (ν : Kernel α R) [IsMarkovKernel ν] (a : α) :
+    iIndepFun (fun n ω ↦ ω n a) (Bandit.streamMeasure ν) := by
+  sorry
+
 lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : ℕ} {a b : α}
     (h : n ≠ m ∨ a ≠ b) :
     IndepFun (fun ω ↦ ω n a) (fun ω ↦ ω m b) (Bandit.streamMeasure ν) := by
   change IndepFun (fun ω ↦ ω (n, a).1 (n, a).2) (fun ω ↦ ω (m, b).1 (m, b).2)
     (Bandit.streamMeasure ν)
   exact (iIndepFun_eval_streamMeasure ν).indepFun (by grind)
 
+lemma indepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) :
+    IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := by
+  sorry
+
 end StreamMeasure
 
 /-- `arm n` is the arm pulled at time `n`. This is a random variable on the measurable space

LeanBandits/ETC.lean

@@ -246,49 +246,38 @@ lemma prob_arm_mul_eq_le (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[i
       sorry
   _ = (𝔓).real {ω | ∑ s ∈ range m, ω.2 s (bestArm ν) ≤ ∑ s ∈ range m, ω.2 s a} := by
     sorry
-  _ = (𝔓).real {ω | m * gap ν a
-      ≤ ∑ s ∈ range m, ((ω.2 s a - (ν a)[id]) - (ω.2 s (bestArm ν) - (ν (bestArm ν))[id]))} := by
-    congr with ω
-    simp only [gap_eq_bestArm_sub, id_eq, sum_sub_distrib, sum_const, card_range, nsmul_eq_mul]
-    ring_nf
-    simp
-  _ = (Bandit.streamMeasure ν).real {ω | m * gap ν a
-      ≤ ∑ s ∈ range m, ((ω s a - (ν a)[id]) - (ω s (bestArm ν) - (ν (bestArm ν))[id]))} := by
-    have : Bandit.streamMeasure ν = (𝔓).map Prod.snd := by rw [← Measure.snd, Bandit.snd_measure]
-    rw [this, measureReal_def, measureReal_def, Measure.map_apply (by fun_prop)]
+  _ = (Bandit.streamMeasure ν).real
+      {ω | ∑ s ∈ range m, ω s (bestArm ν) ≤ ∑ s ∈ range m, ω s a} := by
+    simp_rw [measureReal_def]
+    congr 1
+    rw [← Bandit.snd_measure (etcAlgorithm hK m), Measure.snd_apply]
     · rfl
     · exact measurableSet_le (by fun_prop) (by fun_prop)
   _ ≤ Real.exp (-↑m * gap ν a ^ 2 / 4) := by
     by_cases ha : a = bestArm ν
     · simp [ha]
-    refine (HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun (c := 2) (ε := m * gap ν a)
-      ?_ ?_ ?_).trans_eq ?_
-    · suffices iIndepFun (fun s ω ↦ ω s a - ω s (bestArm ν)) (Bandit.streamMeasure ν) by
-        convert this.comp (fun _ x ↦ x - (ν a)[id] + (ν (bestArm ν))[id]) (by fun_prop) with n h
-        simp only [id_eq, Function.comp_apply]
-        ring
-      suffices iIndepFun (fun s ω ↦ ω s) (Bandit.streamMeasure ν) from
-        this.comp (fun _ x ↦ x a - x (bestArm ν)) (by fun_prop)
-      exact iIndepFun_eval_streamMeasure' ν
+    refine (HasSubgaussianMGF.measure_sum_le_sum_le' (cX := fun _ ↦ 1) (cY := fun _ ↦ 1)
+      ?_ ?_ ?_ ?_ ?_ ?_).trans_eq ?_
+    · exact iIndepFun_eval_streamMeasure'' ν (bestArm ν)
+    · exact iIndepFun_eval_streamMeasure'' ν a
+    · intro i him
+      simp_rw [integral_eval_streamMeasure]
+      refine (hν (bestArm ν)).congr_identDistrib ?_
+      exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
     · intro i him
-      rw [← one_add_one_eq_two]
-      refine HasSubgaussianMGF.sub_of_indepFun ?_ ?_ ?_
-      · refine (hν a).congr_identDistrib ?_
-        exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
-      · refine (hν (bestArm ν)).congr_identDistrib ?_
-        exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
-      · suffices IndepFun (fun ω ↦ ω i a) (fun ω ↦ ω i (bestArm ν)) (Bandit.streamMeasure ν) by
-          exact this.comp (φ := fun x ↦ x - (ν a)[id]) (ψ := fun x ↦ x - (ν (bestArm ν))[id])
-            (by fun_prop) (by fun_prop)
-        exact indepFun_eval_streamMeasure (ν := ν) (by grind)
-    · have : 0 ≤ gap ν a := gap_nonneg
-      positivity
+      simp_rw [integral_eval_streamMeasure]
+      refine (hν a).congr_identDistrib ?_
+      exact (identDistrib_eval_eval_id_streamMeasure _ _ _).symm.sub_const _
+    · exact indepFun_eval_streamMeasure' ν (Ne.symm ha)
+    · gcongr 1 with i him
+      simp_rw [integral_eval_streamMeasure]
+      exact le_bestArm a
     · congr 1
+      simp_rw [integral_eval_streamMeasure]
+      simp only [id_eq, sum_const, card_range, nsmul_eq_mul, mul_one, NNReal.coe_natCast,
+        gap_eq_bestArm_sub, neg_mul]
       field_simp
-      simp_rw [mul_assoc]
-      simp only [NNReal.coe_ofNat, neg_inj, mul_eq_mul_left_iff, ne_eq, OfNat.ofNat_ne_zero,
-        not_false_eq_true, pow_eq_zero_iff]
-      norm_num
+      ring
 
 lemma expectation_pullCount_le (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a))
     (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :

LeanBandits/ForMathlib/SubGaussian.lean

@@ -162,6 +162,19 @@ lemma measure_sum_le_sum_le [IsFiniteMeasure μ]
     · rw [integral_finset_sum _ hY_int]
     · rw [integral_finset_sum _ hX_int]
 
+lemma measure_sum_le_sum_le' [IsFiniteMeasure μ]
+    (hX_indep : iIndepFun X μ) (hY_indep : iIndepFun Y μ)
+    (hX_subG : ∀ i ∈ s, HasSubgaussianMGF (fun ω ↦ X i ω - μ[X i]) (cX i) μ)
+    (hY_subG : ∀ j ∈ t, HasSubgaussianMGF (fun ω ↦ Y j ω - μ[Y j]) (cY j) μ)
+    (h_indep_sum : IndepFun (fun ω ↦ (X · ω)) (fun ω ↦ (Y · ω)) μ)
+    (h_le : ∑ j ∈ t, μ[Y j] ≤ ∑ i ∈ s, μ[X i]) :
+    μ.real {ω | ∑ i ∈ s, X i ω ≤ ∑ j ∈ t, Y j ω}
+      ≤ Real.exp (- (∑ j ∈ t, μ[Y j] - ∑ i ∈ s, μ[X i]) ^ 2
+        / (2 * (∑ i ∈ s, cX i + ∑ j ∈ t, cY j))) := by
+  refine measure_sum_le_sum_le hX_indep hY_indep hX_subG hY_subG ?_ h_le
+  exact h_indep_sum.comp (φ := fun p ↦ ∑ i ∈ s, p i) (ψ := fun p ↦ ∑ j ∈ t, p j)
+    (by fun_prop) (by fun_prop)
+
 end Sum
 
 end HasSubgaussianMGF

LeanBandits/RewardByCountMeasure.lean

@@ -313,6 +313,19 @@ lemma identDistrib_rewardByCount [Countable α] [StandardBorelSpace α] [Nonempt
   aemeasurable_snd := by fun_prop
   map_eq := by rw [(hasLaw_rewardByCount a n hn).map_eq, (hasLaw_rewardByCount a m hm).map_eq]
 
+lemma identDistrib_rewardByCount_id [Countable α] [StandardBorelSpace α] [Nonempty α]
+    (a : α) (n : ℕ) (hn : n ≠ 0) :
+    IdentDistrib (fun ω ↦ rewardByCount a n ω.1 ω.2) id (Bandit.measure alg ν) (ν a) where
+  aemeasurable_fst := by fun_prop
+  aemeasurable_snd := Measurable.aemeasurable <| by fun_prop
+  map_eq := by rw [(hasLaw_rewardByCount a n hn).map_eq, Measure.map_id]
+
+lemma identDistrib_rewardByCount_eval [Countable α] [StandardBorelSpace α] [Nonempty α]
+    (a : α) (n m : ℕ) (hn : n ≠ 0) :
+    IdentDistrib (fun ω ↦ rewardByCount a n ω.1 ω.2) (fun ω ↦ ω m a)
+      (Bandit.measure alg ν) (Bandit.streamMeasure ν) :=
+  (identDistrib_rewardByCount_id a n hn).trans (identDistrib_eval_eval_id_streamMeasure ν m a).symm
+
 lemma iIndepFun_rewardByCount (alg : Algorithm α ℝ) (ν : Kernel α ℝ) [IsMarkovKernel ν] :
     iIndepFun (fun (p : α × ℕ) ω ↦ rewardByCount p.1 p.2 ω.1 ω.2) (Bandit.measure alg ν) := by
   sorry