OAI/Computability/FourierCircuit/PiTensor.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.PiTensor.matrix line 11
  2. theorem OAI.ExactFourier.PiTensor.one line 14
  3. theorem OAI.ExactFourier.PiTensor.mul line 24
  4. def OAI.ExactFourier.PiTensor.hom line 32
  5. theorem OAI.ExactFourier.PiTensor.unit line 37
  6. def OAI.ExactFourier.PiTensor.axisCoordinates line 45
  7. theorem OAI.ExactFourier.PiTensor.axisCoordinates_symm line 48
  8. theorem OAI.ExactFourier.PiTensor.axis_matrix line 52
  9. def OAI.ExactFourier.Packing.Word.axis line 95
  10. theorem OAI.ExactFourier.Packing.Word.matrix_axis line 98
  11. theorem OAI.ExactFourier.Packing.Word.count_axis line 102
  12. def OAI.ExactFourier.Packing.Word.tensor line 107
  13. theorem OAI.ExactFourier.Packing.Word.matrix_tensor line 110
  14. theorem OAI.ExactFourier.Packing.Word.count_tensor line 125
  15. def OAI.ExactFourier.Packing.Word.leftTensor line 144
  16. def OAI.ExactFourier.Packing.Word.rightTensor line 146
  17. theorem OAI.ExactFourier.Packing.Word.matrix_leftTensor line 149
  18. theorem OAI.ExactFourier.Packing.Word.matrix_rightTensor line 157
  19. theorem OAI.ExactFourier.Packing.Word.count_leftTensor line 165
  20. theorem OAI.ExactFourier.Packing.Word.count_rightTensor line 170
  21. def OAI.ExactFourier.Packing.Word.kronecker line 175
  22. theorem OAI.ExactFourier.Packing.Word.matrix_kronecker line 178
  23. theorem OAI.ExactFourier.Packing.Word.count_kronecker line 184
  24. def OAI.ExactFourier.Packing.sectorCoordinates line 200

    Source documentation

    The two tensor axes choose block-copy labels independently, even for repeated species.

    def sectorCoordinates (k : σ→ℕ) :
 (Σ p : σ×σ,(Fin (k p.1)×Fin (k p.2))×(E p.1×E p.2)) ≃
 ((Σ s,Fin (k s)×E s)×(Σ s,Fin (k s)×E s)) where
…
  25. def OAI.ExactFourier.Packing.speciesInventory line 208
  26. def OAI.ExactFourier.Packing.sectorMatrix line 212
  27. theorem OAI.ExactFourier.Packing.inventory_tensor_sectors line 218
  28. def OAI.ExactFourier.Packing.colorEquiv line 250
  29. theorem OAI.ExactFourier.Packing.colorEquiv_fst line 254
  30. theorem OAI.ExactFourier.Packing.color_cast_apply line 258
  31. theorem OAI.ExactFourier.Packing.coloredBlock_on line 262
  32. theorem OAI.ExactFourier.Packing.coloredBlock_reindex line 278
  33. theorem OAI.ExactFourier.Packing.exists_colorEquiv line 288

    Source documentation

    Equal multiplicities give an exact color-preserving matching of call blocks.

    theorem exists_colorEquiv
    {τ : Type} {π : Type} {ρ : Type} [Fintype π] [Fintype ρ] [DecidableEq π] [DecidableEq ρ] [Fintype τ] [DecidableEq τ] (u : π→τ) (v : ρ→τ)
    (h : ∀ t,Fintype.card {p // u p=t}=Fintype.card {r // v r=t}) :
    ∃ e : π≃ρ,∀ p,u p=v (e p) := by
…
  34. abbrev OAI.ExactFourier.Packing.optionalDomain line 310
  35. instance OAI.ExactFourier.Packing.optionalDomain_fintype line 313
  36. instance OAI.ExactFourier.Packing.optionalDomain_decEq line 315
  37. def OAI.ExactFourier.Packing.optionalMatrix line 318
  38. def OAI.ExactFourier.Packing.Step.activeTuple line 324
  39. def OAI.ExactFourier.Packing.Step.monoPart line 328
  40. theorem OAI.ExactFourier.Packing.Step.monoPart_monomial line 332
  41. theorem OAI.ExactFourier.Packing.Step.decompose line 338
  42. abbrev OAI.ExactFourier.Packing.CallIndex line 352
  43. def OAI.ExactFourier.Packing.callSite line 354
  44. def OAI.ExactFourier.Packing.activeTo line 362
  45. theorem OAI.ExactFourier.Packing.activeTo_injective line 365
  46. theorem OAI.ExactFourier.Packing.activeTo_surjective line 378
  47. def OAI.ExactFourier.Packing.activeEquiv line 389
  48. theorem OAI.ExactFourier.Packing.activeEquiv_fst line 393
  49. theorem OAI.ExactFourier.Packing.activeEquiv_on line 396
  50. theorem OAI.ExactFourier.Packing.activeEquiv_reindex line 411