Cleanup: letters used for types, names

.github/workflows/blueprint.yml

@@ -53,13 +53,13 @@ jobs:
 
       - name: Build Verso Documentation
         run: |
-          ./scripts/build_tutorial.sh
+          ./build_tutorial.sh
 
       - name: Compile blueprint and documentation
         uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14
         with:
           homepage: home_page
-          blueprint: true
+          blueprint: false
           build-page: false
           deploy: false
 

LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean

@@ -66,16 +66,16 @@ variable {hK : 0 < K} {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
 lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) :
     IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m - 1) where
-  measurable_A := h.measurable_A
-  measurable_R := h.measurable_R
+  measurable_action := h.measurable_action
+  measurable_feedback := h.measurable_feedback
   hasLaw_action_zero := h.hasLaw_action_zero
-  hasCondDistrib_reward_zero := h.hasCondDistrib_reward_zero
+  hasCondDistrib_feedback_zero := h.hasCondDistrib_feedback_zero
   hasCondDistrib_action n hn := by
     convert h.hasCondDistrib_action n using 1
     simp only [roundRobinAlgorithm, detAlgorithm_policy, etcAlgorithm]
     congr 1 with h
     simp [ETC.nextArm, hn]
-  hasCondDistrib_reward n _ := h.hasCondDistrib_reward n
+  hasCondDistrib_feedback n _ := h.hasCondDistrib_feedback n
 
 section AlgorithmBehavior
 
@@ -229,7 +229,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
     (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
     P[fun ω ↦ (pullCount A a n ω : ℝ)]
       ≤ m + (n - K * m) * Real.exp (- (m : ℝ) * gap ν a ^ 2 / (4 * σ2)) := by
-  have hA := h.measurable_A
+  have hA := h.measurable_action
   have : (fun ω ↦ (pullCount A a n ω : ℝ))
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator (fun _ ↦ 1) ω := by
     filter_upwards [pullCount_of_ge h a hm hn] with ω h

LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean

@@ -67,16 +67,16 @@ variable {hK : 0 < K} {c : ℝ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν]
 lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) :
     IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1) where
-  measurable_A := h.measurable_A
-  measurable_R := h.measurable_R
+  measurable_action := h.measurable_action
+  measurable_feedback := h.measurable_feedback
   hasLaw_action_zero := h.hasLaw_action_zero
-  hasCondDistrib_reward_zero := h.hasCondDistrib_reward_zero
+  hasCondDistrib_feedback_zero := h.hasCondDistrib_feedback_zero
   hasCondDistrib_action n hn := by
     convert h.hasCondDistrib_action n using 1
     simp only [roundRobinAlgorithm, detAlgorithm_policy, ucbAlgorithm]
     congr 1 with h
     simp [UCB.nextArm, hn]
-  hasCondDistrib_reward n _ := h.hasCondDistrib_reward n
+  hasCondDistrib_feedback n _ := h.hasCondDistrib_feedback n
 
 section AlgorithmBehavior
 
@@ -452,16 +452,15 @@ lemma constSum_lt_top (c : ℝ) (n : ℕ) : constSum c n < ∞ := by
   simp only [one_div, ENNReal.inv_lt_top]
   positivity
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Bound on the expectation of the number of pulls of each arm by the UCB algorithm. -/
 lemma expectation_pullCount_le' [Nonempty (Fin K)]
     (h : IsAlgEnvSeq A R (ucbAlgorithm hK (c * σ2)) (stationaryEnv ν) P)
     (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a))
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) :
     ∫⁻ ω, pullCount A a n ω ∂P ≤
       ENNReal.ofReal (8 * c * σ2 * log (n + 1) / gap ν a ^ 2 + 1) + 1 + 2 * constSum c n := by
-  have hA := h.measurable_A
-  have hR := h.measurable_R
+  have hA := h.measurable_action
+  have hR := h.measurable_feedback
   by_cases hn_zero : n = 0
   · simp [hn_zero]
   let C a : ℕ := ⌈8 * c * σ2 * log (n + 1) / gap ν a ^ 2⌉₊
@@ -549,7 +548,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
     (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a) (n : ℕ) :
     P[fun ω ↦ (pullCount A a n ω : ℝ)] ≤
       8 * c * σ2 * log (n + 1) / gap ν a ^ 2 + 2 + 2 * (constSum c n).toReal := by
-  have hA := h.measurable_A
+  have hA := h.measurable_action
   have h := expectation_pullCount_le' h hν hσ2 hc a h_gap n (hK := hK)
   simp_rw [← ENNReal.ofReal_natCast] at h
   rw [← ofReal_integral_eq_lintegral_ofReal] at h