OAI/Combinatorics/Progressions/Probability/MassConvolution.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.realUniformMass line 13
  2. theorem OAI.Erdos3.realUniformMass_nonneg line 16
  3. theorem OAI.Erdos3.sum_realUniformMass line 20
  4. theorem OAI.Erdos3.uniformMass_translation_le_shell line 25
  5. def OAI.Erdos3.massConvolution line 68
  6. theorem OAI.Erdos3.realUniformMass_apply_mem line 73
  7. theorem OAI.Erdos3.realUniformMass_apply_not_mem line 79
  8. theorem OAI.Erdos3.realUniformMass_ne_zero_iff line 84
  9. theorem OAI.Erdos3.massConvolution_nonneg line 92
  10. theorem OAI.Erdos3.massConvolution_comm line 99
  11. theorem OAI.Erdos3.sum_massConvolution line 108
  12. def OAI.Erdos3.convolutionPower line 118
  13. theorem OAI.Erdos3.convolutionPower_zero line 122
  14. theorem OAI.Erdos3.convolutionPower_succ line 125
  15. theorem OAI.Erdos3.convolutionPower_nonneg line 129
  16. theorem OAI.Erdos3.sum_convolutionPower line 138