OAI/Computability/FourierCircuit/MonomialTools.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.MonomialMatrix.mul line 10
  2. theorem OAI.ExactFourier.MonomialMatrix.unit line 22
  3. theorem OAI.ExactFourier.MonomialMatrix.pow line 37
  4. theorem OAI.ExactFourier.MonomialMatrix.tensor line 42
  5. theorem OAI.ExactFourier.MonomialMatrix.blockDiagonal line 53

    Source documentation

    A direct sum of signed monomials, indexed in (internal,block) order.

    theorem blockDiagonal
    {α : Type} {β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : β → Matrix α α ℂ) (hA : ∀ b,MonomialMatrix (A b)) :
    MonomialMatrix (Matrix.blockDiagonal A) := by
…

    Mentions: OAI.ExactFourier.MonomialMatrix

  6. def OAI.ExactFourier.permM line 79
  7. theorem OAI.ExactFourier.permM_monomial line 81
  8. theorem OAI.ExactFourier.permM_mul_apply line 85
  9. theorem OAI.ExactFourier.mul_permM_apply line 95
  10. theorem OAI.ExactFourier.permM_inv line 100
  11. theorem OAI.ExactFourier.permM_conj line 106
  12. theorem OAI.ExactFourier.permM_conj_single line 113
  13. theorem OAI.ExactFourier.exists_perm_pair line 122
  14. theorem OAI.ExactFourier.Embedded.matrix_coordinates line 147
  15. theorem OAI.ExactFourier.Embedded.matrix_on line 154
  16. theorem OAI.ExactFourier.Embedded.matrix_off_row line 158
  17. theorem OAI.ExactFourier.Embedded.matrix_off_col line 169
  18. theorem OAI.ExactFourier.Embedded.matrix_one line 180
  19. theorem OAI.ExactFourier.Embedded.matrix_mul line 184
  20. theorem OAI.ExactFourier.Embedded.matrix_comp line 192
  21. theorem OAI.ExactFourier.Embedded.matrix_equiv line 217
  22. theorem OAI.ExactFourier.MonomialMatrix.reindex line 236
  23. theorem OAI.ExactFourier.MonomialMatrix.directSum line 247
  24. theorem OAI.ExactFourier.MonomialMatrix.blockDiagonal' line 257
  25. theorem OAI.ExactFourier.MonomialMatrix.embed line 270
  26. inductive OAI.ExactFourier.PositiveGeneration.Pattern line 285

    Source documentation

    Exact positive pattern: k forward calls, interleaved with arbitrary monomials.

    inductive Pattern (A : Matrix α α ℂ) : ℕ → Matrix α α ℂ → Prop
  | zero (M) (hM : MonomialMatrix M) : Pattern A 0 M
  | succ {k H} (hH : Pattern A k H) (M) (hM : MonomialMatrix M) : Pattern A (k+1) (H*A*M)

    Mentions: OAI.ExactFourier.MonomialMatrix

  27. def OAI.ExactFourier.PositiveGeneration.Statement line 289
  28. theorem OAI.ExactFourier.PositiveGeneration.pattern_unit line 292
  29. theorem OAI.ExactFourier.PositiveGeneration.monomial_of_projectors line 298

    Source documentation

    If every column projector is diagonal, the matrix is monomial.

    theorem monomial_of_projectors (A : Matrix α α ℂ) (hA : IsUnit A)
    (hp : ∀ k i j,i≠j → A i k*A⁻¹ k j=0) : MonomialMatrix A := by
…

    Mentions: OAI.ExactFourier.MonomialMatrix

  30. theorem OAI.ExactFourier.PositiveGeneration.exists_nondiagonal_projector line 336
  31. def OAI.ExactFourier.PositiveGeneration.changeSign line 354
  32. def OAI.ExactFourier.PositiveGeneration.doubleCoord line 355
  33. theorem OAI.ExactFourier.PositiveGeneration.changeSign_square line 357
  34. theorem OAI.ExactFourier.PositiveGeneration.changeSign_inv line 361
  35. theorem OAI.ExactFourier.PositiveGeneration.changeSign_monomial line 363
  36. theorem OAI.ExactFourier.PositiveGeneration.doubleCoord_monomial line 367
  37. theorem OAI.ExactFourier.PositiveGeneration.doubleCoord_inv line 371
  38. def OAI.ExactFourier.PositiveGeneration.cut line 376
  39. theorem OAI.ExactFourier.PositiveGeneration.cut_apply line 378
  40. theorem OAI.ExactFourier.PositiveGeneration.double_cut line 383
  41. theorem OAI.ExactFourier.PositiveGeneration.isolate_identity line 390
  42. theorem OAI.ExactFourier.PositiveGeneration.single_mem_of_offdiagonal line 400