OAI/Analysis/IrrationalRotation/Product/ProductScaleConstruction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Invariant233.ProductScaleConstruction.State line 13
  2. structure OAI.Invariant233.ProductScaleConstruction.Step line 20
  3. theorem OAI.Invariant233.ProductScaleConstruction.step_exists line 47
  4. def OAI.Invariant233.ProductScaleConstruction.chooseStep line 75
  5. def OAI.Invariant233.ProductScaleConstruction.nextState line 78
  6. def OAI.Invariant233.ProductScaleConstruction.states line 86
  7. def OAI.Invariant233.ProductScaleConstruction.choices line 89
  8. def OAI.Invariant233.ProductScaleConstruction.constructed line 91
  9. theorem OAI.Invariant233.ProductScaleConstruction.states_succ line 99
  10. theorem OAI.Invariant233.ProductScaleConstruction.count_eq line 101
  11. theorem OAI.Invariant233.ProductScaleConstruction.cost_eq line 109
  12. theorem OAI.Invariant233.ProductScaleConstruction.constructed_laws line 118
  13. theorem OAI.Invariant233.ProductScaleConstruction.exists_product_scales line 162