OAI/NumberTheory/GaussianMoat/FiniteLaw.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.entropySum line 14
  2. theorem OAI.GaussianMoat.gibbs_point line 17
  3. theorem OAI.GaussianMoat.gibbs_sum line 30
  4. theorem OAI.GaussianMoat.entropySum_subadd line 37
  5. theorem OAI.GaussianMoat.negMulLog_sum_le line 109
  6. structure OAI.GaussianMoat.FinLaw line 123
  7. instance OAI.GaussianMoat.FinLaw.(instance at line 131) line 131
  8. theorem OAI.GaussianMoat.FinLaw.ext line 133
  9. theorem OAI.GaussianMoat.FinLaw.le_one line 136
  10. theorem OAI.GaussianMoat.FinLaw.nonempty line 140
  11. def OAI.GaussianMoat.FinLaw.entropy line 145
  12. theorem OAI.GaussianMoat.FinLaw.entropy_nonneg line 147
  13. theorem OAI.GaussianMoat.FinLaw.entropy_le_log_card line 150
  14. def OAI.GaussianMoat.FinLaw.map line 167
  15. theorem OAI.GaussianMoat.FinLaw.map_mass line 174
  16. theorem OAI.GaussianMoat.FinLaw.map_id line 179
  17. theorem OAI.GaussianMoat.FinLaw.map_comp line 184
  18. def OAI.GaussianMoat.FinLaw.H line 198
  19. def OAI.GaussianMoat.FinLaw.condH line 200
  20. theorem OAI.GaussianMoat.FinLaw.H_eq_sum line 203
  21. theorem OAI.GaussianMoat.FinLaw.H_eq_of_fibers line 220
  22. theorem OAI.GaussianMoat.FinLaw.H_comp_injective line 233
  23. theorem OAI.GaussianMoat.FinLaw.H_pair_comm line 237
  24. theorem OAI.GaussianMoat.FinLaw.H_pair_assoc line 242
  25. theorem OAI.GaussianMoat.FinLaw.H_pair_function line 247
  26. theorem OAI.GaussianMoat.FinLaw.H_map line 254
  27. theorem OAI.GaussianMoat.FinLaw.map_fst_mass line 257
  28. theorem OAI.GaussianMoat.FinLaw.map_snd_mass line 262
  29. theorem OAI.GaussianMoat.FinLaw.entropy_ge_snd line 266
  30. theorem OAI.GaussianMoat.FinLaw.entropy_subadd line 272
  31. theorem OAI.GaussianMoat.FinLaw.H_pair_ge_snd line 279
  32. theorem OAI.GaussianMoat.FinLaw.H_pair_subadd line 284
  33. theorem OAI.GaussianMoat.FinLaw.condH_nonneg line 289
  34. theorem OAI.GaussianMoat.FinLaw.condH_le_H line 292
  35. theorem OAI.GaussianMoat.FinLaw.H_le_condH_add line 297
  36. theorem OAI.GaussianMoat.FinLaw.entropy_strong_subadd line 303
  37. theorem OAI.GaussianMoat.FinLaw.H_strong_subadd line 329
  38. theorem OAI.GaussianMoat.FinLaw.condH_mono line 335
  39. def OAI.GaussianMoat.FinLaw.mutualInfo line 341
  40. def OAI.GaussianMoat.FinLaw.condMutualInfo line 344
  41. theorem OAI.GaussianMoat.FinLaw.mutualInfo_nonneg line 348
  42. theorem OAI.GaussianMoat.FinLaw.condH_pair_comm line 351
  43. theorem OAI.GaussianMoat.FinLaw.condMutualInfo_nonneg line 359
  44. theorem OAI.GaussianMoat.FinLaw.entropySum_scale line 365
  45. theorem OAI.GaussianMoat.FinLaw.entropySum_le_mass_log_card line 371
  46. theorem OAI.GaussianMoat.FinLaw.entropySum_le_mass_log_support line 393
  47. theorem OAI.GaussianMoat.FinLaw.condH_le_support line 407
  48. def OAI.GaussianMoat.FinLaw.mix line 443
  49. theorem OAI.GaussianMoat.FinLaw.mix_mass line 448
  50. theorem OAI.GaussianMoat.FinLaw.entropy_mix_ge line 451
  51. theorem OAI.GaussianMoat.FinLaw.H_const line 461
  52. theorem OAI.GaussianMoat.FinLaw.H_bool line 465
  53. theorem OAI.GaussianMoat.FinLaw.condH_le_reveal line 473
  54. theorem OAI.GaussianMoat.FinLaw.log_card_le_real line 487
  55. theorem OAI.GaussianMoat.FinLaw.short_list line 493
  56. theorem OAI.GaussianMoat.FinLaw.short_list_deficit line 535
  57. theorem OAI.GaussianMoat.FinLaw.low_mass_deficit line 543