OAI/Computability/FourierCircuit/CircuitExtensions.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Finite-index wrappers for the exact charged DAG model. These are used for the state-clearing tensor-axis maps in the cascade and coefficient boundary cost.

  1. theorem OAI.ExactFourier.Program.eval_original line 8
  2. def OAI.ExactFourier.LinearDAG.fanout line 18
  3. theorem OAI.ExactFourier.LinearDAG.size_fanout line 25
  4. theorem OAI.ExactFourier.LinearDAG.eval_fanout line 28
  5. def OAI.ExactFourier.LinearDAG.withInputs line 39

    Source documentation

    Select or duplicate arbitrary existing inputs; these are wire names, not gates.

    noncomputable def LinearDAG.withInputs {m n a : ℕ} (C : LinearDAG n a)
    (f : Fin n → Fin m) : LinearDAG m a := C.comp (.wires (fun i => (f i).castSucc))

    Mentions: OAI.ExactFourier.LinearDAG, OAI.ExactFourier.LinearDAG.wires

  6. theorem OAI.ExactFourier.LinearDAG.size_withInputs line 42
  7. theorem OAI.ExactFourier.LinearDAG.eval_withInputs line 46
  8. def OAI.ExactFourier.LinearDAG.withOutputs line 54

    Source documentation

    Change the ordered output list without performing an arithmetic operation.

    def LinearDAG.withOutputs {n a b : ℕ} (C : LinearDAG n a) (f : Fin b → Fin a) :
    LinearDAG n b := ⟨C.size, C.program, C.outputs ∘ f⟩

    Mentions: OAI.ExactFourier.LinearDAG

  9. theorem OAI.ExactFourier.LinearDAG.eval_withOutputs line 57
  10. def OAI.ExactFourier.LinearDAG.butterflies line 62

    Source documentation

    One butterfly for each of m pairs: charge m scalar multiplications, m additions, and m subtractions, retaining the scaled terms for both output signs.

    def LinearDAG.butterflies {n m : ℕ} (C : LinearDAG n (m+m)) (c : Fin m → ℂ) :
    LinearDAG n (m+m) where
…

    Mentions: OAI.ExactFourier.LinearDAG

  11. theorem OAI.ExactFourier.LinearDAG.eval_butterflies line 72
  12. structure OAI.ExactFourier.TypedDAG line 103
  13. abbrev OAI.ExactFourier.TypedDAG.size line 109
  14. def OAI.ExactFourier.TypedDAG.eval line 110
  15. def OAI.ExactFourier.TypedDAG.comp line 113
  16. theorem OAI.ExactFourier.TypedDAG.size_comp line 115
  17. theorem OAI.ExactFourier.TypedDAG.eval_comp line 117
  18. def OAI.ExactFourier.TypedDAG.inputs line 122
  19. theorem OAI.ExactFourier.TypedDAG.size_inputs line 124
  20. theorem OAI.ExactFourier.TypedDAG.eval_inputs line 126
  21. def OAI.ExactFourier.TypedDAG.outputs line 131
  22. theorem OAI.ExactFourier.TypedDAG.size_outputs line 133
  23. theorem OAI.ExactFourier.TypedDAG.eval_outputs line 135
  24. def OAI.ExactFourier.TypedDAG.fanout line 140
  25. theorem OAI.ExactFourier.TypedDAG.size_fanout line 144
  26. theorem OAI.ExactFourier.TypedDAG.eval_fanout line 146
  27. def OAI.ExactFourier.TypedDAG.wires line 151
  28. theorem OAI.ExactFourier.TypedDAG.size_wires line 154
  29. theorem OAI.ExactFourier.TypedDAG.eval_wires line 155
  30. def OAI.ExactFourier.TypedDAG.matrix line 161
  31. theorem OAI.ExactFourier.TypedDAG.size_matrix line 163
  32. theorem OAI.ExactFourier.TypedDAG.eval_matrix line 165
  33. def OAI.ExactFourier.TypedDAG.scale line 172
  34. theorem OAI.ExactFourier.TypedDAG.size_scale line 174
  35. theorem OAI.ExactFourier.TypedDAG.eval_scale line 175
  36. def OAI.ExactFourier.TypedDAG.addPair line 180
  37. theorem OAI.ExactFourier.TypedDAG.size_addPair line 184
  38. theorem OAI.ExactFourier.TypedDAG.eval_addPair line 185
  39. def OAI.ExactFourier.TypedDAG.stackFin line 190
  40. theorem OAI.ExactFourier.TypedDAG.size_stackFin line 195
  41. theorem OAI.ExactFourier.TypedDAG.eval_stackFin line 201
  42. def OAI.ExactFourier.TypedDAG.stack line 209
  43. theorem OAI.ExactFourier.TypedDAG.size_stack line 212
  44. theorem OAI.ExactFourier.TypedDAG.eval_stack line 216
  45. def OAI.ExactFourier.TypedDAG.parallel line 220
  46. theorem OAI.ExactFourier.TypedDAG.size_parallel line 222
  47. theorem OAI.ExactFourier.TypedDAG.eval_parallel line 224
  48. def OAI.ExactFourier.TypedDAG.tensor line 228
  49. theorem OAI.ExactFourier.TypedDAG.size_tensor line 231
  50. theorem OAI.ExactFourier.TypedDAG.eval_tensor line 235
  51. def OAI.ExactFourier.TypedDAG.blockCols line 256
  52. theorem OAI.ExactFourier.TypedDAG.size_blockCols line 258
  53. theorem OAI.ExactFourier.TypedDAG.eval_blockCols line 260
  54. def OAI.ExactFourier.TypedDAG.scalar line 267
  55. theorem OAI.ExactFourier.TypedDAG.size_scalar line 269
  56. theorem OAI.ExactFourier.TypedDAG.eval_scalar line 271
  57. def OAI.ExactFourier.TypedDAG.identity line 277
  58. theorem OAI.ExactFourier.TypedDAG.size_identity line 278
  59. theorem OAI.ExactFourier.TypedDAG.eval_identity line 279
  60. def OAI.ExactFourier.TypedDAG.tensorPower line 282
  61. theorem OAI.ExactFourier.TypedDAG.eval_tensorPower line 286
  62. theorem OAI.ExactFourier.TypedDAG.size_tensorPower line 294
  63. def OAI.ExactFourier.PolynomialDAG.nodes line 316
  64. def OAI.ExactFourier.PolynomialDAG.weights line 317
  65. theorem OAI.ExactFourier.PolynomialDAG.nodes_injective line 320
  66. theorem OAI.ExactFourier.PolynomialDAG.coeff_interpolate line 326
  67. def OAI.ExactFourier.PolynomialDAG.coefficients line 335
  68. def OAI.ExactFourier.PolynomialDAG.evalMatrix line 337
  69. def OAI.ExactFourier.PolynomialDAG.reconstruct line 340
  70. theorem OAI.ExactFourier.PolynomialDAG.size_reconstruct line 344
  71. theorem OAI.ExactFourier.PolynomialDAG.eval_reconstruct line 349
  72. def OAI.ExactFourier.PolynomialDAG.pad line 367
  73. theorem OAI.ExactFourier.PolynomialDAG.size_pad line 369
  74. theorem OAI.ExactFourier.PolynomialDAG.eval_pad line 371
  75. theorem OAI.ExactFourier.PolynomialDAG.exists_coefficients line 385