OAI/NumberTheory/Ostmann/Construction/History.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Ostmann.Construction.SlotRole line 10
  2. structure OAI.Ostmann.Construction.SmallSlot line 16
  3. structure OAI.Ostmann.Construction.State line 23
  4. def OAI.Ostmann.Construction.State.values line 32
  5. def OAI.Ostmann.Construction.State.product line 34
  6. def OAI.Ostmann.Construction.State.Coprime line 36
  7. def OAI.Ostmann.Construction.State.Positive line 39
  8. def OAI.Ostmann.Construction.State.PrimeSmall line 41
  9. def OAI.Ostmann.Construction.State.TemplateAt line 43
  10. theorem OAI.Ostmann.Construction.State.templateAt_restore line 46
  11. inductive OAI.Ostmann.Construction.History line 61
  12. def OAI.Ostmann.Construction.History.root line 69
  13. def OAI.Ostmann.Construction.History.frequencies line 73
  14. def OAI.Ostmann.Construction.History.internalOccurrences line 77
  15. def OAI.Ostmann.Construction.History.leafStates line 81
  16. theorem OAI.Ostmann.Construction.History.leafStates_length line 85
  17. theorem OAI.Ostmann.Construction.History.frequencies_length line 92
  18. def OAI.Ostmann.Construction.History.GiantUnits line 100
  19. def OAI.Ostmann.Construction.History.Supported line 104
  20. def OAI.Ostmann.Construction.History.weight line 124
  21. def OAI.Ostmann.Construction.History.supportedWeight line 130
  22. theorem OAI.Ostmann.Construction.History.supportedWeight_of_not_supported line 135
  23. theorem OAI.Ostmann.Construction.History.supported_template line 140
  24. theorem OAI.Ostmann.Construction.History.supported_root_frequency_ne_zero line 145
  25. theorem OAI.Ostmann.Construction.History.supported_root_coprime line 150
  26. theorem OAI.Ostmann.Construction.History.supported_root_frequency_bound line 155
  27. theorem OAI.Ostmann.Construction.History.supported_root_positive line 160
  28. theorem OAI.Ostmann.Construction.History.supported_left line 165
  29. theorem OAI.Ostmann.Construction.History.supported_right line 173
  30. theorem OAI.Ostmann.Construction.History.supported_pivot_pos line 181
  31. theorem OAI.Ostmann.Construction.History.supported_compensation_roles line 188
  32. theorem OAI.Ostmann.Construction.History.supported_compensation_product_pos line 196
  33. theorem OAI.Ostmann.Construction.History.supported_small_split line 210
  34. theorem OAI.Ostmann.Construction.History.supported_child_giants line 218
  35. theorem OAI.Ostmann.Construction.History.supported_child_small line 227
  36. theorem OAI.Ostmann.Construction.History.supported_small_product_split line 235
  37. theorem OAI.Ostmann.Construction.History.supported_child_small_products line 245
  38. theorem OAI.Ostmann.Construction.History.supported_reversal line 257