OAI/Probability/SKGap/Entropy/EntropyTransport.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGap.entropy_fenchel line 13
  2. theorem OAI.SKGap.entropy_variational line 22
  3. theorem OAI.SKGap.entropy_variational_normalized line 38
  4. def OAI.SKGap.entropyTransport line 47
  5. def OAI.SKGap.entropyTransportDeriv line 49
  6. theorem OAI.SKGap.entropyTransport_hasDerivAt line 51
  7. theorem OAI.SKGap.entropyTransportDeriv_pos line 55
  8. theorem OAI.SKGap.entropyTransport_strictMono line 64
  9. theorem OAI.SKGap.entropyTransport_continuous line 68
  10. theorem OAI.SKGap.entropyTransport_sub_abs_le line 71
  11. theorem OAI.SKGap.entropyTransport_surjective line 77
  12. theorem OAI.SKGap.log_entropyTransportDeriv_lower line 90
  13. theorem OAI.SKGap.entropyTransportDeriv_bounds line 103
  14. theorem OAI.SKGap.integrable_log_entropyTransportDeriv line 115
  15. def OAI.SKGap.entropyTransportLog line 135
  16. theorem OAI.SKGap.integrable_sub_mul_tanh line 139
  17. theorem OAI.SKGap.integrable_entropyTransportLog line 145
  18. theorem OAI.SKGap.gaussianPDF_mul_exp_transport line 152
  19. theorem OAI.SKGap.integrable_exp_entropyTransportLog line 172
  20. theorem OAI.SKGap.integral_exp_entropyTransportLog line 184
  21. theorem OAI.SKGap.entropy_transport_lower line 197
  22. theorem OAI.SKGap.log_gaussianPDFReal line 220
  23. def OAI.SKGap.gaussianRatioLog line 229
  24. theorem OAI.SKGap.gaussianRatioLog_formula line 232
  25. theorem OAI.SKGap.gaussianPDF_mul_exp_ratio line 242
  26. theorem OAI.SKGap.integrable_gaussianRatioLog line 248
  27. theorem OAI.SKGap.integrable_exp_gaussianRatioLog line 255
  28. theorem OAI.SKGap.integral_exp_gaussianRatioLog line 261
  29. theorem OAI.SKGap.entropy_variance_comparison line 268
  30. theorem OAI.SKGap.entropy_variance_lower line 281
  31. theorem OAI.SKGap.secondMoment_integrable line 299
  32. theorem OAI.SKGap.centered_secondMoment_integrable line 303
  33. theorem OAI.SKGap.entropy_q_pos line 310
  34. theorem OAI.SKGap.entropy_q_lt_one line 325
  35. theorem OAI.SKGap.entropy_moment_cauchy line 337