OAI/MathematicalPhysics/ContinuumCoulomb/Programs/BisectionRegisters.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Common-denominator registers for approximate bisection. Each update doubles the denominator and uses only addition and doubling of numerators; therefore every register gains at most one bit per iteration.

  1. abbrev OAI.ContinuumCoulomb.BisectionRegisters.Registers line 13
  2. def OAI.ContinuumCoulomb.BisectionRegisters.code line 15
  3. def OAI.ContinuumCoulomb.BisectionRegisters.left line 18
  4. def OAI.ContinuumCoulomb.BisectionRegisters.right line 19
  5. def OAI.ContinuumCoulomb.BisectionRegisters.middle line 20
  6. def OAI.ContinuumCoulomb.BisectionRegisters.interval line 22
  7. def OAI.ContinuumCoulomb.BisectionRegisters.step line 25
  8. def OAI.ContinuumCoulomb.BisectionRegisters.initial line 33
  9. theorem OAI.ContinuumCoulomb.BisectionRegisters.initial_den_pos line 36
  10. theorem OAI.ContinuumCoulomb.BisectionRegisters.middle_eq line 39
  11. theorem OAI.ContinuumCoulomb.BisectionRegisters.initial_interval line 46
  12. theorem OAI.ContinuumCoulomb.BisectionRegisters.step_den_pos line 66
  13. theorem OAI.ContinuumCoulomb.BisectionRegisters.double_quotient line 71
  14. theorem OAI.ContinuumCoulomb.BisectionRegisters.step_interval line 77
  15. theorem OAI.ContinuumCoulomb.BisectionRegisters.iterate_interval line 85
  16. def OAI.ContinuumCoulomb.BisectionRegisters.bits line 97
  17. theorem OAI.ContinuumCoulomb.BisectionRegisters.code_length line 100
  18. theorem OAI.ContinuumCoulomb.BisectionRegisters.bits_le_code line 107
  19. theorem OAI.ContinuumCoulomb.BisectionRegisters.code_le_bits line 112
  20. theorem OAI.ContinuumCoulomb.BisectionRegisters.add_bits_le_max line 117
  21. theorem OAI.ContinuumCoulomb.BisectionRegisters.double_int_bits line 128
  22. theorem OAI.ContinuumCoulomb.BisectionRegisters.step_bits line 133
  23. theorem OAI.ContinuumCoulomb.BisectionRegisters.iterate_bits line 142
  24. theorem OAI.ContinuumCoulomb.BisectionRegisters.residual line 152

    Source documentation

    The actual unreduced register execution satisfies the analytic residual bound; all evaluation calls remain inside the initial rational interval.

    theorem residual {a b δ : ℚ} {f : ℝ → ℝ} {evaluate : ℚ → ℚ} {L : ℝ}
    (hδ : 0 ≤ δ) (hab : a ≤ b) (ha : 0 ≤ f a) (hb : f b ≤ 0) (hL : 0 ≤ L)
    (heval : ∀ q ∈ Set.Icc a b, |(evaluate q : ℝ) - f q| ≤ (δ : ℝ))
    (hLip : ∀ x ∈ Set.Icc (a : ℝ) b, ∀ y ∈ Set.Icc (a : ℝ) b,
      |f x - f y| ≤ L * |x - y|) (n : ℕ) :
    |f (middle ((step δ evaluate)^[n] (initial a b)))| ≤
      2 * (δ : ℝ) + L * (((b : ℝ) - a) / 2 ^ n) := by
…

    Mentions: OAI.ContinuumCoulomb.BisectionRegisters.middle, OAI.ContinuumCoulomb.BisectionRegisters.step, OAI.ContinuumCoulomb.BisectionRegisters.initial