OAI/InformationTheory/PhotonNumber/Generator.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PhysicalGenerator.lowerCoefficient line 23
  2. def OAI.PhysicalGenerator.raiseCoefficient line 24
  3. def OAI.PhysicalGenerator.modeCoefficient line 26
  4. def OAI.PhysicalGenerator.lowerFamily line 29
  5. def OAI.PhysicalGenerator.raiseFamily line 30
  6. def OAI.PhysicalGenerator.modeFamily line 31
  7. def OAI.PhysicalGenerator.baseFamily line 32
  8. def OAI.PhysicalGenerator.dissipator line 34
  9. def OAI.PhysicalGenerator.generator line 39
  10. theorem OAI.PhysicalGenerator.pairing_hasSum line 42
  11. theorem OAI.PhysicalGenerator.dissipator_entry line 65
  12. theorem OAI.PhysicalGenerator.lowerCoefficient_self line 117
  13. theorem OAI.PhysicalGenerator.raiseCoefficient_self line 124
  14. theorem OAI.PhysicalGenerator.modeCoefficient_conj line 131
  15. theorem OAI.PhysicalGenerator.generator_zero_of_geometric_diagonal line 135
  16. theorem OAI.PhysicalGenerator.weighted_pairing_zero_of_geometric_diagonal line 176
  17. theorem OAI.QuantumTrace.thermalWeight_number line 199
  18. theorem OAI.QuantumTrace.thermalWeight_up line 203
  19. theorem OAI.QuantumTrace.thermalWeight_balance line 210
  20. theorem OAI.PhysicalGenerator.weighted_thermal_pairing_zero line 226
  21. theorem OAI.PhysicalGenerator.dissipator_affine line 239
  22. theorem OAI.PhysicalGenerator.generator_affine line 261
  23. theorem OAI.PhysicalGenerator.pairing_affine line 274
  24. theorem OAI.PhysicalGenerator.weighted_pairing_affine line 287
  25. structure OAI.EntropyPhotonNumber.WeightedColumns line 311
  26. theorem OAI.EntropyPhotonNumber.WeightedColumns.base_density line 321
  27. def OAI.EntropyPhotonNumber.WeightedColumns.slice line 325
  28. def OAI.EntropyPhotonNumber.WeightedColumns.sliceRight line 328
  29. theorem OAI.EntropyPhotonNumber.WeightedColumns.thermal_pairing_zero line 331
  30. theorem OAI.EntropyPhotonNumber.weighted_replaced_threeport_generator line 339
  31. def OAI.PhysicalGenerator.weakOperator line 377
  32. theorem OAI.PhysicalGenerator.weak_pairing_hasSum line 381
  33. theorem OAI.PhysicalGenerator.weakOperator_entry line 394
  34. theorem OAI.PhysicalGenerator.weakOperator_affine line 420
  35. theorem OAI.PhysicalGenerator.weak_pairing_affine line 437
  36. theorem OAI.PhysicalGenerator.weakOperator_zero_of_geometric_diagonal line 451
  37. theorem OAI.PhysicalGenerator.weak_thermal_pairing_zero line 477
  38. def OAI.EntropyPhotonNumber.WeightedColumns.rawSlice line 496
  39. def OAI.EntropyPhotonNumber.WeightedColumns.rawSliceRight line 499
  40. theorem OAI.EntropyPhotonNumber.WeightedColumns.thermal_weak_zero line 502
  41. theorem OAI.EntropyPhotonNumber.replaced_threeport_weak line 510
  42. theorem OAI.KrausBounded.dual_one line 549
  43. theorem OAI.BeamLadder.conjugate_one line 567
  44. def OAI.EntropyPhotonNumber.WeightedColumns.expectation line 581
  45. def OAI.EntropyPhotonNumber.WeightedColumns.weakMean line 585
  46. def OAI.EntropyPhotonNumber.WeightedColumns.centeredWeak line 587
  47. theorem OAI.EntropyPhotonNumber.WeightedColumns.expectation_one line 590
  48. theorem OAI.EntropyPhotonNumber.WeightedColumns.centeredWeak_one line 601
  49. theorem OAI.EntropyPhotonNumber.WeightedColumns.rawSlice_one line 604
  50. theorem OAI.EntropyPhotonNumber.WeightedColumns.rawSliceRight_one line 607
  51. theorem OAI.EntropyPhotonNumber.WeightedColumns.expectation_affine line 610
  52. theorem OAI.EntropyPhotonNumber.physical_rawSlice_expectation line 631
  53. theorem OAI.EntropyPhotonNumber.replaced_threeport_centered_weak line 671
  54. theorem OAI.BeamLadder.single_ladder_inner line 722
  55. theorem OAI.EntropyPhotonNumber.WeightedColumns.weakMean_trace line 748
  56. theorem OAI.EntropyPhotonNumber.WeightedColumns.weakMean_reference line 764
  57. def OAI.EntropyPhotonNumber.MainObligation line 768