structure RealEquiv.Bits : Type

• get : ℕ → Bit

theorem RealEquiv.Bits.ext_iff {x y : Bits} : x = y ↔ x.get = y.get

theorem RealEquiv.Bits.ext {x y : Bits} (get : x.get = y.get) : x = y

@[instance_reducible]

instance RealEquiv.instInhabitedBits : Inhabited Bits

Equations

• RealEquiv.instInhabitedBits = { default := RealEquiv.instInhabitedBits.default }

def RealEquiv.Bits.map (bs : Bits) (f : Bit → Bit) : Bits

Equations

• bs.map f = { get := fun (i : ℕ) => f (bs.get i) }

def RealEquiv.Bits.drop (bs : Bits) (n : ℕ) : Bits

Equations

• bs.drop n = { get := fun (i : ℕ) => bs.get (n + i) }

def RealEquiv.Bits.tail (bs : Bits) : Bits

Equations

• bs.tail = bs.drop 1

noncomputable def RealEquiv.Bits.indexOf (bs : Bits) (b : Bit) : Option ℕ

Equations

• bs.indexOf b = some (Nat.find! fun (n : ℕ) => bs.get n = b)

def RealEquiv.Bits.take (bs : Bits) (n : ℕ) : List Bit

Equations

• bs.take n = List.map bs.get (List.range n)

def RealEquiv.Bits.invert (bs : Bits) : Bits

Equations

• bs.invert = bs.map Bit.not

def RealEquiv.Bits.cons (bs : Bits) (b : Bit) : Bits

Equations

• bs.cons b = { get := fun (i : ℕ) => match i with | 0 => b | i.succ => bs.get i }

def RealEquiv.Bits.prepend (bs : Bits) (bs₀ : List Bit) : Bits

Equations

• bs.prepend bs₀ = List.foldr (fun (b : Bit) (bs : RealEquiv.Bits) => bs.cons b) bs bs₀

noncomputable def RealEquiv.Bits.getNat (bs : Bits) : ℕ × Bits

Equations

• bs.getNat = ((bs.indexOf 0).getd, bs.drop ((bs.indexOf 0).getd + 1))

def RealEquiv.Bits.inc (bs : Bits) : Bits

Equations

• bs.inc = bs.cons 1

noncomputable def RealEquiv.Bits.end (bs : Bits) : Option Bit

Equations

• bs.end = choose? fun (b : Bit) => eventually fun (x : ℕ) => bs.get x = b

def RealEquiv.bitsToRat (bs : List Bit) : ℚ

Equations

• RealEquiv.bitsToRat bs = ↑(Nat.ofBits (List.map Bit.toBool bs.reverse).toVec) / 2 ^ bs.length

noncomputable def RealEquiv.ofBitsAux₁ (bs : Bits) : ℝ

Equations

• RealEquiv.ofBitsAux₁ bs = Real.mk! (RealEquiv.bitsToRat ∘ bs.take)

noncomputable def RealEquiv.ofBitsAux₂ (neg : Bit) (bs : Bits) : ℝ

Equations

• RealEquiv.ofBitsAux₂ neg bs = match bs.getNat with | (n, bs) => neg.ite (-1) 1 * (↑n + RealEquiv.ofBitsAux₁ bs)

noncomputable def RealEquiv.ofBits (bs : Bits) : ℝ

Equations

• RealEquiv.ofBits bs = match bs.end with | none => RealEquiv.ofBitsAux₂ (bs.get 0) bs.tail | some Bit.B₀ => RealEquiv.ofBitsAux₂ 0 bs | some Bit.B₁ => RealEquiv.ofBitsAux₂ 1 bs.invert.inc

noncomputable def RealEquiv.toBitsAux₁ (r : ℝ) : Bits

Equations

• RealEquiv.toBitsAux₁ r = { get := fun (i : ℕ) => Bit.ofBool (decide (1 < r * 2 ^ (i + 1))) }

noncomputable def RealEquiv.toBits (r : ℝ) : Bits

Equations

• RealEquiv.toBits r = match (((RealEquiv.toBitsAux₁ (|r| - ↑⌊|r|⌋.toNat)).cons 0).prepend (List.replicate ⌊|r|⌋.toNat 1)).end with | none => (((RealEquiv.toBitsAux₁ (|r| - ↑⌊|r|⌋.toNat)).cons 0).prepend (List.replicate ⌊|r|⌋.toNat 1)).cons (Bit.ofBool (decide (r < 0))) | some Bit.B₀ => ((RealEquiv.toBitsAux₁ (|r| - ↑⌊|r|⌋.toNat)).cons 0).prepend (List.replicate ⌊|r|⌋.toNat 1) | some Bit.B₁ => (((RealEquiv.toBitsAux₁ (|r| - ↑⌊|r|⌋.toNat)).cons 0).prepend (List.replicate ⌊|r|⌋.toNat 1)).invert.inc