OAI/Computability/SpaceSimulation/Evaluation/Interpolation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Fifths.Modulus.sum_code line 13

   Source comment

   Use weights over the whole field (simpler than general Lagrange weights). Enumerate by residue code.

   theorem sum_code (f : P.K → P.K) :
       ∑ i ∈ range P.n, f (i : P.K) = ∑ x : P.K, f x := by
   …

2. theorem OAI.Fifths.Modulus.sum_at_top line 25
3. theorem OAI.Fifths.Modulus.dot_mono line 33
4. theorem OAI.Fifths.Modulus.extract line 45
5. def OAI.Fifths.Modulus.Line line 62

   Source documentation

   Line d f v: f fits a low-degree polynomial with coefficient v at d.

   def Line (d : ℕ) (f : P.K → P.K) (v : P.K) : Prop :=
   …

6. theorem OAI.Fifths.Modulus.Line.congr line 67
7. theorem OAI.Fifths.Modulus.Line.zero line 69
8. theorem OAI.Fifths.Modulus.Line.constant line 71
9. theorem OAI.Fifths.Modulus.Line.lin line 73
10. theorem OAI.Fifths.Modulus.Line.mul line 78
11. theorem OAI.Fifths.Modulus.Line.kMul line 84
12. theorem OAI.Fifths.Modulus.Line.add line 86
13. theorem OAI.Fifths.Modulus.Line.sub line 91
14. theorem OAI.Fifths.Modulus.Line.sums line 98
15. theorem OAI.Fifths.Modulus.Line.prods line 104
16. theorem OAI.Fifths.Modulus.Line.evaluate line 111
17. abbrev OAI.Fifths.Modulus.Vec line 123

    Source documentation

    Vec is allowed to have "ghost" coordinates above the finite width. Every packed access uses just first d+1 coordinates. Gives less cast-burdened proofs about loops. The actual registers store only the charged coordinates.

    abbrev Vec := ℕ → P.K

18. def OAI.Fifths.Modulus.augBit line 125
19. def OAI.Fifths.Modulus.aug line 128
20. def OAI.Fifths.Modulus.chooseCoord line 130
21. def OAI.Fifths.Modulus.basis line 133
22. def OAI.Fifths.Modulus.extWord line 138

    Source documentation

    Single fully augmented Boolean-word lookup. Compute word-valued rules coordinate by coordinate this way.

    def extWord (d : ℕ) (f : ℕ → P.K) (v : P.Vec) : P.K :=
    …

23. def OAI.Fifths.Modulus.extTwo line 140
24. def OAI.Fifths.Modulus.shift line 143
25. theorem OAI.Fifths.Modulus.basis_kronecker line 145
26. theorem OAI.Fifths.Modulus.extWord_aug line 169
27. theorem OAI.Fifths.Modulus.extTwo_aug line 176
28. theorem OAI.Fifths.Modulus.basis_shift line 179
29. theorem OAI.Fifths.Modulus.extWord_shift line 189
30. theorem OAI.Fifths.Modulus.extTwo_shiftF line 193
31. theorem OAI.Fifths.Modulus.extTwo_shiftS line 196