Copyright by Dr. Marek A. Suchenek 2012,2013,2014
This material is intended for future publication.
Absolutely positively no copying no printing no sharing no distributing of ANY kind, please.

A proof of

(n+1)⌊Log2[n+1]⌋-(2^(⌊Log2[n+1]⌋+1))+2=(n+1)(Log2[n+1]+ϵ[n+1])-2n

where ϵ is given by the following definition

β[x_]:=1+x-(2^x)

θ[x_]:=⌈x⌉-x

ϵ[x_]:=β[θ[Log2[x]]]

Function ϵ oscillates between 0 and  
1−lg e+lg lg e ≈0.08607133205593432

Plot[{ϵ[n],0.08607133205593431`,1},{n,0.9`,2.2`},PlotTheme->"Classic",PlotStyle-> {Thickness[Small]},AspectRatio->0.6`,Ticks->{{1,1.3862943611198906`,2,22,64,177,355,512,710,1024},{0,0.08607133205593431`,1}}]

Plot[{ϵ[n],0.08607133205593431`,1},{n,1,1100},PlotTheme->"Classic",PlotStyle-> {Thickness[Small]},AspectRatio->.6, Ticks->{{1,2^.4712336270551024`,2,Round[2^4.4712336270551024`],64,Round[2^7.4712336270551024`],Round[2^8.4712336270551024`],512,Round[2^9.4712336270551024`],1024},{0,0.08607133205593431`,1}}]

First I will prove that

x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))=x(Log2[x]+ϵ[x]-1)

Plot[Tooltip[{x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉)),x(Log2[x]+0-1),x(Log2[x]+0.086-1)}],{x,0.00001,3},PlotTheme->"Classic",PlotStyle-> {Thickness[Small]}]

By the definition of ϵ we have

ϵ[x]=1+⌈Log2[x]⌉-Log2[x]-(2^(⌈Log2[x]⌉-Log2[x]))

Hence

ϵ[x]=1+⌈Log2[x]⌉-Log2[x]-((2^(⌈Log2[x]⌉))/(2^(Log2[x])))

ϵ[x]=1+⌈Log2[x]⌉-Log2[x]-((2^(⌈Log2[x]⌉))/x)

Log2[x]+ϵ[x]-1=⌈Log2[x]⌉-((2^(⌈Log2[x]⌉))/x)

x(Log2[x]+ϵ[x]-1)=x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))

This completes the proof of 
x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))=x(Log2[x]+ϵ[x]-1)

Second, I will prove that

x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))-x

1) For Log2[x]∈ℤ, ⌈Log2[x]⌉=Log2[x]=⌊Log2[x]⌋

So,

x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x Log2[x]-(2^(Log2[x]+1))=x Log2[x]-2 (2^(Log2[x]))=x Log2[x]-2x=x Log2[x]-x-x =x Log2[x]-(2^(Log2[x]))-x=x ⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))-x

2) For x ∉ℤ,⌈x⌉-⌊x⌋=1, so

⌊x⌋=⌈x⌉-1.

Thus for Log2[x] ∉ℤ

⌊Log2[x]⌋=⌈Log2[x]⌉-1

So

x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x(⌈Log2[x]⌉-1)-(2^(⌈Log2[x]⌉-1+1))=x(⌈Log2[x]⌉-1)-(2^(⌈Log2[x]⌉-1+1))=x(⌈Log2[x]⌉)-(2^(⌈Log2[x]⌉))-x

This completes the proof of
x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))-x

Third, I will prove that
x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x(Log2[x]+ϵ[x]-2)

Combining

x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))=x(Log2[x]+ϵ[x]-1)

with

x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x⌈Log2[x]⌉-(2^(⌈Log2[x]⌉))-x

yields

x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x(Log2[x]+ϵ[x]-1)-x=

x(Log2[x]+ϵ[x]-2)

This completes the proof of 
x⌊Log2[x]⌋-(2^(⌊Log2[x]⌋+1))=x(Log2[x]+ϵ[x]-2)

Now, putting x = n+1 we get

(n+1)⌊Log2[n+1]⌋-(2^(⌊Log2[n+1]⌋+1))=(n+1)(Log2[n+1]+ϵ[n+1]-2)

This completes the proof.

Optional interesting fact

The function

β[x]=1+Log2[x]-⌊Log2[x]⌋-(2^(Log2[x]-⌊Log2[x]⌋))

similar to ϵ

may be used to linearly interpolate (Subscript[lg, 2])

Plot[Tooltip[{Log2[x],Log2[x]-(1+Log2[x]-⌊Log2[x]⌋-(2^(Log2[x]-⌊Log2[x]⌋)))}],{x,0.00001,4},PlotTheme->"Classic",PlotStyle-> {Thickness[Small]}]

Plot[Tooltip[{Log2[x],Log2[x]-0.08607133205593431`,Log2[x]-(1+Log2[x]-⌊Log2[x]⌋-(2^(Log2[x]-⌊Log2[x]⌋)))}],{x,0.00001,4},PlotTheme->"Classic",PlotStyle-> {Thickness[Small]}]