OAI/Combinatorics/Progressions/Estimates/InteriorIntervalCutoff.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.abs_sub_le_of_circle_dist_on_interior line 11
  2. theorem OAI.Erdos3.same_side_of_cut_of_small_displacement line 28
  3. theorem OAI.Erdos3.abs_sub_positive_sum_le line 49
  4. theorem OAI.Erdos3.sum_pair_partition_weights line 67
  5. theorem OAI.Erdos3.abs_sub_le_of_circle_dist_from_interior_center line 82
  6. theorem OAI.Erdos3.residue_fraction_mem_unit_interval line 99
  7. theorem OAI.Erdos3.residue_fraction_close_to_interior_center line 104
  8. def OAI.Erdos3.frozenRealSection line 121
  9. theorem OAI.Erdos3.frozenRealSection_unit_interval line 124
  10. def OAI.Erdos3.positiveCellParameter line 131
  11. theorem OAI.Erdos3.positiveCellParameter_of_empty line 136
  12. theorem OAI.Erdos3.positiveCellParameter_of_positive line 141
  13. theorem OAI.Erdos3.positive_discretization_error line 151
  14. theorem OAI.Erdos3.exists_positive_shift_discretization line 167
  15. theorem OAI.Erdos3.positive_partition_sum_unit_interval line 209
  16. theorem OAI.Erdos3.expect_abs_le_of_exceptional_set line 218
  17. theorem OAI.Erdos3.positive_partition_approximation_mean_error line 235
  18. theorem OAI.Erdos3.cellwise_positive_discretization_error line 258
  19. theorem OAI.Erdos3.exists_cellwise_positive_shift_discretization line 277
  20. def OAI.Erdos3.cyclicWrapExceptional line 322
  21. theorem OAI.Erdos3.cyclicWrapExceptional_card_le line 326
  22. theorem OAI.Erdos3.cyclicWrapExceptional_density_le line 346
  23. theorem OAI.Erdos3.outside_cyclicWrapExceptional line 354
  24. theorem OAI.Erdos3.good_circle_observations_control_representatives line 377
  25. theorem OAI.Erdos3.cyclic_wrap_branch_eq_of_good_circle line 388
  26. theorem OAI.Erdos3.cyclic_representative_difference_of_good_circle line 403
  27. theorem OAI.Erdos3.cyclicCutNeighborhood_mono line 421
  28. theorem OAI.Erdos3.cyclicWrapExceptional_mono line 427
  29. def OAI.Erdos3.interiorIntervalCutoff line 445
  30. theorem OAI.Erdos3.interiorIntervalCutoff_range line 448
  31. theorem OAI.Erdos3.interiorIntervalCutoff_one line 452
  32. theorem OAI.Erdos3.interiorIntervalCutoff_support line 457
  33. theorem OAI.Erdos3.interiorIntervalCutoff_lipschitz line 465
  34. theorem OAI.Erdos3.interiorIntervalCutoff_cyclic_loss line 474