Rename lemmas

LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

@@ -246,7 +246,7 @@ lemma prob_ucbIndex_le [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     grind
   _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
     gcongr with k hk
-    exact todo hν hσ2 hc a n k (by grind)
+    exact prob_avg_add_sqrt_log_le hν hσ2 hc a n k (by grind)
   _ ≤ (n + 1) * (1 : ℝ≥0∞) / (n + 1) ^ c := by
     simp only [one_div, sum_const, Nat.card_Icc, add_tsub_cancel_right, nsmul_eq_mul, mul_one]
     rw [div_eq_mul_inv ((n : ℝ≥0∞) + 1)]
@@ -289,7 +289,7 @@ lemma prob_ucbIndex_ge [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     grind
   _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
     gcongr with k hk
-    exact todo' hν hσ2 hc a n k (by grind)
+    exact prob_avg_sub_sqrt_log_ge hν hσ2 hc a n k (by grind)
   _ ≤ (n + 1) * (1 : ℝ≥0∞) / (n + 1) ^ c := by
     simp only [one_div, sum_const, Nat.card_Icc, add_tsub_cancel_right, nsmul_eq_mul, mul_one]
     rw [div_eq_mul_inv ((n : ℝ≥0∞) + 1)]

LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean

@@ -443,7 +443,7 @@ end Congruence
 
 section MeasurabilityAdvanced
 
-lemma measurable_hist_todo [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) :
+lemma measurable_hist_comap [Countable 𝓐] (alg : Algorithm 𝓐 R) (n : ℕ) :
     Measurable[MeasurableSpace.comap (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) inferInstance]
       (hist alg · n) := by
   have h_eq : (hist alg · n) =
@@ -648,7 +648,7 @@ variable [StandardBorelSpace R] [Nonempty R]
 lemma indepFun_fst_add_one_hist [Countable 𝓐] (alg : Algorithm 𝓐 R)
     (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (n : ℕ) :
     IndepFun (fun ω ↦ ω.1 (n + 1)) (hist alg · n) (arrayMeasure ν) :=
-  (indepFun_fst_add_one_aux ν n).of_measurable_right (measurable_hist_todo alg n)
+  (indepFun_fst_add_one_aux ν n).of_measurable_right (measurable_hist_comap alg n)
 
 -- proved by Claude
 omit [Nonempty 𝓐] [StandardBorelSpace 𝓐] [StandardBorelSpace R] in
@@ -868,7 +868,7 @@ lemma indepFun_snd_apply_pullCount_action [Countable 𝓐] (alg : Algorithm 𝓐
         pullCount (action alg) a (n + 1) ω = m}).indicator (fun _ ↦ 1) :=
   (indepFun_snd_apply_aux ν a m).of_measurable_right (measurable_stepsUntil alg a m n)
 
-lemma indepFun_todo {𝓐 β γ δ : Type*} {m𝓐 : MeasurableSpace 𝓐} {mβ : MeasurableSpace β}
+lemma indepFun_cond_comp {𝓐 β γ δ : Type*} {m𝓐 : MeasurableSpace 𝓐} {mβ : MeasurableSpace β}
     {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure 𝓐}
     {X : 𝓐 → β} {Y : 𝓐 → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y)
     {Z : γ → δ} (hZ : Measurable Z) (z : δ) :
@@ -919,7 +919,7 @@ lemma indepFun_snd_hist_cond [Countable 𝓐] (alg : Algorithm 𝓐 R)
   have h_meas := measurable_stepsUntil alg a m n
   obtain ⟨f, hf, hf_eq⟩ := h_meas.exists_eq_measurable_comp
   simp_rw [hf_eq]
-  refine indepFun_todo (Z := f) (z := 1) ?_ ?_ hf
+  refine indepFun_cond_comp (Z := f) (z := 1) ?_ ?_ hf
   · exact indepFun_snd_apply_aux ν a m
   · refine Measurable.prodMk (by fun_prop) ?_
     simp_rw [measurable_pi_iff]

LeanMachineLearning/Online/Bandit/SumRewards.lean

@@ -424,7 +424,7 @@ lemma prob_sum_ge_sqrt_log {σ2 : ℝ≥0}
 open Real
 
 omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in
-lemma todo {σ2 : ℝ≥0} {c : ℝ}
+lemma prob_avg_add_sqrt_log_le {σ2 : ℝ≥0} {c : ℝ}
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
     (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) :
     streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(2 * c * σ2 * log (n + 1) / k) ≤ (ν a)[id]} ≤
@@ -450,7 +450,7 @@ lemma todo {σ2 : ℝ≥0} {c : ℝ}
   _ ≤ 1 / (n + 1) ^ c := prob_sum_le_sqrt_log hν hσ2 hc a k hk
 
 omit [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] in
-lemma todo' {σ2 : ℝ≥0} {c : ℝ}
+lemma prob_avg_sub_sqrt_log_ge {σ2 : ℝ≥0} {c : ℝ}
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)) (hσ2 : σ2 ≠ 0)
     (hc : 0 ≤ c) (a : 𝓐) (n k : ℕ) (hk : k ≠ 0) :
     streamMeasure ν

LeanMachineLearning/Probability/Independence/CondDistrib.lean

@@ -171,7 +171,7 @@ lemma Measure.snd_prodAssoc_compProd_prodMkLeft {α β γ : Type*}
   · exact Kernel.measurable_kernel_prodMk_left hs
   · exact hs.preimage (by fun_prop)
 
-lemma Measure.todo {α β γ : Type*}
+lemma Measure.map_swap_comprod_eq_fst_compProd {α β γ : Type*}
     {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
     {μ : Measure (α × β)} [SFinite μ] {κ : Kernel α γ} [IsSFiniteKernel κ] :
     (((((μ ⊗ₘ (κ.prodMkRight β))).map Prod.swap).map MeasurableEquiv.prodAssoc.symm).fst).map
@@ -255,8 +255,9 @@ lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkRight
     rw [condDistrib_ae_eq_iff_measure_eq_compProd _ (by fun_prop)] at h ⊢
     have h_fst : μ.map Z = (μ.map (fun ω ↦ (Z ω, X ω))).fst := by
       rw [Measure.fst_map_prodMk hX]
-    rw [h_fst, ← Measure.todo, ← h, Measure.map_map (by fun_prop) (by fun_prop),
-      Measure.map_map (by fun_prop) (by fun_prop), Measure.fst,
+    rw [h_fst, ← Measure.map_swap_comprod_eq_fst_compProd, ← h,
+      Measure.map_map (by fun_prop) (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop),
+      Measure.fst,
       Measure.map_map (by fun_prop) (by fun_prop), Measure.map_map (by fun_prop) (by fun_prop)]
     congr
   symm

LeanMachineLearning/Tutorial/MarkovKernel.lean

@@ -53,5 +53,3 @@ example (κ : Kernel 𝓧 𝓨) [IsFiniteKernel κ] :
 example (κ : Kernel 𝓧 𝓨) [IsFiniteKernel κ] (x : 𝓧) :
     IsFiniteMeasure (κ x) := inferInstance
 -- ANCHOR_END: Markov
-
-lemma todo : 0 = 0 := rfl

blueprint/lean_decls

@@ -70,7 +70,7 @@ Bandits.ArrayModel.measurable_reward
 Bandits.ArrayModel.hist_congr
 Bandits.ArrayModel.stepsUntil_congr
 Bandits.ArrayModel.truePast
-Bandits.ArrayModel.measurable_hist_todo
+Bandits.ArrayModel.measurable_hist_comap
 Bandits.ArrayModel.measurable_hist_truePast
 Bandits.ArrayModel.measurable_action_add_one_truePast
 Bandits.ArrayModel.measurable_pullCount_add_one_truePast

blueprint/src/chapters/bandit.tex

@@ -174,10 +174,10 @@ \subsection{Measurability}
 \end{definition}
 
 
-\begin{lemma}\label{lem:AM.measurable_hist_todo}
+\begin{lemma}\label{lem:AM.measurable_hist_comap}
   \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets}
 \leanok
-  \lean{Bandits.ArrayModel.measurable_hist_todo, Bandits.ArrayModel.measurable_hist_truePast}
+  \lean{Bandits.ArrayModel.measurable_hist_comap, Bandits.ArrayModel.measurable_hist_truePast}
 For all $t \in \mathbb{N}$, $H_t$ is measurable with respect to the sigma-algebra generated by $F_{1, t}$, and with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$.
 \end{lemma}
 
@@ -195,7 +195,7 @@ \subsection{Measurability}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{def:AM.history,lem:AM.measurable_hist_todo,def:algFunction}
+  \uses{def:AM.history,lem:AM.measurable_hist_comap,def:algFunction}
 
 \end{proof}
 
@@ -208,7 +208,7 @@ \subsection{Measurability}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{def:AM.history,lem:AM.measurable_hist_todo,def:algFunction}
+  \uses{def:AM.history,lem:AM.measurable_hist_comap,def:algFunction}
 
 \end{proof}
 
@@ -263,7 +263,7 @@ \subsection{Independence}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:AM.measurable_hist_todo,lem:AM.indepFun_fst_add_one_aux}
+  \uses{lem:AM.measurable_hist_comap,lem:AM.indepFun_fst_add_one_aux}
 
 \end{proof}
 
@@ -302,7 +302,7 @@ \subsection{Independence}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:AM.measurable_hist_todo,lem:AM.measurable_hist,lem:AM.indepFun_snd_apply_aux,lem:AM.measurable_stepsUntil,def:AM.probSpaceSubsets}
+  \uses{lem:AM.measurable_hist_comap,lem:AM.measurable_hist,lem:AM.indepFun_snd_apply_aux,lem:AM.measurable_stepsUntil,def:AM.probSpaceSubsets}
 
 \end{proof}