OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborSamplingReindex.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cofinal restriction of the original neighboring samples

  1. def OAI.PolycyclicRecognition.CartanWordModel.NeighborSamplingRow.reindex line 40

    Source documentation

    Every increasing subsequence keeps the original limiting law.

    def NeighborSamplingRow.reindex (u : ℕ → ℕ) (hu : StrictMono u) :
    NeighborSamplingRow T M F hunimod eW π bN cell β X βD
      haarN chartN hchartN pivot B δ Profiles (Λ := Λ) where
…

    Mentions: OAI.PolycyclicRecognition.CartanWordModel.NeighborSamplingRow