OAI/NumberTheory/Ostmann/Construction/HistoryGiantSources.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Ostmann.HistoryGiantSource line 11
2. def OAI.Ostmann.HistoryGiantSource.knownBefore line 15
3. def OAI.Ostmann.HistoryGiantSource.eval line 19
4. def OAI.Ostmann.evolveGiantSources line 23
5. theorem OAI.Ostmann.evolveGiantSources_known line 28
6. def OAI.Ostmann.evolveGiantValues line 55

   Source documentation

   This is the actual forward update: the reconstructed pivot becomes one giant, and the giant on the selected branch is retained.

   def evolveGiantValues (p : ℕ → ℤ) : ℕ → ℤ × ℤ → List Bool → ℤ × ℤ
     | _, g, [] => g
     | d, g, b :: path => evolveGiantValues p (d + 1) (p d, if b then g.2 else g.1) path

7. theorem OAI.Ostmann.evolveGiantSources_eval line 59
8. def OAI.Ostmann.historyGiantSources line 69
9. theorem OAI.Ostmann.historyGiantSources_known line 72
10. def OAI.Ostmann.HistoryGiantSource.fixedFactor line 78
11. def OAI.Ostmann.HistoryGiantSource.ancestorLevels line 82
12. def OAI.Ostmann.HistoryGiantSource.nodeValue line 88
13. theorem OAI.Ostmann.HistoryGiantSource.coefficient line 95
14. def OAI.Ostmann.forwardTreeAncestorScheme line 105
15. theorem OAI.Ostmann.forwardTreeAncestorScheme_left line 115
16. theorem OAI.Ostmann.forwardTreeAncestorScheme_right line 124