OAI/InformationTheory/PhotonNumber/ThermalLimit.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThermalMetric.column_metric_bound line 19
  2. theorem OAI.ThermalMetric.bounded_matrix_bound line 45
  3. theorem OAI.EntropyPhotonNumber.GibbsData.full_defect_on_observable line 93
  4. theorem OAI.EntropyPhotonNumber.GibbsData.observableVector_bound line 106
  5. theorem OAI.EntropyPhotonNumber.GibbsData.weakDefect_bound line 111
  6. def OAI.ThermalRecurrence.lower line 136
  7. theorem OAI.ThermalRecurrence.lower_same line 139
  8. theorem OAI.ThermalRecurrence.lower_sum line 141
  9. def OAI.ThermalRecurrence.Balance line 153
  10. theorem OAI.ThermalRecurrence.entry_zero_of_lt line 160
  11. theorem OAI.ThermalRecurrence.off_diagonal_zero line 183
  12. theorem OAI.ThermalRecurrence.diagonal_step line 195
  13. theorem OAI.ThermalRecurrence.diagonal_formula line 210
  14. theorem OAI.ThermalRecurrence.thermalWeight_eq line 235
  15. theorem OAI.ThermalRecurrence.unique_thermal_matrix line 239
  16. theorem OAI.EntropyPhotonNumber.entry_tendsto line 286
  17. theorem OAI.EntropyPhotonNumber.state_entry_star line 292
  18. theorem OAI.EntropyPhotonNumber.weakDefect_tendsto line 300
  19. theorem OAI.EntropyPhotonNumber.thermal_limit_entries line 317
  20. theorem OAI.EntropyPhotonNumber.thermalState_energy line 359
  21. theorem OAI.EntropyPhotonNumber.thermalState_entropy line 366
  22. theorem OAI.EntropyPhotonNumber.thermal_beamOutput line 388
  23. theorem OAI.EntropyPhotonNumber.ThermalSetup.output_thermal line 431
  24. theorem OAI.EntropyPhotonNumber.op_mem_energySet line 454
  25. theorem OAI.EntropyPhotonNumber.pair_energy_subsequence line 460
  26. theorem OAI.EntropyPhotonNumber.thermal_limit_state line 481
  27. theorem OAI.EntropyPhotonNumber.component_tendsto_zero line 494
  28. theorem OAI.EntropyPhotonNumber.weighted_pair_components line 508
  29. theorem OAI.EntropyPhotonNumber.four_components_tendsto_zero line 522
  30. theorem OAI.EntropyPhotonNumber.pair_thermal_subsequence line 542
  31. theorem OAI.EntropyPhotonNumber.ThermalSetup.minimum_thermal_subsequence line 565
  32. def OAI.EntropyPhotonNumber.thermalRelative line 598
  33. theorem OAI.EntropyPhotonNumber.thermalRelative_nonneg line 601
  34. def OAI.EntropyPhotonNumber.ThermalSetup.out line 615
  35. def OAI.EntropyPhotonNumber.ThermalSetup.entropyPart line 617
  36. def OAI.EntropyPhotonNumber.ThermalSetup.penalty line 621
  37. def OAI.EntropyPhotonNumber.ThermalSetup.offset line 624
  38. theorem OAI.EntropyPhotonNumber.ThermalSetup.objective_offset line 628
  39. theorem OAI.EntropyPhotonNumber.ThermalSetup.penalty_nonneg line 638
  40. theorem OAI.EntropyPhotonNumber.ThermalSetup.entropyPart_tendsto line 644
  41. theorem OAI.EntropyPhotonNumber.ThermalSetup.base_nonnegative line 678