OAI/Analysis/IrrationalRotation/Rotation/CircleParameterRecursion.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Invariant233.CircleParameterRecursion.State line 18
  2. structure OAI.Invariant233.CircleParameterRecursion.Step line 33
  3. theorem OAI.Invariant233.CircleParameterRecursion.step_exists line 64
  4. def OAI.Invariant233.CircleParameterRecursion.chooseStep line 94
  5. def OAI.Invariant233.CircleParameterRecursion.nextState line 98
  6. def OAI.Invariant233.CircleParameterRecursion.initial line 120
  7. def OAI.Invariant233.CircleParameterRecursion.states line 135
  8. def OAI.Invariant233.CircleParameterRecursion.choices line 138
  9. theorem OAI.Invariant233.CircleParameterRecursion.states_d_succ line 141
  10. theorem OAI.Invariant233.CircleParameterRecursion.states_d_ge line 145
  11. theorem OAI.Invariant233.CircleParameterRecursion.states_d_mono line 154
  12. theorem OAI.Invariant233.CircleParameterRecursion.states_keep line 161
  13. theorem OAI.Invariant233.CircleParameterRecursion.exists_global_frequency line 166
  14. def OAI.Invariant233.CircleParameterRecursion.globalFrequency line 177
  15. theorem OAI.Invariant233.CircleParameterRecursion.global_agree line 180
  16. theorem OAI.Invariant233.CircleParameterRecursion.global_block line 185
  17. def OAI.Invariant233.CircleParameterRecursion.constructed line 192
  18. theorem OAI.Invariant233.CircleParameterRecursion.blockEnd_eq line 206
  19. theorem OAI.Invariant233.CircleParameterRecursion.cost_eq line 215
  20. theorem OAI.Invariant233.CircleParameterRecursion.block_mem line 225
  21. theorem OAI.Invariant233.CircleParameterRecursion.coefficientBound_eq line 232
  22. theorem OAI.Invariant233.CircleParameterRecursion.sample_index_bound line 240
  23. theorem OAI.Invariant233.CircleParameterRecursion.samples_eq line 248
  24. theorem OAI.Invariant233.CircleParameterRecursion.alpha_block line 255
  25. theorem OAI.Invariant233.CircleParameterRecursion.constructed_phases line 264
  26. theorem OAI.Invariant233.CircleParameterRecursion.convolution_eq_supported line 276
  27. theorem OAI.Invariant233.CircleParameterRecursion.constructed_ratios line 297
  28. theorem OAI.Invariant233.CircleParameterRecursion.constructed_spread line 329
  29. theorem OAI.Invariant233.CircleParameterRecursion.prod_constructed_block line 375
  30. theorem OAI.Invariant233.CircleParameterRecursion.samplingAverage_eq line 398
  31. theorem OAI.Invariant233.CircleParameterRecursion.shift_eq line 425
  32. theorem OAI.Invariant233.CircleParameterRecursion.ell_eq line 434
  33. theorem OAI.Invariant233.CircleParameterRecursion.constructed_laws line 445
  34. theorem OAI.Invariant233.CircleParameterRecursion.exists_parameters_of_stage_supply line 608