Refactor: Iic -> Fin

[RemyDegenne]

I got annoyed by the duplication that we have everywhere because of the special case of the first action and feedback. Here is the old definition of Environment:

/-- A stochastic environment. -/
structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Distribution of the next observation as function of the past history. -/
  feedback : (n : ℕ) → Kernel ((Iic n → 𝓐 × 𝓨) × 𝓐) 𝓨
  /-- The feedback kernels are Markov kernels. -/
  [h_feedback : ∀ n, IsMarkovKernel (feedback n)]
  /-- Distribution of the first observation given the first action. -/
  ν0 : Kernel 𝓐 𝓨
  /-- The initial observation kernel is a Markov kernel. -/
  [hp0 : IsMarkovKernel ν0]

We have to do a separate lemma for the feedback given by ν0 every time because it does not have the same shape as feedback n. But it could have the same shape! I changed both Algorithm and Environment to have only one data field:

-- A stochastic environment. -/
structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Distribution of the feedback at time `n` as function of the history of the `n` previous
  action-feedback pairs and of the action at time `n`. -/
  feedback : (n : ℕ) → Kernel ((Fin n → 𝓐 × 𝓨) × 𝓐) 𝓨
  /-- The feedback kernels are Markov kernels. -/
  [h_feedback : ∀ n, IsMarkovKernel (feedback n)]

The trick is that Fin 0 → 𝓐 × 𝓨 is a type with a unique element, so Kernel ((Fin 0 → 𝓐 × 𝓨) × 𝓐) 𝓨 is equivalent to Kernel 𝓐 𝓨 and we can recover our ν0 that way (and I introduced a definition for easy access to that simpler kernel). Then feedback (n+1) in the new formulation corresponds to feedback n in the old one (we already had that shifted indexing for things like obliviousEnv, which gets simpler in the new formulation). It reduces a lot of duplication of lemmas and proofs. Of course it also introduces a little friction with the Ionescu-Tulcea theorem of Mathlib that is written with Iic (which was the reason for the Iic choice in LML), but it's localized to a few files at the beginning.

[paulorauber]

This is a massive improvement! Having to deal with different time conventions was indeed a sign that something was off.

I have only lightly reviewed the code.