OAI/NumberTheory/Ostmann/Construction/AtomAncestorSources.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.atomSourceExtend line 11
2. theorem OAI.Ostmann.atomSourceExtend_ne_last line 27
3. def OAI.Ostmann.advanceAtomSources line 37
4. theorem OAI.Ostmann.advanceAtomSources_injective line 42
5. theorem OAI.Ostmann.reverseCopyLabelMap_map line 50
6. theorem OAI.Ostmann.atomSourceExtend_eval line 58
7. theorem OAI.Ostmann.advanceAtomSources_eval line 65

   Source documentation

   Source evaluation gives the actual reverse assignment, including the newly inserted integral pivot. Earlier pivots retain their original indices.

   theorem advanceAtomSources_eval {I B A : Type*} (role : I → CopyScheduleRole)
       (n d : ℕ) (b : Bool) (source : CopyScheduleAtoms role (n + 1) → B ⊕ Fin d)
       (C : B → A) (p : Fin (d + 1) → A) (v : CopyScheduleAtoms role n) :
       Sum.elim C p (advanceAtomSources role n d b source v) =
         reverseCopyLabelMap role n b (p (Fin.last d))
           (fun w => Sum.elim C (fun j => p j.castSucc) (source w)) v := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.advanceAtomSources, OAI.Ostmann.reverseCopyLabelMap

8. def OAI.Ostmann.atomAncestorSet line 76
9. def OAI.Ostmann.atomFixedProduct line 80
10. theorem OAI.Ostmann.atomSource_product line 86

    Source documentation

    No multiplicity bound is postulated: source injectivity gives exactly the finite set product used by PivotDependencyScheme.

    theorem atomSource_product {A B : Type*} [Fintype A] {d : ℕ}
        (source : A → B ⊕ Fin d) (hs : Function.Injective source)
        (C : B → ℤ) (p : Fin d → ℤ) :
        (∏ a, Sum.elim C p (source a)) =
          ancestorCoefficient (atomFixedProduct source C) (atomAncestorSet source) p := by
    …

    Mentions: OAI.Ostmann.ancestorCoefficient, OAI.Ostmann.atomFixedProduct, OAI.Ostmann.atomAncestorSet