OAI/InformationTheory/PhotonNumber/PhysicalMinimum.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TensorLp.positive_quadratic_slices line 29
  2. theorem OAI.BeamLadder.weightedConditional_form line 46
  3. theorem OAI.BeamLadder.weightedConditionalRight_form line 72
  4. theorem OAI.EntropyPhotonNumber.weightedConditional_root_form line 105
  5. theorem OAI.EntropyPhotonNumber.weightedConditionalRight_root_form line 116
  6. theorem OAI.EntropyPhotonNumber.GibbsData.logarithmic_weight_nonneg line 130
  7. theorem OAI.EntropyPhotonNumber.GibbsData.quarticLogarithm_positive line 138
  8. theorem OAI.EntropyPhotonNumber.GibbsData.quarticLogarithm_form line 156
  9. def OAI.EntropyPhotonNumber.WeightedColumns.canonical line 166
  10. theorem OAI.EntropyPhotonNumber.weightedRoot_inverse_one line 173
  11. theorem OAI.EntropyPhotonNumber.WeightedColumns.canonical_slice line 185
  12. theorem OAI.EntropyPhotonNumber.WeightedColumns.canonical_sliceRight line 193
  13. theorem OAI.EntropyPhotonNumber.weightedConditional_positive line 202
  14. theorem OAI.EntropyPhotonNumber.weightedConditionalRight_positive line 207
  15. theorem OAI.EntropyPhotonNumber.weightedConditional_twopass_form line 212
  16. theorem OAI.EntropyPhotonNumber.weightedConditionalRight_twopass_form line 230
  17. theorem OAI.EntropyPhotonNumber.spectral_physical_twopass_identification line 248
  18. theorem OAI.EntropyPhotonNumber.spectral_physical_right_twopass_identification line 271
  19. theorem OAI.EntropyPhotonNumber.output_logarithm_representation line 298
  20. theorem OAI.EntropyPhotonNumber.GibbsData.exact_physical_first_logarithmic_identity line 338
  21. theorem OAI.EntropyPhotonNumber.GibbsData.exact_physical_second_logarithmic_identity line 370
  22. theorem OAI.EntropyPhotonNumber.Regularization.minimum_centered_gibbs_data line 408
  23. theorem OAI.EntropyPhotonNumber.Regularization.minimum_physical_log_data line 465
  24. theorem OAI.WeightedGenerator.pairing_add line 532
  25. theorem OAI.WeightedGenerator.pairing_smul line 541
  26. theorem OAI.WeightedGenerator.pairing_scalar_inverse line 549
  27. theorem OAI.EntropyPhotonNumber.GibbsData.exact_physical_first_logarithmic_pairing line 565
  28. theorem OAI.EntropyPhotonNumber.GibbsData.exact_physical_second_logarithmic_pairing line 598
  29. theorem OAI.EntropyPhotonNumber.Regularization.pairing_balance_algebra line 640
  30. theorem OAI.EntropyPhotonNumber.Regularization.minimum_physical_pairing_balance line 648
  31. theorem OAI.EntropyPhotonNumber.Regularization.canonical_output_generator line 710
  32. theorem OAI.EntropyPhotonNumber.thermal_state_entries line 756
  33. theorem OAI.EntropyPhotonNumber.Regularization.minimum_generator_log_balance line 770