OAI/GroupTheory/PolycyclicRecognition/Geometry/RootIntervalSupports.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact supports of the actual root interval laws

  1. def OAI.PolycyclicRecognition.rootIntervalSupport line 17

    Source documentation

    The closed interval image carries the complete sampling law.

    def rootIntervalSupport (Exp : L → N) {m : ℕ} (letters : Fin m → I)
    (X : I → L) (s : I → ℝ) (r R : ℝ) (j : ℕ) : Set N :=
…
  2. theorem OAI.PolycyclicRecognition.isCompact_rootIntervalSupport line 22
  3. theorem OAI.PolycyclicRecognition.rootIntervalLaw_ae_mem_support line 28