OAI/InformationTheory/PhotonNumber/Inequality.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HilbertBasis.tendsto_isometries line 15
  2. theorem OAI.EntropyPhotonNumber.continuous_oneModeBeamCoefficient line 42
  3. theorem OAI.EntropyPhotonNumber.continuous_beamCoefficient line 54
  4. theorem OAI.EntropyPhotonNumber.tendsto_beamUnitary line 58
  5. theorem OAI.EntropyPhotonNumber.tendsto_beamOutput_parameter line 70
  6. theorem OAI.EntropyPhotonNumber.g_zero line 90
  7. theorem OAI.EntropyPhotonNumber.continuous_g line 92
  8. theorem OAI.EntropyPhotonNumber.hasDerivAt_g line 101
  9. theorem OAI.EntropyPhotonNumber.strictMonoOn_g line 112
  10. theorem OAI.EntropyPhotonNumber.g_nonneg line 120
  11. theorem OAI.EntropyPhotonNumber.g_pos line 123
  12. theorem OAI.EntropyPhotonNumber.gInv_g line 126
  13. theorem OAI.EntropyPhotonNumber.gInv_zero line 136
  14. theorem OAI.EntropyPhotonNumber.h_antitone line 138
  15. theorem OAI.EntropyPhotonNumber.g_ge_log line 146
  16. theorem OAI.EntropyPhotonNumber.g_surjective_nonneg line 151
  17. theorem OAI.EntropyPhotonNumber.gInv_nonneg line 161
  18. theorem OAI.EntropyPhotonNumber.g_gInv line 165
  19. theorem OAI.EntropyPhotonNumber.le_gInv_iff line 169
  20. structure OAI.EntropyPhotonNumber.ThermalInterior line 183
  21. def OAI.EntropyPhotonNumber.ThermalInterior.a line 197
  22. def OAI.EntropyPhotonNumber.ThermalInterior.b line 198
  23. def OAI.EntropyPhotonNumber.ThermalInterior.r0 line 199
  24. theorem OAI.EntropyPhotonNumber.ThermalInterior.a_pos line 200
  25. theorem OAI.EntropyPhotonNumber.ThermalInterior.b_pos line 202
  26. theorem OAI.EntropyPhotonNumber.ThermalInterior.r0_pos line 203
  27. def OAI.EntropyPhotonNumber.ThermalInterior.cap line 204
  28. theorem OAI.EntropyPhotonNumber.ThermalInterior.cap_pos line 205
  29. def OAI.EntropyPhotonNumber.ThermalInterior.eps line 208
  30. theorem OAI.EntropyPhotonNumber.ThermalInterior.eps_pos line 209
  31. theorem OAI.EntropyPhotonNumber.ThermalInterior.eps_limit line 210
  32. def OAI.EntropyPhotonNumber.ThermalInterior.kap line 215
  33. theorem OAI.EntropyPhotonNumber.ThermalInterior.kap_pos line 217
  34. theorem OAI.EntropyPhotonNumber.ThermalInterior.kap_lt_one line 222
  35. theorem OAI.EntropyPhotonNumber.ThermalInterior.kap_limit line 225
  36. def OAI.EntropyPhotonNumber.ThermalInterior.setup line 233
  37. def OAI.EntropyPhotonNumber.ThermalInterior.raw line 264
  38. theorem OAI.EntropyPhotonNumber.ThermalInterior.out_limit line 268
  39. theorem OAI.EntropyPhotonNumber.ThermalInterior.out_entropy_limit line 279
  40. theorem OAI.EntropyPhotonNumber.ThermalInterior.entropy_tangent line 301
  41. theorem OAI.EntropyPhotonNumber.oneModeBeamCoefficient_one line 326
  42. theorem OAI.EntropyPhotonNumber.beamCoefficient_one line 339
  43. theorem OAI.EntropyPhotonNumber.beamUnitary_one line 353
  44. theorem OAI.EntropyPhotonNumber.beamOutput_one line 368
  45. theorem OAI.EntropyPhotonNumber.continuousAt_h_pos line 397
  46. theorem OAI.EntropyPhotonNumber.tendsto_entropy_beamOutput_parameter line 404
  47. def OAI.EntropyPhotonNumber.interiorTransmission line 416
  48. theorem OAI.EntropyPhotonNumber.interiorTransmission_mem line 417
  49. theorem OAI.EntropyPhotonNumber.interiorTransmission_limit line 421
  50. theorem OAI.EntropyPhotonNumber.entropy_tangent_beam line 431
  51. def OAI.EntropyPhotonNumber.NumberCutoff.mass line 466
  52. def OAI.EntropyPhotonNumber.NumberCutoff.projection line 467
  53. def OAI.EntropyPhotonNumber.NumberCutoff.compressed line 468
  54. def OAI.EntropyPhotonNumber.NumberCutoff.vacuum line 469
  55. theorem OAI.EntropyPhotonNumber.NumberCutoff.mass_le_one line 471
  56. theorem OAI.EntropyPhotonNumber.NumberCutoff.compressed_positive line 475
  57. theorem OAI.EntropyPhotonNumber.NumberCutoff.compressed_diagonal line 479
  58. theorem OAI.EntropyPhotonNumber.NumberCutoff.vacuum_diagonal line 489
  59. def OAI.EntropyPhotonNumber.NumberCutoff.state line 495
  60. theorem OAI.EntropyPhotonNumber.NumberCutoff.diagonal line 516
  61. theorem OAI.EntropyPhotonNumber.NumberCutoff.finiteMoment line 526
  62. theorem OAI.EntropyPhotonNumber.NumberCutoff.energy_le line 535
  63. theorem OAI.EntropyPhotonNumber.NumberCutoff.limit line 555
  64. theorem OAI.EntropyPhotonNumber.entropy_tangent_finiteEnergy line 572
  65. def OAI.EntropyPhotonNumber.positiveReference line 598
  66. theorem OAI.EntropyPhotonNumber.positiveReference_pos line 599
  67. theorem OAI.EntropyPhotonNumber.positiveReference_le line 602
  68. theorem OAI.EntropyPhotonNumber.positiveReference_limit line 607
  69. theorem OAI.EntropyPhotonNumber.reference_error_limit line 613
  70. theorem OAI.EntropyPhotonNumber.epni_entropy_interior line 627
  71. theorem OAI.EntropyPhotonNumber.epni_entropy_closed line 666
  72. theorem OAI.EntropyPhotonNumber.entropy_photon_number_inequality line 689

    Distinct definitions of this name: ComparatorChallenges/EntropyPhotonNumber.lean:99 (same statement text; different proof or body). Qualify references as OAI.EntropyPhotonNumber.entropy_photon_number_inequality@path.