OAI/NumberTheory/Ostmann/Construction/AtomSourceDescent.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.AtomSourceBefore line 11
2. theorem OAI.Ostmann.AtomSourceBefore.mono line 15
3. def OAI.Ostmann.advanceNatAtomSources line 21
4. theorem OAI.Ostmann.advanceNatAtomSources_before line 25
5. theorem OAI.Ostmann.advanceNatAtomSources_injective line 36
6. def OAI.Ostmann.descendAtomSources line 49

   Source documentation

   The first entry of the path is the root branch. Source indices count the previously reconstructed pivots in root-to-leaf order.

   noncomputable def descendAtomSources {I B : Type*} (role : I → CopyScheduleRole) :
       (h n d : ℕ) → (Fin h → Bool) → (CopyScheduleAtoms role (n + h) → B ⊕ ℕ) →
         CopyScheduleAtoms role n → B ⊕ ℕ
     | 0, _, _, _, source => source
     | h + 1, n, d, path, source =>
       descendAtomSources role h n (d + 1) (Fin.tail path)
         (advanceNatAtomSources role (n + h) d (path 0) source)

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.advanceNatAtomSources

7. theorem OAI.Ostmann.descendAtomSources_before line 57
8. theorem OAI.Ostmann.descendAtomSources_injective line 69
9. def OAI.Ostmann.descendAtomValues line 82
10. theorem OAI.Ostmann.descendAtomSources_eval line 92

    Source documentation

    Evaluating symbolic sources agrees exactly with the successive integer substitutions. This equality does not discard any pivot or outside coordinate.

    theorem descendAtomSources_eval {I B A : Type*} (role : I → CopyScheduleRole)
        (h n d : ℕ) (path : Fin h → Bool) (source : CopyScheduleAtoms role (n + h) → B ⊕ ℕ)
        (C : B → A) (p : ℕ → A) (v : CopyScheduleAtoms role n) :
        Sum.elim C p (descendAtomSources role h n d path source v) =
          descendAtomValues role h n d path p (fun w => Sum.elim C p (source w)) v := by
    …

    Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.descendAtomSources, OAI.Ostmann.descendAtomValues