Integrate the code from the branch histories

[marekpetrik]

The branch histories has lean code that matches the writeup in the document. However, since the probability definitions have changed, it is no longer compatible.

It would be good to adapt this code to the new results in the probability space. We do not want to be too hasty if we want to change the basic probability results.

[emily-chandran]

In Histories.lean, I've finished lines 1-83 (provided I've done it correctly!) and am working through line 96.

[emily-chandran]

Update: I made it through line 90 but got stuck on
def tuple2hist : Hist M × α × σ → HistNE M | ⟨h, as⟩ => ⟨h.append as, Nat.le.intro rfl⟩
I'll pause here for now, so feel free to pick up here for anyone else working on it!

[marekpetrik]

Thanks! Can you please also update the LaTeX document accordingly to be compatible with our Lean code definitions?