OAI/InformationTheory/BooleanNoise/NormalizedPair.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.hasSum_weighted_nonneg_of_single_crossing line 17
  2. theorem OAI.LeanBlast.CourtadeKumar.logconvex_single_crossing line 49
  3. theorem OAI.LeanBlast.CourtadeKumar.logconvex_mul_pow line 81
  4. theorem OAI.LeanBlast.CourtadeKumar.logconvex_geometric_single_crossing line 94
  5. theorem OAI.LeanBlast.CourtadeKumar.weighted_hasSum_le_of_logconvex line 133
  6. def OAI.LeanBlast.CourtadeKumar.rawPairMoment line 164
  7. def OAI.LeanBlast.CourtadeKumar.normalizedPairMoment line 168
  8. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_zero line 172
  9. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_succ line 176
  10. theorem OAI.LeanBlast.CourtadeKumar.normalized_pair_scale_pos line 180
  11. theorem OAI.LeanBlast.CourtadeKumar.abs_lt_normalized_pair_scale line 184
  12. theorem OAI.LeanBlast.CourtadeKumar.two_atom_moment_logconvex line 190
  13. theorem OAI.LeanBlast.CourtadeKumar.rawPairMoment_logconvex line 203
  14. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_nonneg line 213
  15. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_one line 228
  16. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_two line 237
  17. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_logconvex line 246
  18. theorem OAI.LeanBlast.CourtadeKumar.normalizedPairMoment_one_lt_one line 267
  19. theorem OAI.LeanBlast.CourtadeKumar.hasSum_normalizedPairEntropy line 276
  20. theorem OAI.LeanBlast.CourtadeKumar.hasSum_normalizedPairDissipation line 290
  21. theorem OAI.LeanBlast.CourtadeKumar.normalized_pair_dissipation_ge_of_psi line 305
  22. theorem OAI.LeanBlast.CourtadeKumar.normalized_pair_dissipation_ge_r line 324
  23. theorem OAI.LeanBlast.CourtadeKumar.normalized_pair_bound_of_antitone line 332
  24. theorem OAI.LeanBlast.CourtadeKumar.normalized_pair_bound line 369