OAI/NumberTheory/TwoPoint/Walks/WordResampling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Numerical resampling preserves the symbolic witness relations.

  1. structure OAI.TwoPointCorrelations.LabeledPrimeWord.PatternEquiv line 17

    Source documentation

    Equality of the symbolic data, with an explicit position-preserving index map.

    structure PatternEquiv (w v : LabeledPrimeWord ι) where
…

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord

  2. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.PatternEquiv.interval line 23
  3. def OAI.TwoPointCorrelations.LabeledPrimeWord.resample line 29

    Source documentation

    Only the numerical tuple products change. Orientations, padding, and labels remain fixed.

    def resample (w : LabeledPrimeWord ι) (value : ι → ℕ) : LabeledPrimeWord ι where
…

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord

  4. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.resample_length line 36
  5. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.resample_realizes line 41
  6. def OAI.TwoPointCorrelations.LabeledPrimeWord.resamplePattern line 46
  7. def OAI.TwoPointCorrelations.comparisonIndexEquiv line 58
  8. lemma OAI.TwoPointCorrelations.comparisonRelation_pattern line 66
  9. theorem OAI.TwoPointCorrelations.WitnessSystemData.relationPattern line 86

    Source documentation

    Every mode decodes to the same expression after changing numerical tuples.

    theorem relationPattern (d : WitnessSystemData n N ι)
    {main main' : LabeledPrimeWord ι} {word word' : Fin n → LabeledPrimeWord ι}
    (hm : LabeledPrimeWord.PatternEquiv main main')
    (hw : ∀ i, LabeledPrimeWord.PatternEquiv (word i) (word' i)) (h : ℕ) (i : d.chosen) :
    (∃ e : (d.relation main word h i).Term ≃ (d.relation main' word' h i).Term,
      ∀ t, (d.relation main' word' h i).monomial (e t) = (d.relation main word h i).monomial t) := by
…

    Mentions: OAI.TwoPointCorrelations.WitnessSystemData, OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.LabeledPrimeWord.PatternEquiv

  10. lemma OAI.TwoPointCorrelations.WitnessSystemData.holds_pattern line 101
  11. lemma OAI.TwoPointCorrelations.WitnessSystemData.triangular_pattern line 112