OAI/Computability/FourierTransform/ScalarNetwork.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Scalar portion of one invocation.

  1. abbrev OAI.PowerSaving.Cluster.Center line 10
  2. abbrev OAI.PowerSaving.Cluster.Side line 11
  3. abbrev OAI.PowerSaving.Cluster.Aux line 12
  4. abbrev OAI.PowerSaving.Cluster.XY line 13
  5. abbrev OAI.PowerSaving.Cluster.Box line 14
  6. instance OAI.PowerSaving.Cluster.boxDec line 15
  7. abbrev OAI.PowerSaving.Cluster.bx line 17
  8. abbrev OAI.PowerSaving.Cluster.byy line 18
  9. abbrev OAI.PowerSaving.Cluster.bs line 19
  10. abbrev OAI.PowerSaving.Cluster.bc line 20
  11. def OAI.PowerSaving.Cluster.vlocal line 22
  12. def OAI.PowerSaving.Cluster.wgt line 25
  13. def OAI.PowerSaving.Cluster.jlocal line 27
  14. def OAI.PowerSaving.Cluster.glocal line 30
  15. def OAI.PowerSaving.Cluster.rlocal line 34
  16. abbrev OAI.PowerSaving.Cluster.rmat line 38
  17. theorem OAI.PowerSaving.Cluster.rg_entry line 40
  18. theorem OAI.PowerSaving.Cluster.jv_entry line 54
  19. theorem OAI.PowerSaving.Cluster.rg_jv line 66

    Source documentation

    Crucial projection identity.

    theorem rg_jv : rmat * glocal + jlocal * vlocal = 1 := by
…

    Mentions: OAI.PowerSaving.Cluster.rmat, OAI.PowerSaving.Cluster.glocal, OAI.PowerSaving.Cluster.jlocal, OAI.PowerSaving.Cluster.vlocal

  20. abbrev OAI.PowerSaving.Cluster.Q line 81
  21. def OAI.PowerSaving.Cluster.takeAux line 83
  22. def OAI.PowerSaving.Cluster.giveAux line 84
  23. def OAI.PowerSaving.Cluster.eV line 86
  24. def OAI.PowerSaving.Cluster.eG line 87
  25. def OAI.PowerSaving.Cluster.eJ line 88
  26. def OAI.PowerSaving.Cluster.eR line 89
  27. def OAI.PowerSaving.Cluster.eXY line 91
  28. theorem OAI.PowerSaving.Cluster.zero_VV line 93
  29. theorem OAI.PowerSaving.Cluster.zero_GG line 95
  30. theorem OAI.PowerSaving.Cluster.zero_JJ line 97
  31. theorem OAI.PowerSaving.Cluster.zero_RR line 99
  32. theorem OAI.PowerSaving.Cluster.zero_XX line 101
  33. def OAI.PowerSaving.Cluster.net line 105

    Source documentation

    Multiplier from the eight rows (chronologically right to left).

    def net : Q :=
…

    Mentions: OAI.PowerSaving.Cluster.Q

  34. theorem OAI.PowerSaving.Cluster.rect_commute line 108
  35. theorem OAI.PowerSaving.Cluster.net_eq line 113
  36. theorem OAI.PowerSaving.Cluster.inv_one_add line 146

    Source documentation

    Inverse partner.

    theorem inv_one_add {X : Q} (hh : X*X=0) : (1+X)*(1-X)=1 := by
…

    Mentions: OAI.PowerSaving.Cluster.Q

  37. theorem OAI.PowerSaving.Cluster.inv_one_sub line 148