OAI/InformationTheory/AmplitudeDamping/PureRecursion.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.vecMass line 16
  2. theorem OAI.GAD.vecMass_nonneg line 18
  3. theorem OAI.GAD.pure_posSemidef line 21
  4. theorem OAI.GAD.pure_trace line 24
  5. theorem OAI.GAD.pure_state line 27
  6. theorem OAI.GAD.vecMass_eq_zero line 30
  7. def OAI.GAD.unitVec line 42
  8. theorem OAI.GAD.vecMass_unitVec line 44
  9. theorem OAI.GAD.vecMass_smul line 48
  10. def OAI.GAD.normalize line 52
  11. theorem OAI.GAD.sqrt_mass_normalize line 55
  12. theorem OAI.GAD.normalize_mass line 64
  13. theorem OAI.GAD.normSq_normalize line 71
  14. def OAI.GAD.branch line 84
  15. def OAI.GAD.population line 87
  16. theorem OAI.GAD.population_nonneg line 90
  17. theorem OAI.GAD.population_le_mass line 98
  18. theorem OAI.GAD.population_mem line 106
  19. theorem OAI.GAD.vecMass_branches line 110
  20. theorem OAI.GAD.population_zero line 116
  21. theorem OAI.GAD.population_succ line 122
  22. theorem OAI.GAD.population_normalize line 128
  23. def OAI.GAD.basisSplit line 137
  24. theorem OAI.GAD.basisSplit_inl line 146
  25. theorem OAI.GAD.basisSplit_inr line 147
  26. theorem OAI.GAD.channel_pure_apply line 154
  27. theorem OAI.GAD.tensorKraus_mulVec_cons line 159
  28. theorem OAI.GAD.channel_first_site_entry line 168
  29. theorem OAI.GAD.channel_branch_blocks line 197
  30. theorem OAI.GAD.columns_smul line 223
  31. theorem OAI.GAD.columns_normalize line 229
  32. theorem OAI.GAD.gram_columns line 234
  33. theorem OAI.GAD.mass_channel_columns line 237
  34. theorem OAI.GAD.thermal_sqrt_smul line 246
  35. theorem OAI.GAD.channel_state line 256
  36. theorem OAI.GAD.output_entropy_recursion line 261