OAI/Computability/FourierTransform/NetworkInvocation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PowerSaving.Cluster.DPath line 10

    Source documentation

    Conveniently prove the shear and inverse-transpose shear together.

    def DPath (j : J) (F : StartAxes) (s t : Lab) (M : Q) (d : ℕ) : Prop :=
…

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

  2. lemma OAI.PowerSaving.Cluster.rat_if line 14
  3. lemma OAI.PowerSaving.Cluster.ap_one line 17
  4. lemma OAI.PowerSaving.Cluster.ap_mul line 25
  5. lemma OAI.PowerSaving.Cluster.DPath.of_id line 35
  6. lemma OAI.PowerSaving.Cluster.DPath.trans line 38
  7. lemma OAI.PowerSaving.Cluster.DPath.paired line 49
  8. lemma OAI.PowerSaving.Cluster.DPath.rise line 74
  9. theorem OAI.PowerSaving.Cluster.invocation_path line 79
  10. def OAI.PowerSaving.Cluster.forward line 105

    Source documentation

    Induced logical actions.

    def forward (x : Box→ℂ) : Box→ℂ
  | .inl (.inr i) => x (byy i) + x (bx i)
  | r => x r

    Mentions: OAI.PowerSaving.Cluster.Box, OAI.PowerSaving.Cluster.byy, OAI.PowerSaving.Cluster.bx

  11. def OAI.PowerSaving.Cluster.backward line 109
  12. lemma OAI.PowerSaving.Cluster.ap_add line 113
  13. lemma OAI.PowerSaving.Cluster.ap_sub line 116
  14. lemma OAI.PowerSaving.Cluster.ap_f line 120
  15. lemma OAI.PowerSaving.Cluster.ap_b line 126
  16. theorem OAI.PowerSaving.Cluster.invocation line 132