def Hex.TSeries.newton {R : Type u} {n : Nat} (step : TSeries R n → Nat → TSeries R n) (init : TSeries R n) : Nat → TSeries R n

Apply a Newton step k times, passing target precision 2^(j+1) at iteration j.

Equations

• Hex.TSeries.newton step init 0 = init
• Hex.TSeries.newton step init j.succ = step (Hex.TSeries.newton step init j) (2 ^ (j + 1))

def Hex.TSeries.steps (n : Nat) : Nat

Number of doublings needed to reach precision n from precision one.

Equations

• Hex.TSeries.steps n = if n ≤ 1 then 0 else (n - 1).log2 + 1

theorem Hex.TSeries.steps_mono {m n : Nat} (h : m ≤ n) : steps m ≤ steps n

Increasing the requested precision cannot decrease the Newton step count.

theorem Hex.TSeries.newton_agree {R : Type u} {n : Nat} [Zero R] (step : TSeries R n → Nat → TSeries R n) (init : TSeries R n) (stable : ∀ (j : Nat), Agree (2 ^ j) (newton step init (j + 1)) (newton step init j)) {j k : Nat} (hjk : j ≤ k) : Agree (2 ^ j) (newton step init k) (newton step init j)

If every Newton stage preserves the prefix established by the preceding stage, any later iterate agrees with an earlier iterate throughout that prefix.

theorem Hex.TSeries.two_pow_steps_ge (n : Nat) : n ≤ 2 ^ steps n

The Newton step count reaches every requested coefficient.