OAI/NumberTheory/GaussianMoat/SignedResidues.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GaussianMoat.SplitSieve.SignedIndex line 10
  2. def OAI.GaussianMoat.SplitSieve.signedPrime line 12
  3. def OAI.GaussianMoat.SplitSieve.signedFactorAt line 14
  4. lemma OAI.GaussianMoat.SplitSieve.signedFactorAt_norm line 17
  5. lemma OAI.GaussianMoat.SplitSieve.signedFactorAt_ne_zero line 22
  6. abbrev OAI.GaussianMoat.SplitSieve.Residue line 32
  7. instance OAI.GaussianMoat.SplitSieve.residueFintype line 34
  8. lemma OAI.GaussianMoat.SplitSieve.residue_card line 39
  9. def OAI.GaussianMoat.SplitSieve.residue line 46
  10. lemma OAI.GaussianMoat.SplitSieve.residue_fibers line 49
  11. lemma OAI.GaussianMoat.FinLaw.uniform_expect line 55
  12. lemma OAI.GaussianMoat.SplitSieve.signedIndex_nonempty line 60
  13. theorem OAI.GaussianMoat.SplitSieve.signed_coverage_deficit line 65
  14. def OAI.GaussianMoat.FinLaw.lowResidues line 106
  15. lemma OAI.GaussianMoat.FinLaw.not_mem_lowResidues line 109
  16. lemma OAI.GaussianMoat.FinLaw.lowResidues_prob line 113
  17. lemma OAI.GaussianMoat.FinLaw.lowResidues_equiv line 132
  18. theorem OAI.GaussianMoat.FinLaw.lowResidues_base line 145
  19. theorem OAI.GaussianMoat.FinLaw.lowResidues_backward line 163