OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/RadixEncoding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Infinite tape tails and their radix coordinates

Unlike finite prefix interval arithmetic, these lemmas connect the actual infinite symbolic tail to a real point of its coding interval.

  1. def OAI.ForcedComputation.Radix.encode line 18
  2. theorem OAI.ForcedComputation.Radix.summable_bound line 21
  3. theorem OAI.ForcedComputation.Radix.summable_digits line 29
  4. theorem OAI.ForcedComputation.Radix.tsum_bound line 35
  5. theorem OAI.ForcedComputation.Radix.encode_mem_unit line 54
  6. theorem OAI.ForcedComputation.Radix.encode_shift line 64
  7. def OAI.ForcedComputation.Radix.prepend line 80
  8. theorem OAI.ForcedComputation.Radix.encode_prepend line 83
  9. theorem OAI.ForcedComputation.Radix.encode_const line 88
  10. def OAI.ForcedComputation.Radix.prependWord line 98
  11. def OAI.ForcedComputation.Radix.prefixValue line 102
  12. theorem OAI.ForcedComputation.Radix.encode_prependWord line 106
  13. theorem OAI.ForcedComputation.Radix.encode_finite_input line 118

    Source documentation

    A finite input on a blank tail has an explicitly rational radix formula.

    theorem encode_finite_input {B : ℝ} {digit : A → ℝ} (hB : 1 < B)
    (hd : ∀ a, 0 ≤ digit a ∧ digit a ≤ B - 1) (w : List A) (blank : A) :
    encode B digit (prependWord w (fun _ => blank)) =
      prefixValue B digit w + B⁻¹ ^ w.length * (digit blank / (B - 1)) := by
…

    Mentions: OAI.ForcedComputation.Radix.encode, OAI.ForcedComputation.Radix.prependWord, OAI.ForcedComputation.Radix.prefixValue

  14. theorem OAI.ForcedComputation.Radix.encode_in_first_cylinder line 124