OAI/InformationTheory/PhotonNumber/Interpolation.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyPhotonNumber.boundaryB_f_sq line 27
  2. theorem OAI.EntropyPhotonNumber.boundaryB_eq_B line 52
  3. theorem OAI.EntropyPhotonNumber.exists_B_resolvent line 57
  4. theorem OAI.EntropyPhotonNumber.Herglotz.compactIntegral_re_pos line 89
  5. def OAI.EntropyPhotonNumber.resolventB line 121
  6. def OAI.EntropyPhotonNumber.resolventR line 124
  7. theorem OAI.EntropyPhotonNumber.analyticAt_resolventB line 127
  8. theorem OAI.EntropyPhotonNumber.analyticAt_resolventR line 131
  9. theorem OAI.EntropyPhotonNumber.resolventR_im_nonpos line 144
  10. theorem OAI.EntropyPhotonNumber.resolventR_real line 150
  11. theorem OAI.EntropyPhotonNumber.resolventR_real_pos line 154
  12. theorem OAI.EntropyPhotonNumber.resolventR_stieltjes line 161
  13. theorem OAI.EntropyPhotonNumber.analytic_eqOn_rightHalfPlane_of_real_interval line 173
  14. theorem OAI.EntropyPhotonNumber.deriv_resolventB_on_original line 208
  15. theorem OAI.EntropyPhotonNumber.deriv_resolventB_ode line 219
  16. theorem OAI.EntropyPhotonNumber.hasDerivAt_resolventB_one line 247
  17. theorem OAI.EntropyPhotonNumber.compactIntegral_one line 255
  18. theorem OAI.EntropyPhotonNumber.resolventB_real line 275
  19. theorem OAI.EntropyPhotonNumber.hasDerivAt_real_resolventB line 279
  20. theorem OAI.EntropyPhotonNumber.strictAntiOn_real_resolventB line 289
  21. theorem OAI.EntropyPhotonNumber.exists_analytic_stieltjes_B line 302
  22. theorem OAI.EntropyPhotonNumber.logarithmicMean_exp_pair line 350
  23. theorem OAI.EntropyPhotonNumber.dualLogarithmicMean_exp_pair line 371
  24. theorem OAI.EntropyPhotonNumber.comparison_basic_weights line 379
  25. theorem OAI.EntropyPhotonNumber.B_f_sq_all line 399
  26. def OAI.EntropyPhotonNumber.genericAdditionalE line 404
  27. theorem OAI.EntropyPhotonNumber.genericAdditionalE_pos line 407
  28. theorem OAI.EntropyPhotonNumber.genericAdditionalE_difference line 422
  29. theorem OAI.EntropyPhotonNumber.continuous_genericAdditionalE_f line 462
  30. theorem OAI.EntropyPhotonNumber.scalar_minimum_off line 480
  31. theorem OAI.EntropyPhotonNumber.scalar_minimum line 501
  32. def OAI.EntropyPhotonNumber.interpolationQuadratic line 538
  33. theorem OAI.EntropyPhotonNumber.interpolationQuadratic_expand line 545
  34. theorem OAI.EntropyPhotonNumber.interpolationQuadratic_complete line 560
  35. theorem OAI.EntropyPhotonNumber.interpolationQuadratic_lower line 573
  36. theorem OAI.EntropyPhotonNumber.interpolationQuadratic_minimum line 589
  37. theorem OAI.EntropyPhotonNumber.comparison_interpolation_of_stieltjes line 602
  38. theorem OAI.EntropyPhotonNumber.four_weight_interpolation line 631