fix names in verso blueprint

verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean

@@ -112,7 +112,7 @@ We denote by $`\mathcal{F}^A_t` the sigma-algebra generated by the history up to
 :::
 
 
-:::lemma_ "IsAlgEnvSeq.adapted" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.adapted_step, Learning.IsAlgEnvSeq.adapted_hist, Learning.IsAlgEnvSeq.adapted_action, Learning.IsAlgEnvSeq.adapted_reward")
+:::lemma_ "IsAlgEnvSeq.adapted" (parent := "algorithm_environment") (lean := "Learning.IsAlgEnvSeq.adapted_step, Learning.IsAlgEnvSeq.adapted_hist, Learning.IsAlgEnvSeq.adapted_action, Learning.IsAlgEnvSeq.adapted_feedback")
 The history, step, action and observation processes ({uses "history"}[]) are adapted to the filtration $`(\mathcal{F}_t)_{t \in \mathbb{N}}` ({uses "IsAlgEnvSeq.filtration"}[]).
 :::
 
@@ -144,20 +144,20 @@ Recall that in a stationary environment, there exists a Markov kernel $`\nu : \m
 
 Let $`(A, R, P)` be an algorithm-environment interaction in a stationary environment with kernel $`\nu`.
 
-:::lemma_ "condDistrib_reward_stationaryEnv" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condDistrib_reward_stationaryEnv")
+:::lemma_ "condDistrib_feedback_stationaryEnv" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condDistrib_feedback_stationaryEnv")
 In a {uses "stationaryEnv"}[stationary environment], an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] satisfies for any $`t \in \mathbb{N}`, $`P\left(R_t \mid A_t\right) = \nu`.
 :::
 
-:::proof "condDistrib_reward_stationaryEnv"
+:::proof "condDistrib_feedback_stationaryEnv"
 Uses: {uses "law_step"}[]
 :::
 
 
-::: lemma_ "condIndepFun_reward_hist_action" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condIndepFun_reward_hist_action")
+::: lemma_ "condIndepFun_feedback_hist_action" (parent := "stationary_environment") (lean := "Learning.IsAlgEnvSeq.condIndepFun_feedback_hist_action")
 For an {uses "IsAlgEnvSeq"}[algorithm-environment interaction] in a {uses "stationaryEnv"}[stationary environment], for any $`t \in \mathbb{N}`, the reward $`R_{t+1}` is conditionally independent of the history $`H_t` given the action $`A_{t+1}` (more succinctly, $`R_{t+1} \ind H_t \mid A_{t+1}`).
 :::
 
-:::proof "condIndepFun_reward_hist_action"
+:::proof "condIndepFun_feedback_hist_action"
 :::
 
 
@@ -244,19 +244,19 @@ We now go back to the setting of an algorithm interacting with an environment an
 Likewise, $`\mu = P_0 \otimes \nu'_0` for a probability measure $`P_0` on $`\mathcal{A}` and a Markov kernel $`\nu'_0 : \mathcal{A} \rightsquigarrow \mathcal{R}`.
 The step random variable $`X_t` takes values in $`\mathcal{A} \times \mathcal{R}`.
 
-:::definition "IT.actionReward" (parent := "ionescu_tulcea") (lean := "Learning.IT.action, Learning.IT.reward")
+:::definition "IT.actionReward" (parent := "ionescu_tulcea") (lean := "Learning.IT.action, Learning.IT.feedback")
 We write $`A_t` and $`R_t` for the projections of $`X_t` ({uses "IT.history"}[]) on $`\mathcal{A}` and $`\mathcal{R}` respectively.
 $`A_t` is the action taken at time $`t` and $`R_t` is the reward received at time $`t`.
 Formally, $`A_t(\omega) = \omega_{t,1}` and $`R_t(\omega) = \omega_{t,2}` for $`\omega = \prod_{t=0}^{+\infty}(\omega_{t,1}, \omega_{t,2}) \in \Omega_{\mathcal{T}} = \prod_{t=0}^{+\infty} \mathcal{A} \times \mathcal{R}`.
 :::
 
 
-:::lemma_ "IT.adapted_action_reward" (parent := "ionescu_tulcea") (lean := "Learning.IT.adapted_action, Learning.IT.adapted_reward")
+:::lemma_ "IT.adapted_action_feedback" (parent := "ionescu_tulcea") (lean := "Learning.IT.adapted_action, Learning.IT.adapted_feedback")
 The random variables $`A_t` and $`R_t` ({uses "IT.actionReward"}[]) are $`\mathcal{F}_t`-measurable.
 Said differently, the processes $`(A_t)_{t \in \mathbb{N}}` and $`(R_t)_{t \in \mathbb{N}}` are adapted to the {uses "IT.filtration"}[filtration] $`(\mathcal{F}_t)_{t \in \mathbb{N}}`.
 :::
 
-:::proof "IT.adapted_action_reward"
+:::proof "IT.adapted_action_feedback"
 Uses: {uses "IT.adapted_history"}[].
 :::
 
@@ -275,7 +275,7 @@ Since $`A_{t+1}` is the projection of $`X_{t+1}` on $`\mathcal{A}`, $`P_{\mathca
 :::
 
 
-:::lemma_ "IT.condDistrib_R_add_one" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_reward")
+:::lemma_ "IT.condDistrib_R_add_one" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_feedback")
 For any $`t \in \mathbb{N}`, $`P_{\mathcal{T}}\left(R_{t+1} \mid H_t, A_{t+1}\right) = \nu_t`.
 
 Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "ionescu-tulcea"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "IT.history"}[].
@@ -305,7 +305,7 @@ Uses: {uses "ionescu-tulcea"}[], {uses "IT.history"}[], {uses "IT.law_X_zero"}[]
 :::
 
 
-:::lemma_ "IT.condDistrib_R_zero" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_reward_zero")
+:::lemma_ "IT.condDistrib_R_zero" (parent := "ionescu_tulcea") (lean := "Learning.IT.condDistrib_feedback_zero")
 $`P_{\mathcal{T}}\left(R_0 \mid A_0\right) = \nu'_0`.
 
 Uses: {uses "environment"}[], {uses "algorithm"}[], {uses "IT.actionReward"}[], {uses "trajMeasure"}[], {uses "ionescu-tulcea"}[].