OAI/InformationTheory/BooleanNoise/PairEntropy.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.pair_mean_mem_Ioo line 17
  2. theorem OAI.LeanBlast.CourtadeKumar.pair_add_mem_Ioo line 21
  3. theorem OAI.LeanBlast.CourtadeKumar.pair_sub_mem_Ioo line 24
  4. theorem OAI.LeanBlast.CourtadeKumar.pair_denom_add_pos line 27
  5. theorem OAI.LeanBlast.CourtadeKumar.pair_denom_sub_pos line 31
  6. theorem OAI.LeanBlast.CourtadeKumar.pair_abs_lt_denom_add line 35
  7. theorem OAI.LeanBlast.CourtadeKumar.pair_abs_lt_denom_sub line 38
  8. theorem OAI.LeanBlast.CourtadeKumar.div_mem_Ioo line 41
  9. theorem OAI.LeanBlast.CourtadeKumar.pair_ratio_add_mem_Ioo line 50
  10. theorem OAI.LeanBlast.CourtadeKumar.pair_ratio_sub_mem_Ioo line 54
  11. theorem OAI.LeanBlast.CourtadeKumar.pair_variance_pos line 58
  12. theorem OAI.LeanBlast.CourtadeKumar.pair_abs_lt_variance line 62
  13. theorem OAI.LeanBlast.CourtadeKumar.pair_weighted_sq line 68
  14. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_eq_psi line 77
  15. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_zero line 82
  16. theorem OAI.LeanBlast.CourtadeKumar.pairDissipation_zero line 85
  17. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_neg_right line 88
  18. theorem OAI.LeanBlast.CourtadeKumar.weighted_psi_div line 94
  19. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_weighted line 108
  20. theorem OAI.LeanBlast.CourtadeKumar.pair_artanh_eq_log_sub line 116
  21. theorem OAI.LeanBlast.CourtadeKumar.artanh_div line 122
  22. theorem OAI.LeanBlast.CourtadeKumar.pairDissipation_weighted line 134
  23. theorem OAI.LeanBlast.CourtadeKumar.pairDissipation_nonneg line 147
  24. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_nonneg line 160
  25. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_div_variance_nonneg line 167
  26. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_lt_ell line 171
  27. theorem OAI.LeanBlast.CourtadeKumar.pair_entropyAverage_pos line 183
  28. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_lt_entropy line 189
  29. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_le_quadratic line 194
  30. theorem OAI.LeanBlast.CourtadeKumar.pairEntropyGap_div_variance_lt_ell line 212
  31. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_pairEntropyGap line 224
  32. theorem OAI.LeanBlast.CourtadeKumar.pairDissipation_eq_mul_deriv line 241
  33. theorem OAI.LeanBlast.CourtadeKumar.pairDissipation_weighted_r line 246
  34. theorem OAI.LeanBlast.CourtadeKumar.r_pairEntropyGap_le_pairDissipation line 253
  35. theorem OAI.LeanBlast.CourtadeKumar.rGap_pairEntropyGap_le line 267
  36. theorem OAI.LeanBlast.CourtadeKumar.K_pairEntropyGap_le line 271