OAI/NumberTheory/GaussianMoat/FiniteEntropy.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.FinLaw.Hf line 15
  2. def OAI.GaussianMoat.FinLaw.cHf line 19
  3. theorem OAI.GaussianMoat.FinLaw.Hf_eq_H line 22
  4. theorem OAI.GaussianMoat.FinLaw.Hf_eq_of_fibers line 27
  5. def OAI.GaussianMoat.FinLaw.outputRange line 39
  6. def OAI.GaussianMoat.FinLaw.outputCode line 43
  7. theorem OAI.GaussianMoat.FinLaw.outputCode_eq_iff line 48
  8. theorem OAI.GaussianMoat.FinLaw.Hf_code line 51
  9. theorem OAI.GaussianMoat.FinLaw.Hf_pair_code line 56
  10. theorem OAI.GaussianMoat.FinLaw.Hf_triple_code line 62
  11. theorem OAI.GaussianMoat.FinLaw.Hf_nonneg line 70
  12. theorem OAI.GaussianMoat.FinLaw.Hf_le_log_card_sample line 74
  13. theorem OAI.GaussianMoat.FinLaw.Hf_pair_comm line 85
  14. theorem OAI.GaussianMoat.FinLaw.Hf_pair_assoc line 90
  15. theorem OAI.GaussianMoat.FinLaw.Hf_pair_ge_snd line 95
  16. theorem OAI.GaussianMoat.FinLaw.Hf_pair_subadd line 100
  17. theorem OAI.GaussianMoat.FinLaw.Hf_strong_subadd line 105
  18. theorem OAI.GaussianMoat.FinLaw.cHf_nonneg line 111
  19. theorem OAI.GaussianMoat.FinLaw.cHf_le_Hf line 114
  20. theorem OAI.GaussianMoat.FinLaw.cHf_mono line 117
  21. theorem OAI.GaussianMoat.FinLaw.Hf_comp_le line 123
  22. theorem OAI.GaussianMoat.FinLaw.Hf_le_of_determined line 132
  23. theorem OAI.GaussianMoat.FinLaw.Hf_const line 141
  24. theorem OAI.GaussianMoat.FinLaw.Hf_finset_subadd line 145
  25. def OAI.GaussianMoat.FinLaw.prefixVar line 181
  26. def OAI.GaussianMoat.FinLaw.orderedEntropy line 184
  27. theorem OAI.GaussianMoat.FinLaw.prefixVar_zero line 188
  28. theorem OAI.GaussianMoat.FinLaw.orderedEntropy_zero line 191
  29. theorem OAI.GaussianMoat.FinLaw.orderedEntropy_nonneg line 198
  30. theorem OAI.GaussianMoat.FinLaw.prefixVar_chain line 201
  31. theorem OAI.GaussianMoat.FinLaw.orderedEntropy_step line 228
  32. theorem OAI.GaussianMoat.FinLaw.ordered_remaining_exchange line 233
  33. theorem OAI.GaussianMoat.FinLaw.cHf_mono_of_refines line 252
  34. theorem OAI.GaussianMoat.FinLaw.orderedEntropy_concave line 269
  35. theorem OAI.GaussianMoat.FinLaw.orderedEntropy_slope line 283
  36. def OAI.GaussianMoat.FinLaw.signedEntropy line 299
  37. theorem OAI.GaussianMoat.FinLaw.signedEntropy_zero line 302
  38. theorem OAI.GaussianMoat.FinLaw.signedEntropy_slope line 305
  39. theorem OAI.GaussianMoat.FinLaw.cHf_chain line 312
  40. theorem OAI.GaussianMoat.FinLaw.cHf_pair_subadd line 322
  41. theorem OAI.GaussianMoat.FinLaw.enrichment_chain line 330