OAI/NumberTheory/Ostmann/Construction/ScheduledNodeSources.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.boundAtomSources line 11
2. theorem OAI.Ostmann.boundAtomSources_unbound line 17
3. theorem OAI.Ostmann.boundAtomSources_injective line 24
4. theorem OAI.Ostmann.boundAtomSources_eval line 32
5. def OAI.Ostmann.scheduledReversePath line 40
6. abbrev OAI.Ostmann.scheduledNodeLevel line 44
7. theorem OAI.Ostmann.scheduledNodeLevel_add_depth line 47
8. def OAI.Ostmann.scheduledNodeRootEquiv line 53
9. def OAI.Ostmann.scheduledRawNodeSources line 59
10. theorem OAI.Ostmann.scheduledRawNodeSources_before line 65
11. theorem OAI.Ostmann.scheduledRawNodeSources_injective line 72
12. def OAI.Ostmann.scheduledNodeSources line 82
13. theorem OAI.Ostmann.scheduledNodeSources_injective line 88
14. def OAI.Ostmann.scheduledNodeHSources line 94
15. theorem OAI.Ostmann.scheduledNodeHSources_injective line 100
16. def OAI.Ostmann.scheduledActualSourceScheme line 110

    Source documentation

    In v H_R - w H_L, the left coefficient is the right H source product.

    noncomputable def scheduledActualSourceScheme {I : Type*} [Fintype I]
        (role : I → CopyScheduleRole) (S : Finset ℤ) (n : ℕ) (t : FrequencyTree S n)
        (C : CopyScheduleAtoms role n → ℤ) : PivotDependencyScheme (2 ^ n - 1) :=
    …

    Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.PivotDependencyScheme

17. def OAI.Ostmann.nodeAncestorValues line 116
18. def OAI.Ostmann.scheduledNodeValues line 120
19. theorem OAI.Ostmann.scheduledNodeSources_eval line 130

    Source documentation

    The finite source encoding evaluates to the actual assignment reached by the ancestor substitutions along this node's path.

    theorem scheduledNodeSources_eval {I A : Type*} [Zero A] (role : I → CopyScheduleRole)
        (n : ℕ) (j : Fin (2 ^ n - 1))
        (C : CopyScheduleAtoms role n → A) (p : Fin (2 ^ n - 1) → A)
        (v : CopyScheduleAtoms role (scheduledNodeLevel n j + 1)) :
        Sum.elim C (fun a => p (ancestorNodeIndex n j a)) (scheduledNodeSources role n j v) =
          scheduledNodeValues role n j C p v := by
    …

    Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduledNodeLevel, OAI.Ostmann.ancestorNodeIndex, OAI.Ostmann.scheduledNodeSources, OAI.Ostmann.scheduledNodeValues