OAI/Computability/FourierCircuit/BoundaryActiveCircuit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Common ordered spatial generators for the active boundary DAG. Scalar weights may be arbitrarily large and depend on the modulus; every use is charged.

  1. def OAI.ExactFourier.Boundary.activeWeights line 13
  2. theorem OAI.ExactFourier.Boundary.activeMatrix_blocks line 17
  3. theorem OAI.ExactFourier.Boundary.exists_active_dag line 32
  4. theorem OAI.ExactFourier.Boundary.exists_uniform_active_dag line 75
  5. theorem OAI.ExactFourier.Boundary.exists_uniform_active_price line 116
  6. theorem OAI.ExactFourier.ScalarConvolution.exists_prefix_dag line 151
  7. theorem OAI.ExactFourier.ScalarConvolution.prefix_inv line 171
  8. theorem OAI.ExactFourier.ScalarConvolution.price_prefix line 177
  9. theorem OAI.ExactFourier.MatrixPrice.conjugate_le line 213
  10. theorem OAI.ExactFourier.MatrixPrice.le_conjugate line 222
  11. theorem OAI.ExactFourier.MatrixPrice.scalar line 235
  12. theorem OAI.ExactFourier.MatrixPrice.scalar_unit line 243
  13. theorem OAI.ExactFourier.MatrixPrice.prefix_tensor_price line 251
  14. theorem OAI.ExactFourier.Boundary.exists_boundary_bound line 274