OAI/NumberTheory/TwoPoint/Walks/IndexedQuotientPaths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.indexed_chain_quotient_data line 17

   Source documentation

   Forgetting the omitted-label cut retains precisely the original constant intervals. Renaming regular labels therefore supplies actual quotient run data.

   theorem indexed_chain_quotient_data (D : Submodule K (α → K))
       (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α) (rename : α → ι)
       (label : ℕ → α) (coefficient : ℕ → K)
       (first : ℕ × α) (rest : List (ℕ × α))
       (hchain : (first :: rest).IsChain (IndexedRunStep label))
       (hname : ∀ p ∈ first :: rest, regularLabel (rename p.2) = p.2)
       (hline : ∀ p ∈ first :: rest,
         ∃ c : K, D.mkQ (formalDeparture label coefficient p.1) = anchor (rename p.2) +
           c • D.mkQ (Pi.basisFun K α (regularLabel (rename p.2))))
       (hnonzero : ∀ p q, p ∈ first :: rest → q ∈ first :: rest → p.1 < q.1 →
         (∀ t ∈ Ico p.1 q.1, label t = p.2) → (∑ t ∈ Ico p.1 q.1, coefficient t) ≠ 0) :
       QuotientRunData D anchor regularLabel label coefficient first.1 (rename first.2)
   …

   Mentions: OAI.TwoPointCorrelations.IndexedRunStep, OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.QuotientRunData

2. theorem OAI.TwoPointCorrelations.indexed_regular_piece_quotient_data line 56

   Source documentation

   Every nonempty regular piece produced from an actual block has the quotient path data. Its transitions are proved from the indexed scan.

   theorem indexed_regular_piece_quotient_data (D : Submodule K (α → K))
       (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α) (rename : α → ι)
       (label : ℕ → α) (coefficient : ℕ → K) (start len : ℕ)
       (omitted : α → Bool) (first : ℕ × α) (rest : List (ℕ × α))
       (hpiece : Sum.inl (first :: rest) ∈ partitionColumnRuns (fun p => omitted p.2)
         (indexedBlockRuns label start len))
       (hname : ∀ z, omitted z = false → regularLabel (rename z) = z)
       (hline : ∀ t ∈ Ico start (start + len), omitted (label t) = false →
         ∃ c : K, D.mkQ (formalDeparture label coefficient t) = anchor (rename (label t)) +
           c • D.mkQ (Pi.basisFun K α (regularLabel (rename (label t)))))
       (hnonzero : ∀ a b z, start ≤ a → a < b → b ≤ start + len →
         (∀ t ∈ Ico a b, label t = z) → (∑ t ∈ Ico a b, coefficient t) ≠ 0) :
   …

   Mentions: OAI.TwoPointCorrelations.partitionColumnRuns, OAI.TwoPointCorrelations.indexedBlockRuns, OAI.TwoPointCorrelations.formalDeparture