OAI/NumberTheory/TwoPoint/Bounds/RunTransitionPaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.scanRunTransitions line 14

   Source documentation

   Scan the remaining positions, recording precisely the starts of new runs.

   def scanRunTransitions (runLabel : ℕ → ι) : ℕ → ℕ → ι → List (ℕ × ι)
     | _, 0, _ => []
     | n, len + 1, previous =>
         if runLabel n = previous then scanRunTransitions runLabel (n + 1) len previous
         else (n, runLabel n) :: scanRunTransitions runLabel (n + 1) len (runLabel n)
   
   /-- Local constant-run geometry suffices for the actual greedy transition list;
   no path, run boundaries, or scalar sums are supplied as encoding data. -/

2. theorem OAI.TwoPointCorrelations.scanRunTransitions_data line 22

   Source documentation

   Local constant-run geometry suffices for the actual greedy transition list; no path, run boundaries, or scalar sums are supplied as encoding data.

   theorem scanRunTransitions_data (D : Submodule K (α → K))
       (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α)
       (label : ℕ → α) (coefficient : ℕ → K) (runLabel : ℕ → ι)
       (start finish : ℕ)
       (hlabel : ∀ t ∈ Ico start finish, label t = regularLabel (runLabel t))
       (hline : ∀ t ∈ Ico start finish,
         ∃ c : K, D.mkQ (formalDeparture label coefficient t) = anchor (runLabel t) +
           c • D.mkQ (Pi.basisFun K α (regularLabel (runLabel t))))
       (hnonzero : ∀ a b i, start ≤ a → a < b → b ≤ finish →
         (∀ t ∈ Ico a b, label t = regularLabel i) → (∑ t ∈ Ico a b, coefficient t) ≠ 0)
       (a n len : ℕ) (i : ι) (hsa : start ≤ a) (han : a < n) (hend : n + len ≤ finish)
       (hcurrent : runLabel a = i)
   …

   Mentions: OAI.TwoPointCorrelations.formalDeparture

3. theorem OAI.TwoPointCorrelations.regular_segment_run_data line 61

   Source documentation

   Begin immediately after the first position of a nonempty regular segment.

   theorem regular_segment_run_data (D : Submodule K (α → K))
       (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α)
       (label : ℕ → α) (coefficient : ℕ → K) (runLabel : ℕ → ι)
       (start len : ℕ) (hlen : 0 < len)
       (hlabel : ∀ t ∈ Ico start (start + len), label t = regularLabel (runLabel t))
       (hline : ∀ t ∈ Ico start (start + len),
         ∃ c : K, D.mkQ (formalDeparture label coefficient t) = anchor (runLabel t) +
           c • D.mkQ (Pi.basisFun K α (regularLabel (runLabel t))))
       (hnonzero : ∀ a b i, start ≤ a → a < b → b ≤ start + len →
         (∀ t ∈ Ico a b, label t = regularLabel i) → (∑ t ∈ Ico a b, coefficient t) ≠ 0) :
       QuotientRunData D anchor regularLabel label coefficient start (runLabel start)
         (scanRunTransitions runLabel (start + 1) (len - 1) (runLabel start)) := by
   …

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