OAI/NumberTheory/TwoPoint/Walks/CanonicalColumnNames.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.perfectColumnName line 14
2. lemma OAI.TwoPointCorrelations.perfectColumnName_injective line 18
3. lemma OAI.TwoPointCorrelations.perfectColumnName_ne_fresh line 22
4. def OAI.TwoPointCorrelations.canonicalColumnName line 28

   Source documentation

   Perfect classes keep their forest/omitted name. Classes with no perfect occurrence use the index of their first occurrence.

   def canonicalColumnName (label : Fin N → α) (perfect : Finset (Fin N))
       (name : Fin N → ℕ ⊕ ℕ) (i : Fin N) : CanonicalColumnLabel :=
   …

   Mentions: OAI.TwoPointCorrelations.CanonicalColumnLabel

5. lemma OAI.TwoPointCorrelations.canonicalColumnName_of_label_eq line 33
6. theorem OAI.TwoPointCorrelations.canonicalColumnName_eq_iff line 41

   Source documentation

   The only needed naming hypothesis concerns the perfect occurrences. Fresh imperfect classes are separated by their canonical references.

   theorem canonicalColumnName_eq_iff (label : Fin N → α) (perfect : Finset (Fin N))
       (name : Fin N → ℕ ⊕ ℕ)
       (hname : ∀ i ∈ perfect, ∀ j ∈ perfect, name i = name j ↔ label i = label j)
       (i j : Fin N) :
       canonicalColumnName label perfect name i = canonicalColumnName label perfect name j ↔
         label i = label j := by
   …

   Mentions: OAI.TwoPointCorrelations.canonicalColumnName

7. def OAI.TwoPointCorrelations.canonicalPerfectEntries line 68
8. theorem OAI.TwoPointCorrelations.canonical_reference_resolves line 74

   Source documentation

   Looking up the canonical representative yields the intended class name, including when the class has no perfect occurrence.

   theorem canonical_reference_resolves (label : Fin N → α) (perfect : Finset (Fin N))
       (name : Fin N → ℕ ⊕ ℕ) (i : Fin N) :
       resolveColumnReference (canonicalPerfectEntries label perfect name)
         (columnRepresentative label perfect i).val = canonicalColumnName label perfect name i := by
   …

   Mentions: OAI.TwoPointCorrelations.resolveColumnReference, OAI.TwoPointCorrelations.canonicalPerfectEntries, OAI.TwoPointCorrelations.columnRepresentative, OAI.TwoPointCorrelations.canonicalColumnName

9. def OAI.TwoPointCorrelations.columnPositionEntries line 96
10. theorem OAI.TwoPointCorrelations.marked_position_entries line 99
11. theorem OAI.TwoPointCorrelations.canonical_imperfect_reconstruction line 108

    Source documentation

    All imperfect attachments are now verified for the actual occurrence representatives, rather than supplied as lookup assumptions.

    theorem canonical_imperfect_reconstruction (label : Fin N → α) (perfect : Finset (Fin N))
        (name : Fin N → ℕ ⊕ ℕ) :
        attachImperfectLabels (canonicalPerfectEntries label perfect name)
            (canonicalPerfectEntries label perfect name)
            (imperfectColumnReferences (fun i => (columnRepresentative label perfect i).val)
              (columnPositionEntries perfect)) =
          List.ofFn (canonicalColumnName label perfect name) := by
    …

    Mentions: OAI.TwoPointCorrelations.attachImperfectLabels, OAI.TwoPointCorrelations.canonicalPerfectEntries, OAI.TwoPointCorrelations.imperfectColumnReferences, OAI.TwoPointCorrelations.columnRepresentative, OAI.TwoPointCorrelations.columnPositionEntries, OAI.TwoPointCorrelations.canonicalColumnName