OAI/Combinatorics/Progressions/Estimates/NativeSeparatedSumIntervals.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_absorb_pair_missing_coordinate_errors line 12
  2. theorem OAI.Erdos3.exists_fullCube_proper_factors line 134
  3. theorem OAI.Erdos3.exists_mixedCube_proper_factors line 176
  4. theorem OAI.Erdos3.exists_full_mixed_cube_proper_factors line 216
  5. theorem OAI.Erdos3.exists_normalized_cube_weights line 251
  6. theorem OAI.Erdos3.exists_absorb_fixed_target_cube_errors line 300
  7. def OAI.Erdos3.HasSumTargetIntervals line 374
  8. theorem OAI.Erdos3.HasSumTargetIntervals.mono line 391
  9. theorem OAI.Erdos3.HasWeightedTargetCubeIntervals.to_sum line 405
  10. def OAI.Erdos3.HasMixedTargetIntervals line 440
  11. def OAI.Erdos3.HasCommonMixedTargetInterval line 455
  12. theorem OAI.Erdos3.HasMixedTargetIntervals.mono line 470
  13. theorem OAI.Erdos3.HasCommonMixedTargetInterval.mono line 484
  14. theorem OAI.Erdos3.exists_retained_sum_target_intervals line 504
  15. theorem OAI.Erdos3.HasMixedTargetIntervals.common line 552
  16. theorem OAI.Erdos3.exists_separated_sum_intervals line 609