New algorithm and environment classes

[RemyDegenne]

closes #97

In general, algorithms and environments are given by sequences of kernels that depend on the history of the interaction.
We introduce several Prop-valued classes for properties of those kernels.

New classes:

• IsDeterministicAlg. The kernels describing the algorithm are deterministic. We add definitions for functions such that the kernels are the deterministic kernels of those functions. actionZero at time 0 and nextAction afterwards.
• IsDeterministicEnv. A similar class for environments. With definitions feedbackFunZero and feedbackFun
• IsObliviousEnv. The kernel of the environment depends only on the latest action of the agent and not the prior history. We define a kernel feedbackCondAction : Kernel α R that depends only on the action.

New constructors for environments:

• obliviousEnv. Given a sequence of Kernel α R, build an environment that satisfies IsObliviousEnv. The definition of stationaryEnv is changed to be obliviousEnv for a constant sequence.
• onlineEvalEnv: build an oblivious and deterministic environment from a sequence of functions α → R
• evalEnv, taken from Add the evalEnv environment #98 : oblineEvalEnv for a constant sequence

co-authored by: Gaëtan Serré @gaetanserre

[RemyDegenne]

(In CI for the last commit we can see a very nice feature of our verso tutorials: their CI now fails and I need to reflect the code changes in the tutorials. This is great and will help keep the documentation up to date.)

[gaetanserre]

I find these additions very elegant and complete. I'm wondering if the deterministic kernels in IsDeterministicAlg and IsDeterministicEnv should implement IsDeterministic of leanprover-community/mathlib4#38211 or if it's far-fetched.

[RemyDegenne]

Yes, I intend to use your IsDeterministic definition once it reaches our repository (and I linked to it in the issue that this closes). But first it needs to be merged to Mathlib and then we need to update Mathlib.

[gaetanserre]

(In CI for the last commit we can see a very nice feature of our verso tutorials: their CI now fails and I need to reflect the code changes in the tutorials. This is great and will help keep the documentation up to date.)

Indeed whenever you're using anchor you need the code in the doc and the files to be "str"-equal. However, we could change the way the doc is handled for avoiding code duplication. For example in my repo KernelHom, the verso doc does not use a single anchor by using a meta program I found in a repo of Yuma Mizuno. This main advantage is that you can directly reference names of your project in the verso doc that will be displayed in a similar way than when using anchor (see Examples.lean).