OAI/NumberTheory/GaussianMoat/FreshEntropy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GaussianMoat.expect_restrict line 10
  2. theorem OAI.GaussianMoat.expect_precomp_injective line 22
  3. lemma OAI.GaussianMoat.signMeasure_real_eq_expect line 38
  4. lemma OAI.GaussianMoat.expect_sign_restriction line 43
  5. lemma OAI.GaussianMoat.uniform_entropy_event_bound line 50
  6. abbrev OAI.GaussianMoat.SplitSieve.restrict line 64
  7. def OAI.GaussianMoat.SplitSieve.enumeration line 72
  8. def OAI.GaussianMoat.prefixIndices line 75
  9. lemma OAI.GaussianMoat.mem_prefixIndices line 78
  10. lemma OAI.GaussianMoat.prefixIndices_card line 81
  11. def OAI.GaussianMoat.SplitSieve.prefixSet line 92
  12. lemma OAI.GaussianMoat.SplitSieve.prefixSet_subset line 96
  13. lemma OAI.GaussianMoat.SplitSieve.prefixSet_card line 102
  14. abbrev OAI.GaussianMoat.SplitSieve.prefixSieve line 110
  15. def OAI.GaussianMoat.SplitSieve.residueVector line 114
  16. def OAI.GaussianMoat.SplitSieve.prefixIndex line 118
  17. lemma OAI.GaussianMoat.SplitSieve.prefixIndex_injective line 122
  18. lemma OAI.GaussianMoat.SplitSieve.prefix_injective_of_no_bad line 128
  19. theorem OAI.GaussianMoat.SplitSieve.prefix_entropy_rectangle line 155
  20. def OAI.GaussianMoat.SplitSieve.meanLog line 193
  21. lemma OAI.GaussianMoat.SplitSieve.prefix_log_period line 196
  22. lemma OAI.GaussianMoat.SplitSieve.prefix_product_tail line 207
  23. theorem OAI.GaussianMoat.SplitSieve.signed_prefix_entropy line 227
  24. lemma OAI.GaussianMoat.SplitSieve.residueVector_entropy_le line 275
  25. lemma OAI.GaussianMoat.SplitSieve.residue_prefix_entropy_le line 292
  26. theorem OAI.GaussianMoat.SplitSieve.actual_fresh_entropy line 305