OAI/NumberTheory/TwoPoint/Bounds/LabeledWordSegments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Splitting a coded word into the main path and its attached witness paths.

  1. def OAI.TwoPointCorrelations.LabeledPrimeWord.segment line 13

    Source documentation

    A segment inherits the original labels, including shared prime classes.

    def segment (w : LabeledPrimeWord ι) (a n : ℕ) : LabeledPrimeWord ι where
…

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord

  2. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.segment_length line 22
  3. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.segment_resample_word line 27
  4. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.segment_realizes line 49