OAI/Dynamics/EntropyCounterexample/MapSignal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.Construction.scheduledSignal line 13
  2. theorem OAI.Problem340.Construction.baseInput_eq_delayed_signal line 18
  3. theorem OAI.Problem340.Construction.input_eq_baseInput_of_mem_Ico line 32
  4. theorem OAI.Problem340.Construction.input_eq_delayed_signal line 37
  5. theorem OAI.Problem340.Construction.norm_scheduledSignal_le line 48
  6. theorem OAI.Problem340.Construction.baseInput_eq_zero_of_not_mem_preparation line 68
  7. theorem OAI.Problem340.Construction.input_eq_zero_of_not_mem_preparation line 77
  8. theorem OAI.Problem340.Construction.norm_phase_coe_eq_one line 84
  9. theorem OAI.Problem340.Construction.predictedClock_succ_eq_increment line 88
  10. theorem OAI.Problem340.Construction.predictedClock_monotone_of_gate_nonneg line 95
  11. theorem OAI.Problem340.Construction.barrier_eq_one_of_readoutCoeff_ne_zero line 103
  12. theorem OAI.Problem340.Construction.predictedClock_unit_step_at_readout line 112
  13. theorem OAI.Problem340.Construction.predicted_readout_single_hit line 119
  14. theorem OAI.Problem340.Construction.input_eq_delayed_signal_of_predicted_hit line 138
  15. theorem OAI.Problem340.Construction.scheduledSignal_eq_readout_smul line 151
  16. theorem OAI.Problem340.Construction.sum_scheduledSignal_eq_readout_smul line 162