OAI/NumberTheory/GaussianMoat/DyadicSieve.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.chosenSplitFactor line 10
  2. lemma OAI.GaussianMoat.chosenSplitFactor_spec line 13
  3. def OAI.GaussianMoat.splitSieveOf line 18
  4. def OAI.GaussianMoat.dyadicSieve line 27
  5. lemma OAI.GaussianMoat.gaussian_norm_log_nonneg line 32
  6. def OAI.GaussianMoat.residueWeight line 37
  7. lemma OAI.GaussianMoat.residueWeight_mono line 40
  8. lemma OAI.GaussianMoat.residueWeight_nonneg line 43
  9. theorem OAI.GaussianMoat.residue_vector_entropy line 46
  10. lemma OAI.GaussianMoat.residue_finset_entropy line 62
  11. def OAI.GaussianMoat.SplitSieve.availableFactors line 69
  12. lemma OAI.GaussianMoat.SplitSieve.signed_mem_available line 72
  13. lemma OAI.GaussianMoat.SplitSieve.available_ne_zero line 76
  14. lemma OAI.GaussianMoat.SplitSieve.available_weight line 86
  15. lemma OAI.GaussianMoat.FinLaw.cIf_finset_union line 99