OAI/NumberTheory/GaussianMoat/SeparatedParameters.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.binEnum line 10
  2. lemma OAI.GaussianMoat.binEnum_eq line 13
  3. lemma OAI.GaussianMoat.binEnum_mem line 16
  4. lemma OAI.GaussianMoat.binEnum_strictMono line 20
  5. lemma OAI.GaussianMoat.binEnum_surj line 25
  6. lemma OAI.GaussianMoat.binEnum_sum line 31
  7. lemma OAI.GaussianMoat.precedingFactors_enum_subset line 47
  8. lemma OAI.GaussianMoat.precedingFactors_enum_cost line 56
  9. lemma OAI.GaussianMoat.precedingFactors_enum_all line 67
  10. def OAI.GaussianMoat.allBins line 83
  11. lemma OAI.GaussianMoat.bin_window_gap line 86
  12. lemma OAI.GaussianMoat.allBins_separated line 100
  13. lemma OAI.GaussianMoat.bins_disjoint line 116
  14. lemma OAI.GaussianMoat.allBins_card_upper line 132
  15. lemma OAI.GaussianMoat.allBins_rate line 151
  16. lemma OAI.GaussianMoat.exists_separated_parameters line 183