OAI/InformationTheory/PhotonNumber/GibbsVariational.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuantumTrace.negMulLog_lt_crossEntropy line 23
  2. structure OAI.QuantumTrace.StochasticOverlap line 41
  3. theorem OAI.QuantumTrace.StochasticOverlap.hasSum_row_product line 50
  4. def OAI.QuantumTrace.StochasticOverlap.transpose line 66
  5. theorem OAI.QuantumTrace.StochasticOverlap.hasSum_col_product line 72
  6. theorem OAI.QuantumTrace.StochasticOverlap.hasSum_prod_nonneg line 76
  7. def OAI.QuantumTrace.StochasticOverlap.diagonal line 85
  8. theorem OAI.QuantumTrace.StochasticOverlap.hasSum_crossEntropy line 87
  9. theorem OAI.QuantumTrace.StochasticOverlap.klein line 104
  10. def OAI.QuantumTrace.basisOverlap line 139
  11. theorem OAI.QuantumTrace.basisOverlap_diagonal line 149
  12. theorem OAI.QuantumTrace.quantum_klein line 155
  13. theorem OAI.QuantumTrace.hasSum_entropy_eigenvalues line 197
  14. theorem OAI.QuantumTrace.spectral_gibbs_variational line 210
  15. theorem OAI.QuantumTrace.spectral_gibbs_attains line 239
  16. def OAI.EntropyPhotonNumber.crossEntropy line 297
  17. theorem OAI.EntropyPhotonNumber.entropy_hasSum line 301
  18. theorem OAI.EntropyPhotonNumber.entropy_le_crossEntropy line 309
  19. theorem OAI.EntropyPhotonNumber.crossEntropy_self line 326
  20. theorem OAI.EntropyPhotonNumber.crossEntropy_finite line 339
  21. theorem OAI.QuantumTrace.spectralGibbs_seventh_moment line 365
  22. theorem OAI.EntropyPhotonNumber.exists_gibbs_state line 406
  23. theorem OAI.EntropyPhotonNumber.gibbs_slice_real_trace line 443
  24. def OAI.EntropyPhotonNumber.sliceFreeEnergy line 477
  25. theorem OAI.EntropyPhotonNumber.sliced_gibbs_minimizer line 482
  26. theorem OAI.EntropyPhotonNumber.crossEntropy_mixture line 541
  27. theorem OAI.EntropyPhotonNumber.one_port_majorant line 556
  28. structure OAI.EntropyPhotonNumber.KrausFlow line 617
  29. theorem OAI.EntropyPhotonNumber.composedKraus_second_ensemble line 631
  30. def OAI.EntropyPhotonNumber.Regularization.rawOutput line 647
  31. def OAI.EntropyPhotonNumber.Regularization.firstFlow line 651
  32. def OAI.EntropyPhotonNumber.Regularization.secondFlow line 672
  33. theorem OAI.EntropyPhotonNumber.flow_minimum_gibbs line 698
  34. theorem OAI.EntropyPhotonNumber.Regularization.minimum_gibbs line 746
  35. theorem OAI.EntropyPhotonNumber.GibbsData.crossEntropy_hamiltonian line 793
  36. def OAI.EntropyPhotonNumber.relativeEntropy line 823
  37. theorem OAI.EntropyPhotonNumber.flow_relative_entropy_identity line 826
  38. theorem OAI.TensorLp.tensor_mul_moment line 868
  39. theorem OAI.TensorLp.ensemble_tensor_mul_moment line 876
  40. def OAI.EntropyPhotonNumber.powerMoment line 890
  41. theorem OAI.EntropyPhotonNumber.powerMoment_eq line 893
  42. theorem OAI.EntropyPhotonNumber.finiteMoment_iff line 904
  43. theorem OAI.EntropyPhotonNumber.beamOutput_powerMoment_le line 917
  44. theorem OAI.EntropyPhotonNumber.beamOutput_finiteMoment line 964