OAI/Computability/FourierCircuit/CircuitCost.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactFourier.CircuitCost.Realizes line 12
  2. theorem OAI.ExactFourier.CircuitCost.exists_size line 14
  3. def OAI.ExactFourier.CircuitCost.cost line 17
  4. theorem OAI.ExactFourier.CircuitCost.optimal line 21
  5. theorem OAI.ExactFourier.CircuitCost.cost_le line 25
  6. theorem OAI.ExactFourier.CircuitCost.cost_matrix line 29
  7. theorem OAI.ExactFourier.CircuitCost.cost_one line 33
  8. theorem OAI.ExactFourier.CircuitCost.cost_mul line 38
  9. theorem OAI.ExactFourier.CircuitCost.cost_reindex_le line 46
  10. theorem OAI.ExactFourier.CircuitCost.cost_reindex line 58
  11. theorem OAI.ExactFourier.CircuitCost.cost_monomial line 65
  12. theorem OAI.ExactFourier.CircuitCost.cost_sum line 80
  13. theorem OAI.ExactFourier.CircuitCost.cost_tensor line 91
  14. def OAI.ExactFourier.sigmaFinSucc line 108

    Source documentation

    Separating the first output block, without inserting extra coordinates.

    def sigmaFinSucc {n : ℕ} (D : Fin (n+1)→Type) : (Σ i,D i)≃(D 0⊕Σ i : Fin n,D i.succ) where
…
  15. def OAI.ExactFourier.TypedDAG.stackDepFin line 118
  16. theorem OAI.ExactFourier.TypedDAG.size_stackDepFin line 123
  17. theorem OAI.ExactFourier.TypedDAG.eval_stackDepFin line 129
  18. def OAI.ExactFourier.TypedDAG.stackDep line 138
  19. theorem OAI.ExactFourier.TypedDAG.size_stackDep line 143
  20. theorem OAI.ExactFourier.TypedDAG.eval_stackDep line 148
  21. theorem OAI.ExactFourier.CircuitCost.cost_blocks line 161
  22. theorem OAI.ExactFourier.Layered.blocks_fin line 182
  23. theorem OAI.ExactFourier.Layered.blocks line 203
  24. theorem OAI.ExactFourier.Layered.blockDiagonal line 223
  25. theorem OAI.ExactFourier.Layered.transpose line 243
  26. theorem OAI.ExactFourier.Layered.two_reindex line 255
  27. inductive OAI.ExactFourier.Round line 272
  28. theorem OAI.ExactFourier.Round.one line 283
  29. def OAI.ExactFourier.Round.joint line 285
  30. theorem OAI.ExactFourier.Round.joint_length line 288
  31. theorem OAI.ExactFourier.Round.joint_prod line 292
  32. theorem OAI.ExactFourier.Round.joint_all line 308
  33. theorem OAI.ExactFourier.Round.joint_rounds line 327
  34. theorem OAI.ExactFourier.Layered.rounds line 335

    Source documentation

    Finite lists of simultaneous rounds, with identity padding and no change of width.

    theorem rounds {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) :
 ∃ L : List (Matrix α α ℂ),L.length=d ∧ L.prod=M ∧ ∀ X∈L,Round X := by
…

    Mentions: OAI.ExactFourier.Layered, OAI.ExactFourier.L, OAI.ExactFourier.Round