OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Truncation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.SourceBonferroni.truncation line 24
  2. lemma OAI.OrdinaryCorrelations.SourceBonferroni.truncation_succ line 27
  3. lemma OAI.OrdinaryCorrelations.SourceBonferroni.truncation_zero line 33
  4. theorem OAI.OrdinaryCorrelations.SourceBonferroni.even_error line 41
  5. def OAI.OrdinaryCorrelations.SourceBonferroni.badCount line 59
  6. def OAI.OrdinaryCorrelations.SourceBonferroni.joint line 62
  7. def OAI.OrdinaryCorrelations.SourceBonferroni.survives line 65
  8. lemma OAI.OrdinaryCorrelations.SourceBonferroni.joint_choose line 68
  9. lemma OAI.OrdinaryCorrelations.SourceBonferroni.survives_eq line 84
  10. def OAI.OrdinaryCorrelations.SourceBonferroni.intersectionMass line 90
  11. def OAI.OrdinaryCorrelations.SourceBonferroni.survivalMass line 93
  12. def OAI.OrdinaryCorrelations.SourceBonferroni.eventTruncation line 96
  13. lemma OAI.OrdinaryCorrelations.SourceBonferroni.eventTruncation_eq line 100
  14. theorem OAI.OrdinaryCorrelations.SourceBonferroni.finite_bonferroni line 119
  15. def OAI.OrdinaryCorrelations.SourceBonferroni.elementary line 142
  16. theorem OAI.OrdinaryCorrelations.SourceBonferroni.elementary_le_exp line 145
  17. theorem OAI.OrdinaryCorrelations.SourceBonferroni.elementary_source_scale line 174