OAI/Combinatorics/Progressions/Estimates/FiniteWeightedExpansion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.jointRetainedExpansion line 12
  2. theorem OAI.Erdos3.jointRetainedExpansion_eq_product line 17
  3. theorem OAI.Erdos3.jointRetainedExpansion_count line 27
  4. theorem OAI.Erdos3.jointRetainedExpansion_coefficient_mass line 32
  5. theorem OAI.Erdos3.jointRetainedExpansion_mass_bound line 40
  6. theorem OAI.Erdos3.retainedExpansion_norm_bound line 50
  7. theorem OAI.Erdos3.joint_retained_integer_approximation line 60
  8. theorem OAI.Erdos3.norm_weighted_mixture_sub_le line 93
  9. theorem OAI.Erdos3.norm_weighted_mixture_sub_le_uniform line 104
  10. def OAI.Erdos3.weightedMixtureExpansion line 112
  11. theorem OAI.Erdos3.weightedMixtureExpansion_eq_sum line 117
  12. theorem OAI.Erdos3.weightedMixtureExpansion_coefficient_mass line 123
  13. theorem OAI.Erdos3.weightedMixtureExpansion_mass_le line 130
  14. theorem OAI.Erdos3.weightedMixtureExpansion_card_le line 142
  15. theorem OAI.Erdos3.weightedMixtureExpansion_approximation line 149