A picture of [0,oo]

Stream: new members

[Lars Ericson]

Just for fun:
Screenshot-from-2020-12-11-00-19-25.png

[Kenny Lau]

how did you do that?

[Lars Ericson]

In Python in a Jupyter notebook, by hand, after picking out all the definitions, like this:

from graphviz import Digraph
def show(e):
    g = Digraph(comment='Grundbegriffe')
    g.attr(shape='box')
    for a,b in e:
        g.node(a, shape='box')
        g.node(b, shape='box')
        g.edge(a,b)
    return g

show([('probability_space', 'Steinhaus'),
   ('P_I01', 'Steinhaus'),
   ('measure_space', 'probability_space'),
   ('measure', 'probability_measure'),
   ('measure', 'measure_space'),
   ('probability_measure', 'probability_space'),
   ('probability_measure', 'P_I01'),
   ('I01', 'P_I01'),
   ('set', 'I01'),
   ('ℝ', 'I01')
  ])

which gives

Screenshot-from-2020-12-11-09-16-40.png

The notebook is here.

I am trying to teach some friends about approximation of solution to stochastic processes using an ancient book written in a dead language. Because I don't really know anything, in particular, I don't know enough what is trivial window-dressing that I should take for granted, I am stuck on an irrelevant concept on page 3, and I thought Lean might help me clear up my thinking:

Screenshot-from-2020-12-11-09-21-25.png