OAI/GroupTheory/PolycyclicRecognition/Algebra/BundleParameterCharts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.rectangularCoordinateChart line 12

   Source documentation

   A coordinate permutation followed by currying.

   def rectangularCoordinateChart {h n M : ℕ} (e : Fin h × Fin n ≃ Fin M) :
       (Fin M → ℝ) ≃L[ℝ] (Fin h → Fin n → ℝ) :=
   …

2. theorem OAI.PolycyclicRecognition.rectangularCoordinateChart_apply line 22
3. def OAI.PolycyclicRecognition.bundleParameterIndex line 28

   Source documentation

   First all first samples, then all second samples; each block is grouped by bundle before the generator position.

   def bundleParameterIndex (h m : ℕ) :
       Fin h × Fin (m + m) ≃ Fin (h * m + h * m) :=
   …

4. def OAI.PolycyclicRecognition.bundleParameterChart line 34
5. def OAI.PolycyclicRecognition.bundleOutputChart line 38
6. theorem OAI.PolycyclicRecognition.bundleParameterIndex_left line 42
7. theorem OAI.PolycyclicRecognition.bundleParameterIndex_right line 50
8. theorem OAI.PolycyclicRecognition.bundleParameterChart_left line 58
9. theorem OAI.PolycyclicRecognition.bundleParameterChart_right line 64