OAI/Computability/FourierTransform/NetworkLabels.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PowerSaving.Cluster.BoxBasis line 8

    Source comment

    Throughout one invocation a product basis for each physical wire.
    abbrev BoxBasis := Box → OBase Blocks

    Mentions: OAI.PowerSaving.Cluster.Box, OAI.PowerSaving.Cluster.Blocks

  2. abbrev OAI.PowerSaving.Cluster.StartAxes line 9
  3. def OAI.PowerSaving.Cluster.basisBox line 11
  4. abbrev OAI.PowerSaving.Cluster.Lab line 16
  5. def OAI.PowerSaving.Cluster.stamp line 17
  6. lemma OAI.PowerSaving.Cluster.stamp_mono line 23
  7. def OAI.PowerSaving.Cluster.bp line 35
  8. def OAI.PowerSaving.Cluster.b0 line 36
  9. def OAI.PowerSaving.Cluster.b1 line 37
  10. def OAI.PowerSaving.Cluster.b2 line 38
  11. def OAI.PowerSaving.Cluster.b3 line 39
  12. def OAI.PowerSaving.Cluster.b4 line 40
  13. def OAI.PowerSaving.Cluster.b5 line 41
  14. def OAI.PowerSaving.Cluster.b6 line 42
  15. def OAI.PowerSaving.Cluster.b7 line 43
  16. def OAI.PowerSaving.Cluster.bend line 44
  17. lemma OAI.PowerSaving.Cluster.inc_bp_b0 line 46
  18. lemma OAI.PowerSaving.Cluster.inc_b0_b1 line 50
  19. lemma OAI.PowerSaving.Cluster.inc_b1_b2 line 57
  20. lemma OAI.PowerSaving.Cluster.inc_b2_b3 line 68
  21. lemma OAI.PowerSaving.Cluster.loss34 line 79
  22. lemma OAI.PowerSaving.Cluster.inc_b4_b5 line 86
  23. lemma OAI.PowerSaving.Cluster.inc_b5_b6 line 100
  24. lemma OAI.PowerSaving.Cluster.inc_b6_b7 line 107
  25. lemma OAI.PowerSaving.Cluster.inc_b7_bend line 114
  26. def OAI.PowerSaving.Cluster.syncBox line 119

    Source documentation

    A support condition checks the Gate/projection interaction.

    def syncBox (j : J) (F : StartAxes) (L : Lab) (Q : Matrix Box Box ℚ) :=
…

    Mentions: OAI.PowerSaving.Cluster.J, OAI.PowerSaving.Cluster.StartAxes, OAI.PowerSaving.Cluster.Lab, OAI.PowerSaving.Cluster.Q, OAI.PowerSaving.Cluster.Box

  27. lemma OAI.PowerSaving.Cluster.upd_same line 123
  28. lemma OAI.PowerSaving.Cluster.sync_J line 127
  29. lemma OAI.PowerSaving.Cluster.sync_R line 144
  30. lemma OAI.PowerSaving.Cluster.sync_V line 154
  31. lemma OAI.PowerSaving.Cluster.sync_G line 171
  32. lemma OAI.PowerSaving.Cluster.sync0 line 180
  33. lemma OAI.PowerSaving.Cluster.sync1 line 186
  34. lemma OAI.PowerSaving.Cluster.sync2 line 188
  35. lemma OAI.PowerSaving.Cluster.sync3 line 194
  36. lemma OAI.PowerSaving.Cluster.sync4 line 196
  37. lemma OAI.PowerSaving.Cluster.sync5 line 198
  38. lemma OAI.PowerSaving.Cluster.sync6 line 204
  39. lemma OAI.PowerSaving.Cluster.sync7 line 206