OAI/NumberTheory/TwoPoint/Bounds/ObservedColumnNames.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Factor canonical occurrence names through the original observed labels.

  1. def OAI.TwoPointCorrelations.observedColumnName line 11
  2. theorem OAI.TwoPointCorrelations.observedColumnName_at line 17
  3. theorem OAI.TwoPointCorrelations.canonical_forest_name_at_perfect line 25
  4. theorem OAI.TwoPointCorrelations.observed_forest_name_regular line 36

    Source documentation

    On actual perfect regular positions, the canonical class name is the line number produced by the shared forest.

    theorem observed_forest_name_regular (label : Fin n → α) (perfect : Finset (Fin n))
    (regular : Finset α) (number : regular → ℕ) (i : Fin n)
    (hi : i ∈ perfect) (hr : label i ∈ regular) :
    observedColumnName label perfect (forestPerfectName label perfect regular number) (label i) =
      .regular (number ⟨label i, hr⟩) := by
…

    Mentions: OAI.TwoPointCorrelations.observedColumnName, OAI.TwoPointCorrelations.forestPerfectName

  5. theorem OAI.TwoPointCorrelations.observed_forest_name_omitted line 46

    Source documentation

    Omitted perfect classes carry an occurrence index strictly below the original column length, independent of any numerical prime value.

    theorem observed_forest_name_omitted (label : Fin n → α) (perfect : Finset (Fin n))
    (regular : Finset α) (number : regular → ℕ) (i : Fin n)
    (hi : i ∈ perfect) (hr : label i ∉ regular) :
    observedColumnName label perfect (forestPerfectName label perfect regular number) (label i) =
      .omitted (columnRepresentative label perfect i).val := by
…

    Mentions: OAI.TwoPointCorrelations.observedColumnName, OAI.TwoPointCorrelations.forestPerfectName, OAI.TwoPointCorrelations.columnRepresentative

  6. theorem OAI.TwoPointCorrelations.observed_forest_name_eq_iff line 54