OAI/Dynamics/EntropyCounterexample/SphereCutoffsAffine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SphereCutoffs.affineHeight line 11
  2. def OAI.Problem340.SphereCutoffs.affineClockGate line 13
  3. def OAI.Problem340.SphereCutoffs.affinePreparationCutoff line 16
  4. theorem OAI.Problem340.SphereCutoffs.contDiff_affineHeight line 21
  5. theorem OAI.Problem340.SphereCutoffs.contDiff_affineClockGate line 26
  6. theorem OAI.Problem340.SphereCutoffs.contDiff_affinePreparationCutoff line 31
  7. theorem OAI.Problem340.SphereCutoffs.affineClockGate_mem_Icc line 38
  8. theorem OAI.Problem340.SphereCutoffs.affinePreparationCutoff_mem_Icc line 41
  9. theorem OAI.Problem340.SphereCutoffs.affineClockGate_eq_zero line 47
  10. theorem OAI.Problem340.SphereCutoffs.affineClockGate_eq_one line 55
  11. theorem OAI.Problem340.SphereCutoffs.affinePreparationCutoff_eq_one line 63
  12. theorem OAI.Problem340.SphereCutoffs.affinePreparationCutoff_eq_zero_of_small line 76
  13. theorem OAI.Problem340.SphereCutoffs.affinePreparationCutoff_eq_zero_of_large line 85
  14. theorem OAI.Problem340.SphereCutoffs.clockGate_eq_affineClockGate line 94
  15. theorem OAI.Problem340.SphereCutoffs.preparationCutoff_eq_affinePreparationCutoff line 98
  16. theorem OAI.Problem340.SphereCutoffs.hasCompactSupport_affinePreparationCutoff line 103
  17. theorem OAI.Problem340.SphereCutoffs.continuous_onePointElim_of_eq_const_off_isCompact line 111
  18. def OAI.Problem340.SphereCutoffs.onePointClockGate line 123
  19. def OAI.Problem340.SphereCutoffs.onePointPreparationCutoff line 125
  20. theorem OAI.Problem340.SphereCutoffs.onePointClockGate_coe line 127
  21. theorem OAI.Problem340.SphereCutoffs.onePointClockGate_infty line 130
  22. theorem OAI.Problem340.SphereCutoffs.onePointPreparationCutoff_coe line 132
  23. theorem OAI.Problem340.SphereCutoffs.onePointPreparationCutoff_infty line 135
  24. theorem OAI.Problem340.SphereCutoffs.continuous_onePointClockGate line 139
  25. theorem OAI.Problem340.SphereCutoffs.continuous_onePointPreparationCutoff line 148
  26. theorem OAI.Problem340.SphereCutoffs.onePointClockGate_mem_Icc line 157
  27. theorem OAI.Problem340.SphereCutoffs.onePointPreparationCutoff_mem_Icc line 163