OAI/Computability/FourierCircuit/PortMatrices.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.Reindexed.unit line 15
  2. theorem OAI.ExactFourier.Reindexed.mul line 18
  3. theorem OAI.ExactFourier.Reindexed.symm_apply_apply line 22
  4. theorem OAI.ExactFourier.Reindexed.apply_symm_apply line 28
  5. def OAI.ExactFourier.OnePort.splitRight line 39

    Source documentation

    The shared coordinate is explicitly a single PUnit port, not an unspecified padding block.

    def splitRight (ι κ : Type*) : ι × (PUnit ⊕ κ) ≃ ι ⊕ (ι × κ) :=
…
  6. def OAI.ExactFourier.OnePort.splitLeft line 43
  7. def OAI.ExactFourier.OnePort.firstSelected line 49
  8. def OAI.ExactFourier.OnePort.firstRest line 54
  9. def OAI.ExactFourier.OnePort.secondSelected line 59
  10. def OAI.ExactFourier.OnePort.secondRest line 64
  11. theorem OAI.ExactFourier.OnePort.reindex_first_all line 69
  12. theorem OAI.ExactFourier.OnePort.reindex_second_all line 78
  13. theorem OAI.ExactFourier.OnePort.first_factorization line 87
  14. theorem OAI.ExactFourier.OnePort.second_factorization line 94
  15. def OAI.ExactFourier.OnePort.plane line 103

    Source documentation

    The selected row and column have one shared coordinate. Their complement is exactly the Cartesian product of the two unshared data sets.

    def plane : ((α ⊕ PUnit) × (PUnit ⊕ β)) ≃ (((α ⊕ PUnit) ⊕ β) ⊕ (α × β)) where
…
  16. def OAI.ExactFourier.OnePort.unionFirst line 119
  17. def OAI.ExactFourier.OnePort.unionSecond line 122
  18. def OAI.ExactFourier.OnePort.product line 127
  19. theorem OAI.ExactFourier.OnePort.plane_first line 130
  20. theorem OAI.ExactFourier.OnePort.plane_second line 140
  21. theorem OAI.ExactFourier.OnePort.selected_unit line 150
  22. theorem OAI.ExactFourier.OnePort.rest_unit line 157
  23. theorem OAI.ExactFourier.OnePort.union_unit line 166
  24. theorem OAI.ExactFourier.OnePort.product_isUnit line 173
  25. theorem OAI.ExactFourier.OnePort.union_prices line 177
  26. theorem OAI.ExactFourier.OnePort.rest_prices line 187
  27. theorem OAI.ExactFourier.OnePort.selected_product_price line 205
  28. theorem OAI.ExactFourier.OnePort.price line 213
  29. def OAI.ExactFourier.rectangularShear line 249
  30. theorem OAI.ExactFourier.rectangularShear_unit line 252
  31. def OAI.ExactFourier.replayOrder line 257

    Source documentation

    Move the dirty gate memory into a literal identity summand.

    def replayOrder {n a k : ℕ} : ((Fin a ⊕ Fin n) ⊕ Fin k) ≃ ((Fin n ⊕ Fin k) ⊕ Fin a) where
…
  32. theorem OAI.ExactFourier.replayMatrix_reindex line 263
  33. theorem OAI.ExactFourier.MatrixPrice.rectangularShear_bound line 272
  34. theorem OAI.ExactFourier.rectangularShear_mul line 296
  35. theorem OAI.ExactFourier.rectangularShear_inv line 301
  36. theorem OAI.ExactFourier.MatrixPrice.rectangularShear_neg line 308
  37. def OAI.ExactFourier.lowerShear line 313
  38. theorem OAI.ExactFourier.lowerShear_reindex line 316
  39. theorem OAI.ExactFourier.lowerShear_unit line 323
  40. theorem OAI.ExactFourier.MatrixPrice.lowerShear_price line 327
  41. theorem OAI.ExactFourier.signedSwap_monomial line 332
  42. theorem OAI.ExactFourier.twoWay_identity line 338
  43. theorem OAI.ExactFourier.MatrixPrice.twoWay_bound line 347

    Source documentation

    Necessary pre-corner price bound: both the forward and inverse circuits are charged.

    theorem MatrixPrice.twoWay_bound (p : MatrixPrice) {ι : Type}
    [Fintype ι] [DecidableEq ι] (G : Matrix ι ι ℂ) (hG : IsUnit G) :
    2 * p.value G ≤ 2 * p.value (rectangularShear G) + p.value (rectangularShear G⁻¹) := by
…

    Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.rectangularShear