OAI/Dynamics/EntropyCounterexample/PhaseAlignment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.aligned_square_norm line 9
  2. theorem OAI.Problem340.aligned_square_ne_zero line 20
  3. theorem OAI.Problem340.aligned_square_phase line 28
  4. theorem OAI.Problem340.pow_two_pow_le_of_square_le line 39
  5. theorem OAI.Problem340.prediction_phase_power line 52
  6. theorem OAI.Problem340.tendsto_atTop_of_square_le line 58
  7. theorem OAI.Problem340.aligned_orbit_phase_until line 66
  8. theorem OAI.Problem340.aligned_orbit_phase line 97
  9. theorem OAI.Problem340.aligned_orbit_norm line 107
  10. theorem OAI.Problem340.aligned_readout_sum line 121
  11. theorem OAI.Problem340.readout_gain_ge_two line 145
  12. theorem OAI.Problem340.tendsto_atTop_of_eventually_square_le line 160
  13. theorem OAI.Problem340.aligned_orbit_escape line 173