Dimension function of a finite factor in Lean via greedy binary digits

To get a dimension function on the projections of a II1 factor without a trace, fix a nested halving e0 >= e1 >= ... with e(n+1) ~ en - e(n+1). Run a greedy algorithm: at step n, subtract a copy of e(n+1) from the remainder if one fits (use if h : MvNLE f r then h.choose else 0 and define remainders by structural recursion). Finite cancellation keeps the remainder after n steps subequivalent to en. Then every q is the strong sum of its greedy pieces, and q ~ q' iff the digits agree. Greedy digits never end in 0111..., because otherwise the remainder would be equivalent to e(n+1). So dim q = sum d_n 2^-(n+1) satisfies both q <~ q' iff dim q <= dim q' and q ~ q' iff dim q = dim q'. For the real part, split tsums with Summable.sum_add_tsum_nat_add and use Summable.tsum_lt_tsum at one zero digit.