Prove a few sorry (#33)

Author: RemyDegenne

LeanBandits/Algorithm.lean

@@ -208,6 +208,43 @@ lemma action_zero_detAlgorithm [MeasurableSingletonClass α] : action 0 =ᵐ[
     simp [detAlgorithm]
   exact ae_of_ae_map (by fun_prop) h_eq
 
+lemma action_eq_eval_comp_hist (n : ℕ) :
+    action (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl
+
+lemma reward_eq_eval_comp_hist (n : ℕ) :
+    reward (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl
+
+lemma measurable_hist_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (hist n) := by
+  simp [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe,
+    measurable_iff_comap_le]
+
+-- todo: due to the type of `Adapted` and the fact that `Iic n → α × R` depends on `n`, we cannot
+-- state that `hist` is adapted.
+
+lemma measurable_action_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (action n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [action_eq_eval_comp_hist, measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
+  refine MeasurableSpace.comap_mono ?_
+  rw [← measurable_iff_comap_le]
+  fun_prop
+
+lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α]
+    [SecondCountableTopology α] [OpensMeasurableSpace α] :
+    Adapted (Learning.filtration α R) action :=
+  fun n ↦ (measurable_action_filtration n).stronglyMeasurable
+
+lemma measurable_reward_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (reward n) := by
+  simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe]
+  rw [reward_eq_eval_comp_hist, measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
+  refine MeasurableSpace.comap_mono ?_
+  rw [← measurable_iff_comap_le]
+  fun_prop
+
+lemma adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R]
+    [SecondCountableTopology R] [OpensMeasurableSpace R] :
+    Adapted (Learning.filtration α R) reward :=
+  fun n ↦ (measurable_reward_filtration n).stronglyMeasurable
+
 lemma action_detAlgorithm_ae_eq
     [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (n : ℕ) :

LeanBandits/Bandit.lean

@@ -121,16 +121,18 @@ lemma integral_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n :
     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
-
 lemma iIndepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] :
-    iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) := by
-  sorry
+    iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) :=
+  iIndepFun_infinitePi (μ := fun (_ : ℕ) ↦ Measure.infinitePi ν) (Ω := fun _ ↦ α → R)
+    (X := fun i u ↦ u) (fun i ↦ by fun_prop)
 
 lemma iIndepFun_eval_streamMeasure'' (ν : Kernel α R) [IsMarkovKernel ν] (a : α) :
-    iIndepFun (fun n ω ↦ ω n a) (Bandit.streamMeasure ν) := by
+    iIndepFun (fun n ω ↦ ω n a) (Bandit.streamMeasure ν) :=
+  (iIndepFun_eval_streamMeasure' ν).comp (g := fun i ω ↦ ω a) (by fun_prop)
+
+lemma iIndepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] :
+    iIndepFun (fun (p : ℕ × α) ω ↦ ω p.1 p.2) (Bandit.streamMeasure ν) := by
+  have h_ind := iIndepFun_eval_streamMeasure' ν
   sorry
 
 lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : ℕ} {a b : α}

LeanBandits/Regret.lean

@@ -193,11 +193,24 @@ lemma stepsUntil_eq_congr {h' : ℕ → α × ℝ} (h_eq : ∀ i ≤ n, arm i h
 
 lemma pullCount_stepsUntil_add_one (h_exists : ∃ s, pullCount a (s + 1) h = m) :
     pullCount a (stepsUntil a m h + 1).toNat h = m := by
-  sorry
+  classical
+  have h_eq := stepsUntil_eq_dite a m h
+  simp only [h_exists, ↓reduceDIte] at h_eq
+  have h' := Nat.find_spec h_exists
+  rw [h_eq]
+  rw [ENat.toNat_add (by simp) (by simp)]
+  simp only [ENat.toNat_coe, ENat.toNat_one]
+  exact h'
 
 lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount a (s + 1) h = m) :
     pullCount a (stepsUntil a m h).toNat h = m - 1 := by
-  sorry
+  have h_arm := arm_eq_of_stepsUntil_eq_coe (n := (stepsUntil a m h).toNat) (a := a) (ω := h) hm ?_
+  swap; · symm; simpa [stepsUntil_eq_top_iff]
+  have h_add_one := pullCount_stepsUntil_add_one h_exists
+  nth_rw 1 [← h_arm] at h_add_one
+  rw [ENat.toNat_add ?_ (by simp), ENat.toNat_one, pullCount_eq_pullCount_add_one] at h_add_one
+  swap; · simpa [stepsUntil_eq_top_iff]
+  grind
 
 section SumRewards