OAI/Dynamics/EntropyCounterexample/SphereCutoffs.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SphereCutoffs.clockGateAmbient line 9
  2. def OAI.Problem340.SphereCutoffs.preparationCutoffAmbient line 12
  3. def OAI.Problem340.SphereCutoffs.clockGate line 16
  4. def OAI.Problem340.SphereCutoffs.preparationCutoff line 18
  5. theorem OAI.Problem340.SphereCutoffs.contDiff_clockGateAmbient line 21
  6. theorem OAI.Problem340.SphereCutoffs.contDiff_preparationCutoffAmbient line 28
  7. theorem OAI.Problem340.SphereCutoffs.continuous_clockGate line 38
  8. theorem OAI.Problem340.SphereCutoffs.continuous_preparationCutoff line 42
  9. theorem OAI.Problem340.SphereCutoffs.clockGateAmbient_nonneg line 45
  10. theorem OAI.Problem340.SphereCutoffs.clockGateAmbient_le_one line 48
  11. theorem OAI.Problem340.SphereCutoffs.preparationCutoffAmbient_nonneg line 51
  12. theorem OAI.Problem340.SphereCutoffs.preparationCutoffAmbient_le_one line 55
  13. theorem OAI.Problem340.SphereCutoffs.clockGateAmbient_eq_zero line 60
  14. theorem OAI.Problem340.SphereCutoffs.clockGateAmbient_eq_one line 65
  15. theorem OAI.Problem340.SphereCutoffs.preparationCutoffAmbient_eq_one line 70
  16. theorem OAI.Problem340.SphereCutoffs.preparationCutoffAmbient_eq_zero_of_low line 77
  17. theorem OAI.Problem340.SphereCutoffs.preparationCutoffAmbient_eq_zero_of_high line 82
  18. theorem OAI.Problem340.SphereCutoffs.support_preparationCutoffAmbient line 87
  19. theorem OAI.Problem340.SphereCutoffs.clockGate_mem_Icc line 97
  20. theorem OAI.Problem340.SphereCutoffs.preparationCutoff_mem_Icc line 100
  21. theorem OAI.Problem340.SphereCutoffs.clockGate_eq_zero_of_radius line 104
  22. theorem OAI.Problem340.SphereCutoffs.clockGate_eq_one_of_radius line 112
  23. theorem OAI.Problem340.SphereCutoffs.preparationCutoff_eq_one_of_radius line 120
  24. theorem OAI.Problem340.SphereCutoffs.preparationCutoff_eq_zero_of_small_radius line 132
  25. theorem OAI.Problem340.SphereCutoffs.preparationCutoff_eq_zero_of_large_radius line 141