delete AuxSums file

Author: RemyDegenne

LeanMachineLearning.lean

@@ -19,7 +19,6 @@ public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBor
 public import LeanMachineLearning.Probability.Moments.SubGaussian
 public import LeanMachineLearning.Probability.Kernel.IonescuTulcea.Traj
 public import LeanMachineLearning.SequentialLearning.Algorithm
-public import LeanMachineLearning.SequentialLearning.Algorithms.AuxSums
 public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
 public import LeanMachineLearning.SequentialLearning.Deterministic
 public import LeanMachineLearning.SequentialLearning.FiniteActions

LeanMachineLearning/SequentialLearning/Algorithms/AuxSums.lean

@@ -5,7 +5,6 @@ Authors: Rémy Degenne
 -/
 module
 
-public import LeanMachineLearning.SequentialLearning.Algorithms.AuxSums
 public import LeanMachineLearning.SequentialLearning.Deterministic
 public import LeanMachineLearning.SequentialLearning.FiniteActions
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
@@ -27,7 +26,48 @@ he action `n % K`.
 open MeasureTheory ProbabilityTheory Finset Learning
 open scoped ENNReal NNReal
 
-namespace Bandits
+section Aux
+
+lemma sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
+    (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) = 1 := by
+  have h_iff (s : ℕ) (hs : s < K) : ⟨s % K, Nat.mod_lt _ hK⟩ = a ↔ s = a := by
+    simp only [Nat.mod_eq_of_lt hs, Fin.ext_iff]
+  calc (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
+  _ = ∑ s ∈ range K, if s = a then 1 else 0 := sum_congr rfl fun s hs ↦ by grind
+  _ = _ := by
+    rw [sum_ite_eq']
+    simp
+
+lemma sum_mod_range_mul {K : ℕ} (hK : 0 < K) (m : ℕ) (a : Fin K) :
+    (∑ s ∈ range (K * m), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) = m := by
+  induction m with
+  | zero => simp
+  | succ n hn =>
+    calc (∑ s ∈ range (K * (n + 1)), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
+    _ = (∑ s ∈ range (K * n + K), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by ring_nf
+    _ = (∑ s ∈ range (K * n), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
+        + (∑ s ∈ Ico (K * n) (K * n + K), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by
+      rw [sum_range_add_sum_Ico]
+      grind
+    _ = n + (∑ s ∈ Ico (K * n) (K * n + K), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by
+      rw [hn]
+    _ = n + (∑ s ∈ range K, if ⟨(s + K * n) % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by
+      congr 1
+      let e : ℕ ↪ ℕ := ⟨fun i : ℕ ↦ i + K * n, fun i j hij ↦ by grind⟩
+      have : Finset.map e (range K) = Ico (K * n) (K * n + K) := by
+        ext x
+        simp only [mem_map, mem_range, Function.Embedding.coeFn_mk, mem_Ico, e]
+        refine ⟨fun h ↦ by grind, fun h ↦ ?_⟩
+        use x - K * n
+        grind
+      rw [← this, Finset.sum_map]
+      congr
+    _ = n + (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := by simp
+    _ = n + 1 := by rw [sum_mod_range hK]
+
+end Aux
+
+namespace Learning
 
 variable {K : ℕ}
 
@@ -123,4 +163,4 @@ lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)]
 
 end RoundRobin
 
-end Bandits
+end Learning