OAI/NumberTheory/JointDickman/Probability/SiteTestRestriction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Single-site tests after fixing sampled coordinates

  1. def OAI.JointDickman.siteTestMean line 12
  2. def OAI.JointDickman.maskedSiteTest line 17
  3. theorem OAI.JointDickman.siteProduct_unfrozen_pair line 20
  4. theorem OAI.JointDickman.siteTestMean_masked_frozen line 34
  5. theorem OAI.JointDickman.siteTestMean_restriction_bound line 54