OAI/NumberTheory/Jacobsthal/Sieve/ActualCofactorCellData.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosCofactorChoices.selections line 14
  2. theorem OAI.Erdos970.ErdosCofactorChoices.mem_selections line 18
  3. def OAI.Erdos970.ErdosCofactorChoices.selectionProduct line 23
  4. def OAI.Erdos970.ErdosCofactorChoices.selectionPrimes line 26
  5. theorem OAI.Erdos970.ErdosCofactorChoices.selection_disjoint line 29
  6. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_eq_union line 36
  7. theorem OAI.Erdos970.ErdosCofactorChoices.recover_bin line 43
  8. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_primeFactors line 58
  9. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_pos line 69
  10. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_injOn line 83
  11. def OAI.Erdos970.ErdosCofactorChoices.cofactorChoices line 98
  12. theorem OAI.Erdos970.ErdosCofactorChoices.selections_card line 102
  13. theorem OAI.Erdos970.ErdosCofactorChoices.cofactorChoices_card line 107
  14. theorem OAI.Erdos970.ErdosCofactorChoices.cofactorChoices_nonempty line 115
  15. theorem OAI.Erdos970.ErdosCofactorChoices.cofactor_positive line 124
  16. theorem OAI.Erdos970.ErdosCofactorChoices.half_power_le_choose line 139
  17. theorem OAI.Erdos970.ErdosCofactorChoices.factorial_le_uniform_power line 152
  18. theorem OAI.Erdos970.ErdosCofactorChoices.scaled_power_le_choose line 156
  19. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_squarefree line 184
  20. theorem OAI.Erdos970.ErdosCofactorChoices.cofactor_squarefree line 198
  21. theorem OAI.Erdos970.ErdosCofactorChoices.prime_factor_bin_recovery line 206
  22. theorem OAI.Erdos970.ErdosCofactorChoices.cofactor_card_half_lower line 225
  23. theorem OAI.Erdos970.ErdosCofactorChoices.cofactor_card_scaled_lower line 236
  24. theorem OAI.Erdos970.ErdosCofactorChoices.denominator_loss_budget line 269
  25. theorem OAI.Erdos970.ErdosCofactorChoices.cofactor_card_exponential_lower line 303
  26. theorem OAI.Erdos970.ErdosCofactorChoices.source_log_budget line 337
  27. theorem OAI.Erdos970.ErdosCofactorChoices.sqrt_sourceW_dominates line 348
  28. theorem OAI.Erdos970.ErdosCofactorChoices.source_multiplicity_room line 371
  29. theorem OAI.Erdos970.ErdosCofactorChoices.source_prime_bin_data line 392
  30. theorem OAI.Erdos970.ErdosCofactorChoices.source_cofactor_count_lower line 432
  31. theorem OAI.Erdos970.ErdosCofactorChoices.source_span_geometry line 479
  32. def OAI.Erdos970.ErdosCofactorChoices.actualBins line 498
  33. def OAI.Erdos970.ErdosCofactorChoices.cofactorScale line 501
  34. theorem OAI.Erdos970.ErdosCofactorChoices.cofactorScale_nonneg line 504
  35. theorem OAI.Erdos970.ErdosCofactorChoices.actual_source_many_cofactors line 511
  36. theorem OAI.Erdos970.ErdosCofactorChoices.actual_source_many_cofactors_power line 533
  37. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_upper line 564
  38. theorem OAI.Erdos970.ErdosCofactorChoices.selectionProduct_lower line 578
  39. theorem OAI.Erdos970.ErdosCofactorChoices.actual_cofactor_range line 595
  40. theorem OAI.Erdos970.ErdosCofactorChoices.actual_cofactor_positive line 621
  41. theorem OAI.Erdos970.ErdosCofactorChoices.actual_cofactor_ratio line 627
  42. theorem OAI.Erdos970.ErdosCofactorChoices.actual_reciprocal_variation line 650
  43. theorem OAI.Erdos970.ErdosCofactorChoices.source_bin_factor_subpower line 663
  44. theorem OAI.Erdos970.ErdosCofactorChoices.source_cofactor_weight_variation line 686
  45. theorem OAI.Erdos970.ErdosInverseCells.actual_cofactorScale_pos line 712
  46. theorem OAI.Erdos970.ErdosInverseCells.actual_cofactor_squarefree line 719
  47. theorem OAI.Erdos970.ErdosInverseCells.actual_cofactor_effective_range line 725
  48. theorem OAI.Erdos970.ErdosInverseCells.source_cofactor_cell_data line 750