OAI/NumberTheory/Jacobsthal/Partitions/TwoSingletonBins.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.SubsetBoxBookkeeping.subset_box_original_weight line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.SubsetBoxBookkeeping.search_card_le_multiplicity line 20
  3. theorem OAI.Erdos970.NumberTheoryLean.SubsetBoxBookkeeping.length_bounded_subset_wrong_mass line 31
  4. def OAI.Erdos970.NumberTheoryLean.CanonicalSubsetBox.selectionMass line 72
  5. theorem OAI.Erdos970.NumberTheoryLean.CanonicalSubsetBox.canonical_points line 75
  6. theorem OAI.Erdos970.NumberTheoryLean.CanonicalSubsetBox.canonical_weight line 80
  7. theorem OAI.Erdos970.NumberTheoryLean.CanonicalSubsetBox.selectionMass_eq_weighted line 83
  8. theorem OAI.Erdos970.NumberTheoryLean.CanonicalSubsetBox.canonical_no_nearfull_mass line 90
  9. theorem OAI.Erdos970.NumberTheoryLean.CanonicalSubsetBox.canonical_wrong_mass line 104
  10. def OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.eraseMultiplicity line 130
  11. def OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.eraseSelection line 132
  12. def OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.fillSelection line 134
  13. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.erase_selection_mem line 137
  14. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.erased_coordinate_empty line 145
  15. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.fill_selection_mem line 150
  16. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.erase_fill line 160
  17. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.fill_erase line 167
  18. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSelection.singleton_selection_recovery line 174
  19. def OAI.Erdos970.NumberTheoryLean.PartitionedSelections.restrictMultiplicity line 189
  20. def OAI.Erdos970.NumberTheoryLean.PartitionedSelections.restrictSelection line 191
  21. def OAI.Erdos970.NumberTheoryLean.PartitionedSelections.joinSelection line 193
  22. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelections.restricted_mem line 196
  23. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelections.restricted_empty line 205
  24. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelections.joined_mem line 211
  25. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelections.join_restrictions line 222
  26. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelections.restrict_join line 227
  27. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinProduct.filled_product line 249
  28. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinProduct.filled_reciprocal line 261
  29. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelectionSums.joined_product line 275
  30. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelectionSums.partitioned_sum line 290
  31. theorem OAI.Erdos970.NumberTheoryLean.PartitionedSelectionSums.partitioned_weighted_sum line 311
  32. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSum.singleton_sum line 332
  33. theorem OAI.Erdos970.NumberTheoryLean.SingletonBinSum.singleton_weighted_sum line 359
  34. def OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.eraseTwo line 379
  35. def OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.fillTwo line 381
  36. theorem OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.eraseTwo_zero line 384
  37. theorem OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.eraseTwo_le line 387
  38. theorem OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.fillTwo_mem line 391
  39. theorem OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.fillTwo_product line 398
  40. theorem OAI.Erdos970.NumberTheoryLean.TwoSingletonBins.two_singleton_weighted_sum line 408