\(\texttt{LossHistory}\ N\ t\) is the type of length-\(t\) histories of loss vectors for \(N\) experts: it is the function type \(\mathrm{Fin}\, t \to \mathrm{Fin}\, N \to \mathbb {R}\), recording all loss vectors that have been revealed in the past \(t\) rounds.

Given a history \(h : \texttt{LossHistory}\ N\ t\), \(\text{\texttt{LossHistory.toLossSeq}}\ h\) coerces it to a \(\texttt{LossSeq}\ N\ t\), enabling the reuse of definitions and theorems from the pathwise Hedge formalization that are stated over finite loss sequences.

A \(\texttt{LearnerPolicy}\ N\) is a deterministic online strategy for a learner interacting with \(N\) experts: it provides a weight function \(\mathrm{weights} : (t : \mathbb {N}) \to \texttt{LossHistory}\ N\ t \to \mathrm{Fin}\, N \to \mathbb {R}\) together with proofs that the weights are nonnegative and sum to one, so that the weight vector at each round forms a valid mixed strategy.

An \(\texttt{AdaptiveAdversary}\ N\) is an online strategy for the adversary: it provides a loss-selection function \(\mathrm{loss} : (t : \mathbb {N}) \to \texttt{LossHistory}\ N\ t \to (\mathrm{Fin}\, N \to \mathbb {R}) \to \mathrm{Fin}\, N \to \mathbb {R}\) that maps the current round index, the past loss history, and the learner’s current mixed strategy to a loss vector, subject to the validity condition that every coordinate of the chosen loss vector lies in \([0, 1]\).

\(\texttt{hedgePolicy}\ N\ \eta \) is the \(\texttt{LearnerPolicy}\) that implements the Hedge algorithm with learning rate \(\eta \gt 0\): at each round \(t\) and for each loss history \(h\), the weights are given by \(\texttt{hedgeDist}\ \eta \ (\text{\texttt{LossHistory.toLossSeq}}\ h)\ t\), the exponential-weights distribution derived from the past realized losses.

\(\texttt{episodeLossNat}\ \mathrm{learner}\ \mathrm{adversary}\ t : \mathrm{Fin}\, N \to \mathbb {R}\) is the loss vector produced at round \(t\) when the learner and adversary interact adaptively: the adversary sees the prefix of losses from rounds \(0, \ldots , t-1\) and the learner’s mixed strategy for round \(t\), then returns the loss vector for round \(t\). The definition is well-founded because the recursion only refers to strictly earlier rounds.

\(\texttt{episodeLossSeq}\ T\ \mathrm{learner}\ \mathrm{adversary} : \texttt{LossSeq}\ N\ T\) is the finite loss sequence realized over \(T\) rounds by running the learner against the adaptive adversary, obtained by restricting \(\texttt{episodeLossNat}\) to the first \(T\) rounds.

An \(\texttt{Episode}\ N\ T\) packages a learner policy, an adaptive adversary, and a finite loss sequence of length \(T\) for \(N\) experts, together with a consistency proof that the stored loss sequence equals the one generated by running \(\texttt{episodeLossSeq}\ T\ \mathrm{learner}\ \mathrm{adversary}\).

\(\texttt{Episode.generated}\ \mathrm{learner}\ \mathrm{adversary}\) is the canonical \(\texttt{Episode}\ N\ T\) constructed by taking the loss sequence to be exactly \(\texttt{episodeLossSeq}\ T\ \mathrm{learner}\ \mathrm{adversary}\); the consistency condition is satisfied by reflexivity.