OAI/Computability/FourierCircuit/WordScheduling.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.Packing.scheduledStep line 12
  2. theorem OAI.ExactFourier.Packing.scheduledStep_matrix line 15
  3. theorem OAI.ExactFourier.Packing.scheduledStep_product line 24
  4. def OAI.ExactFourier.Packing.scheduledLayer line 36
  5. theorem OAI.ExactFourier.Packing.scheduledLayer_product line 41

    Source documentation

    Schedule correctness on fixed, disjoint physical supports, including every monomial.

    theorem scheduledLayer_product (W : ∀ p,Word D A (β p)) {T : ℕ}
    (time : ∀ p,Fin (W p).length→Fin T) (ht : ∀ p,StrictMono (time p)) :
    (List.ofFn (scheduledLayer W time)).prod=Matrix.blockDiagonal' (fun p=>(W p).matrix) := by
…

    Mentions: OAI.ExactFourier.Packing.Word, OAI.ExactFourier.Packing.scheduledLayer

  6. def OAI.ExactFourier.Packing.Word.substitute line 71
  7. theorem OAI.ExactFourier.Packing.Word.matrix_substitute line 76
  8. def OAI.ExactFourier.Packing.Word.weight line 85
  9. theorem OAI.ExactFourier.Packing.Word.weight_nil line 87
  10. theorem OAI.ExactFourier.Packing.Word.weight_cons_mono line 88
  11. theorem OAI.ExactFourier.Packing.Word.weight_cons_call line 90
  12. theorem OAI.ExactFourier.Packing.Word.weight_append line 92
  13. theorem OAI.ExactFourier.Packing.Word.weight_embed line 94
  14. theorem OAI.ExactFourier.Packing.Word.weight_reindex line 96
  15. theorem OAI.ExactFourier.Packing.Word.weight_substitute line 100
  16. theorem OAI.ExactFourier.Packing.Word.weight_count line 109
  17. theorem OAI.ExactFourier.MonomialMatrix.inverse line 134
  18. theorem OAI.ExactFourier.MonomialMatrix.submatrix_unit line 149

    Source documentation

    A unit square submatrix of a monomial matrix is monomial.

    theorem submatrix_unit {β : Type} [Fintype β] [DecidableEq β]
 {B : Matrix β β ℂ} (hB : MonomialMatrix B) (e f : α ↪ β)
 (hA : IsUnit (B.submatrix e f)) : MonomialMatrix (B.submatrix e f) := by
…

    Mentions: OAI.ExactFourier.MonomialMatrix

  19. theorem OAI.ExactFourier.Packing.pattern_from_word line 206
  20. theorem OAI.ExactFourier.Packing.word_generates line 220
  21. theorem OAI.ExactFourier.Packing.monomial_of_subsingleton line 226
  22. def OAI.ExactFourier.Packing.shearU line 240
  23. theorem OAI.ExactFourier.Packing.shearU_unit line 242
  24. theorem OAI.ExactFourier.Packing.shearU_not_monomial line 244
  25. theorem OAI.ExactFourier.Packing.shear_word_exists line 257
  26. theorem OAI.ExactFourier.reindex_comp line 300
  27. theorem OAI.ExactFourier.reindex_sum line 304
  28. theorem OAI.ExactFourier.reindex_tensor line 311
  29. theorem OAI.ExactFourier.reindex_inverse line 318
  30. theorem OAI.ExactFourier.Embedded.matrix_domain line 332
  31. def OAI.ExactFourier.Packing.Step.rename line 359
  32. def OAI.ExactFourier.Packing.Word.rename line 362
  33. theorem OAI.ExactFourier.Packing.Word.matrix_rename line 364
  34. theorem OAI.ExactFourier.Packing.Word.weight_rename line 378