OAI/Computability/FourierTransform/AddressTables.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transposed column address trick: a table of the addition of two f-bit digit vectors. We will be able to charge construction of the whole table.

  1. def OAI.PowerSaving.RAM.xorOrd line 13
  2. def OAI.PowerSaving.RAM.xorTab line 15
  3. lemma OAI.PowerSaving.RAM.digit_prefix line 17
  4. lemma OAI.PowerSaving.RAM.digit_plus line 28
  5. theorem OAI.PowerSaving.RAM.Can.xor_value line 43

    Source documentation

    Assume the input environment supplies arguments to this subcalculation at O(1) cost.

    private theorem xor_value (v : ∀ i, Bits (f i) × Bits (f i))
    (hf : Can m B s w x f (fun _ => 0))
    (ha : Can m B s w x (fun i => (bits (f i)).loc (v i).1) (fun _ => 0))
    (hb : Can m B s w x (fun i => (bits (f i)).loc (v i).2) (fun _ => 0))
    (hB : Small B f) (hd : Small B fun i => 2^f i) :
    Can m B s w x (fun i => (bits (f i)).loc ((v i).1+(v i).2)) f := by
…

    Mentions: OAI.PowerSaving.RAM.Can, OAI.PowerSaving.RAM.Small

  6. theorem OAI.PowerSaving.RAM.Can.xor_prepare line 95
  7. theorem OAI.PowerSaving.RAM.Can.xor_lookup line 129