OAI/NumberTheory/TwoPoint/Walks/WordRelations.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.relationAdd line 13
2. def OAI.TwoPointCorrelations.relationNeg line 16
3. lemma OAI.TwoPointCorrelations.relationAdd_eval line 20
4. lemma OAI.TwoPointCorrelations.relationNeg_eval line 25
5. lemma OAI.TwoPointCorrelations.relationAdd_contribution line 29
6. lemma OAI.TwoPointCorrelations.relationNeg_contribution line 37
7. lemma OAI.TwoPointCorrelations.relationAdd_support line 45
8. lemma OAI.TwoPointCorrelations.relationNeg_support line 50
9. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.occurrence_has_label line 58
10. theorem OAI.TwoPointCorrelations.LabeledPrimeWord.active_relation line 68

    Source documentation

    The active numerical relation supplies a concrete interval polynomial with the required nonzero coefficient and a distinct controlling label.

    theorem active_relation (w : LabeledPrimeWord ι) (h : ℕ) (value : ι → ℕ)
        (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
        (hw : w.Realizes value) (y : ι) (hy : ActivePrime h w.word (value y)) :
        ∃ c a b, c ≠ y ∧ a ≤ b ∧ b ≤ w.word.length ∧
          primeRelationEvent (w.intervalRelation h a b) y c (fun j => (value j : ℤ)) := by
    …

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.ActivePrime, OAI.TwoPointCorrelations.primeRelationEvent

11. lemma OAI.TwoPointCorrelations.LabeledPrimeWord.intervalRelation_not_mem line 86
12. def OAI.TwoPointCorrelations.comparisonRelation line 98

    Source documentation

    The three contiguous parts of the earlier-departure comparison.

    def comparisonRelation {ι : Type*} [DecidableEq ι]
        (main wi wj : LabeledPrimeWord ι) (h aj ai ri rj : ℕ) :=
    …

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord

13. lemma OAI.TwoPointCorrelations.comparisonRelation_eval line 103
14. lemma OAI.TwoPointCorrelations.comparisonRelation_contribution line 116
15. lemma OAI.TwoPointCorrelations.comparisonRelation_not_mem line 132
16. lemma OAI.TwoPointCorrelations.comparisonRelation_event line 148

    Source documentation

    Simultaneous positivity supplies the comparison congruence, and the exact selected contribution supplies its retained nondegeneracy test.

    lemma comparisonRelation_event {ι : Type*} [DecidableEq ι]
        (main wi wj : LabeledPrimeWord ι) (h aj ai ri rj : ℕ) (value : ι → ℕ)
        (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
        (hm : main.Realizes value) (hi : wi.Realizes value) (hj : wj.Realizes value)
        (hai : ai ≤ main.word.length) (haji : aj ≤ ai) (x : ℤ) (selected control : ι)
        (hwi : PositiveWord h (x + wordDisplacement h (main.word.take ai)) wi.word)
        (hwj : PositiveWord h (x + wordDisplacement h (main.word.take aj)) wj.word)
        (hci : TuplePrimeAt wi.word (value control) ri)
        (hcj : TuplePrimeAt wj.word (value control) rj)
        (hnonzero : ¬(value control : ℤ) ∣
          wordPrimeContribution h main.word (value selected) aj ai +
            wordPrimeContribution h wi.word (value selected) 0 ri -
    …

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordPrimeContribution