OAI/NumberTheory/TwoPointCorrelations/ColumnRepresentatives.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.columnRepresentativeCandidates line 15

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:15 (same declaration text).

2. lemma OAI.TwoPointCorrelations.columnRepresentativeCandidates_nonempty line 20

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:20 (same declaration text).

3. def OAI.TwoPointCorrelations.columnRepresentative line 28

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:28 (same declaration text).

4. lemma OAI.TwoPointCorrelations.columnRepresentative_mem line 32

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:32 (same declaration text).

5. theorem OAI.TwoPointCorrelations.columnRepresentative_label line 37

   Source documentation

   A reference always carries the intended label.

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:37 (same declaration text).

   theorem columnRepresentative_label (label : Fin N → α) (perfect : Finset (Fin N)) (i : Fin N) :
       label (columnRepresentative label perfect i) = label i := by
   …

   Mentions: OAI.TwoPointCorrelations.columnRepresentative

6. theorem OAI.TwoPointCorrelations.columnRepresentative_perfect line 44

   Source documentation

   Perfect occurrences are preferred whenever the class has one.

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:44 (same declaration text).

   theorem columnRepresentative_perfect (label : Fin N → α) (perfect : Finset (Fin N)) (i : Fin N)
       (h : ∃ j ∈ perfect, label j = label i) : columnRepresentative label perfect i ∈ perfect := by
   …

   Mentions: OAI.TwoPointCorrelations.columnRepresentative

7. theorem OAI.TwoPointCorrelations.columnRepresentative_imperfect line 55

   Source documentation

   An unrepresented class refers to its first occurrence, which is necessarily imperfect; two such classes cannot share a reference.

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:55 (same declaration text).

   theorem columnRepresentative_imperfect (label : Fin N → α) (perfect : Finset (Fin N)) (i : Fin N)
       (h : ¬∃ j ∈ perfect, label j = label i) : columnRepresentative label perfect i ∉ perfect := by
   …

   Mentions: OAI.TwoPointCorrelations.columnRepresentative

8. theorem OAI.TwoPointCorrelations.columnRepresentative_eq_iff line 60

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:60 (same declaration text).

9. theorem OAI.TwoPointCorrelations.columnRepresentative_first line 76

   Source documentation

   In the absence of a perfect representative, the selected occurrence precedes every other occurrence in its class.

   Also declared: OAI/NumberTheory/TwoPoint/Walks/ColumnRepresentatives.lean:76 (same declaration text).

   theorem columnRepresentative_first (label : Fin N → α) (perfect : Finset (Fin N)) (i : Fin N)
       (h : ¬∃ j ∈ perfect, label j = label i) (j : Fin N) (hj : label j = label i) :
       columnRepresentative label perfect i ≤ j := by
   …

   Mentions: OAI.TwoPointCorrelations.columnRepresentative