OAI/NumberTheory/Jacobsthal/Estimates/ConditionalPatternCounts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.ErdosLargePatternLaw.FullPattern line 14
  2. def OAI.Erdos970.ErdosLargePatternLaw.weight line 18
  3. def OAI.Erdos970.ErdosLargePatternLaw.expectation line 22
  4. def OAI.Erdos970.ErdosLargePatternLaw.survives line 25
  5. def OAI.Erdos970.ErdosLargePatternLaw.jointCondition line 31
  6. def OAI.Erdos970.ErdosLargePatternLaw.indicator line 34
  7. def OAI.Erdos970.ErdosLargePatternLaw.survivorCount line 37
  8. theorem OAI.Erdos970.ErdosLargePatternLaw.pattern_card line 40
  9. theorem OAI.Erdos970.ErdosLargePatternLaw.weight_positive line 45
  10. theorem OAI.Erdos970.ErdosLargePatternLaw.weight_sum line 53
  11. theorem OAI.Erdos970.ErdosLargePatternLaw.indicator_binary line 63
  12. theorem OAI.Erdos970.ErdosLargePatternLaw.count_eq_indicator_sum line 68
  13. def OAI.Erdos970.ErdosLargePatternLaw.projectedUnit line 83
  14. theorem OAI.Erdos970.ErdosLargePatternLaw.projectedUnit_coe line 86
  15. def OAI.Erdos970.ErdosLargePatternLaw.divisorCondition line 95
  16. def OAI.Erdos970.ErdosLargePatternLaw.coprimeCondition line 99
  17. theorem OAI.Erdos970.ErdosLargePatternLaw.joint_condition_split line 104
  18. theorem OAI.Erdos970.ErdosLargePatternLaw.divisor_condition_card line 115
  19. theorem OAI.Erdos970.ErdosLargePatternLaw.multiply_unit_iff line 139
  20. theorem OAI.Erdos970.ErdosLargePatternLaw.coprime_condition_card line 148