Skip to content

Commit 3604489

Browse files
committed
Implemented computation of eb distribution
1 parent 8526404 commit 3604489

File tree

2 files changed

+15
-4
lines changed

2 files changed

+15
-4
lines changed

analysis/markov/Linleios/Evolve.lean

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,3 +58,12 @@ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat →
5858

5959
def totalProbability (states : Probabilities) : Probability :=
6060
states.values.sum
61+
62+
def ebDistribution : Probabilities → HashMap Nat Probability :=
63+
HashMap.fold
64+
(
65+
fun acc state p =>
66+
HashMap.mergeWith (fun _ => Add.add) acc
67+
$ singleton ⟨ state.ebCount , p ⟩
68+
)
69+

analysis/markov/Main.lean

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,14 @@ import Linleios
44

55
def env : Environment := makeEnvironment 0.05 0.95 0.90 600 0.75 1 4 7
66

7-
def s0 : Probabilities := default
8-
def sn := simulate env s0 1e-6 2
9-
def pn := totalProbability sn
7+
def sn := simulate env default 1e-6 10
108

119
def main : IO Unit :=
1210
do
1311
let print {α : Type} [Repr α] (x : α) : IO Unit := IO.println (reprPrec x 0).pretty
12+
IO.println ""
1413
print sn
15-
print $ 1 - pn
14+
IO.println ""
15+
print $ ebDistribution sn
16+
IO.println ""
17+
print $ 1 - totalProbability sn

0 commit comments

Comments
 (0)