From 83d6d772f96975e5f4296229fdb371572878e9f5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 11 May 2026 20:54:37 +0200 Subject: [PATCH] fix names in verso blueprint --- .../LMLBlueprint/Chapters/Algorithm.lean | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean b/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean index 5f185aa6..f8495655 100644 --- a/verso_blueprint/LMLBlueprint/Chapters/Algorithm.lean +++ b/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"}[].