OAI/Combinatorics/Progressions/Estimates/NormalizedTwistParameterPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.exponentialProgressionScale line 11
  2. theorem OAI.Erdos3.exponentialProgressionScale_bounds line 14
  3. theorem OAI.Erdos3.FiniteProgressionPartition.normalized_point_sub_point_le line 78
  4. theorem OAI.Erdos3.FiniteProgressionPartition.normalized_point_sub_point_le_of_bound line 104
  5. theorem OAI.Erdos3.FiniteProgressionPartition.normalized_point_sub_start_le line 111
  6. theorem OAI.Erdos3.FiniteProgressionPartition.normalized_point_sub_start_le_of_bound line 120
  7. theorem OAI.Erdos3.FiniteProgressionPartition.label_card_mul_le_of_length_lower line 139
  8. theorem OAI.Erdos3.FiniteProgressionPartition.label_card_le_exp_of_length_lower line 149
  9. theorem OAI.Erdos3.exists_normalizedTwist_parameter_partition line 162