OAI/NumberTheory/GaussianMoat/WalkWords.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.incrementWord line 10
  2. lemma OAI.GaussianMoat.incrementWord_sum line 13
  3. lemma OAI.GaussianMoat.block_displacement line 20
  4. lemma OAI.GaussianMoat.residue_block_update line 34
  5. theorem OAI.GaussianMoat.incrementWord_blocks_entropy line 45
  6. def OAI.GaussianMoat.boundedWord line 73
  7. lemma OAI.GaussianMoat.boundedWord_fibers line 79
  8. lemma OAI.GaussianMoat.boundedWord_entropy_le line 90
  9. lemma OAI.GaussianMoat.gaussianResidue_add line 101
  10. lemma OAI.GaussianMoat.gaussianResidue_sub line 103
  11. lemma OAI.GaussianMoat.gaussianResidue_zero line 105
  12. lemma OAI.GaussianMoat.short_residue_hits_disjoint line 107
  13. lemma OAI.GaussianMoat.short_residue_hit_prob line 129
  14. theorem OAI.GaussianMoat.smoothed_package_hit_lower line 140
  15. lemma OAI.GaussianMoat.true_residue_no_hit line 163
  16. lemma OAI.GaussianMoat.FinLaw.cHf_congr_fibers line 178
  17. lemma OAI.GaussianMoat.residueCode_vector_fibers line 190
  18. theorem OAI.GaussianMoat.word_residue_smoothing line 195