OAI/Computability/FourierCircuit/MultiWord.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.ExactFourier.Packing.Step line 11
  2. def OAI.ExactFourier.Packing.Step.matrix line 18
  3. def OAI.ExactFourier.Packing.Step.kind line 22
  4. def OAI.ExactFourier.Packing.Step.embed line 26
  5. theorem OAI.ExactFourier.Packing.Step.matrix_embed line 30
  6. theorem OAI.ExactFourier.Packing.Step.kind_embed line 36
  7. abbrev OAI.ExactFourier.Packing.Word line 38
  8. def OAI.ExactFourier.Packing.Word.matrix line 41
  9. def OAI.ExactFourier.Packing.Word.calls line 43
  10. def OAI.ExactFourier.Packing.Word.count line 45
  11. def OAI.ExactFourier.Packing.Word.embed line 47
  12. theorem OAI.ExactFourier.Packing.Word.matrix_nil line 49
  13. theorem OAI.ExactFourier.Packing.Word.matrix_cons line 50
  14. theorem OAI.ExactFourier.Packing.Word.matrix_append line 52
  15. theorem OAI.ExactFourier.Packing.Word.calls_append line 54
  16. theorem OAI.ExactFourier.Packing.Word.count_append line 56
  17. theorem OAI.ExactFourier.Packing.Word.matrix_embed line 59
  18. theorem OAI.ExactFourier.Packing.Word.calls_embed line 67
  19. theorem OAI.ExactFourier.Packing.Word.count_embed line 70
  20. theorem OAI.ExactFourier.Packing.Word.unit line 73
  21. def OAI.ExactFourier.Packing.monoWord line 82
  22. def OAI.ExactFourier.Packing.callWord line 83
  23. theorem OAI.ExactFourier.Packing.matrix_monoWord line 84
  24. theorem OAI.ExactFourier.Packing.matrix_callWord line 86
  25. theorem OAI.ExactFourier.Packing.calls_monoWord line 88
  26. theorem OAI.ExactFourier.Packing.calls_callWord line 90
  27. theorem OAI.ExactFourier.Packing.pattern_word line 93
  28. def OAI.ExactFourier.Embedded.sigmaIn line 119
  29. theorem OAI.ExactFourier.Embedded.matrix_sigmaIn line 121
  30. theorem OAI.ExactFourier.Embedded.list_update_prod line 141
  31. theorem OAI.ExactFourier.Embedded.blockDiagonal'_product line 155
  32. theorem OAI.ExactFourier.Embedded.card_complement line 184
  33. theorem OAI.ExactFourier.Embedded.exists_completion line 190

    Source documentation

    Complete a prescribed active-tuple matching with untouched spectator wires.

    theorem exists_completion (e : β ↪ α) (f : β ↪ γ)
    (hcard : Fintype.card α≤Fintype.card γ) :
    ∃ g : α ↪ γ,e.trans g=f := by
…
  34. theorem OAI.ExactFourier.Embedded.realize_active line 206
  35. def OAI.ExactFourier.Embedded.sigmaEmbed line 216
  36. theorem OAI.ExactFourier.Embedded.matrix_sigmaEmbed line 226
  37. theorem OAI.ExactFourier.Packing.Word.matrix_flatten line 284
  38. theorem OAI.ExactFourier.Packing.Word.calls_flatten line 290
  39. def OAI.ExactFourier.Packing.Word.reindex line 296
  40. theorem OAI.ExactFourier.Packing.Word.matrix_reindex line 299
  41. theorem OAI.ExactFourier.Packing.Word.calls_reindex line 302
  42. def OAI.ExactFourier.Packing.Word.blockSum line 308
  43. theorem OAI.ExactFourier.Packing.Word.matrix_blockSum line 311
  44. theorem OAI.ExactFourier.Packing.Word.calls_blockSum line 317
  45. theorem OAI.ExactFourier.Packing.Word.count_blockSum line 322
  46. theorem OAI.ExactFourier.Packing.prod_filter_map line 337

    Source documentation

    Deleting only identity factors preserves a noncommutative product.

    theorem prod_filter_map {X M : Type*} [Monoid M] (L : List X) (p : X→Prop)
    [DecidablePred p] (f : X→M) (hf : ∀ x∈L,¬p x → f x=1) :
    ((L.filter p).map f).prod=(L.map f).prod := by
…

    Mentions: OAI.ExactFourier.L

  47. theorem OAI.ExactFourier.Packing.ordered_padding line 349

    Source documentation

    Physical slot padding retains every local program's exact multiplication order.

    theorem ordered_padding {M : Type*} [Monoid M] {k T : ℕ} (time : Fin k→Fin T)
    (ht : StrictMono time) (f : Fin k→M) :
    (List.ofFn (Function.extend time f (fun _=>1))).prod=(List.ofFn f).prod := by
…