OAI/Combinatorics/Progressions/Probability/UniformSelectedCoefficientProductLaw.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.pmf_map_injective_cap line 12
  2. theorem OAI.Erdos3.pmf_bind_point_cap line 22
  3. theorem OAI.Erdos3.pmf_bind_injective_toReal_cap line 29
  4. theorem OAI.Erdos3.pmf_map_toReal_indicator line 40
  5. theorem OAI.Erdos3.pmf_point_indicator_norm line 51
  6. def OAI.Erdos3.baseArrayJoin line 68
  7. theorem OAI.Erdos3.baseArrayJoin_injective line 71
  8. theorem OAI.Erdos3.baseArrayJoin_eta line 77
  9. theorem OAI.Erdos3.independentProductPMF_base_split line 83
  10. theorem OAI.Erdos3.independentProductPMF_base_cap line 105
  11. abbrev OAI.Erdos3.SelectedCoefficientComplement line 128
  12. def OAI.Erdos3.selectedCoefficientComplementFill line 131
  13. def OAI.Erdos3.selectedCoefficientJoin line 135
  14. theorem OAI.Erdos3.selectedCoefficientJoin_selected line 140
  15. theorem OAI.Erdos3.selectedCoefficientJoin_complement line 146
  16. theorem OAI.Erdos3.selectedCoefficientJoin_injective line 153
  17. theorem OAI.Erdos3.selectedCoefficientJoin_eta line 161
  18. theorem OAI.Erdos3.prod_selected_complement line 170
  19. theorem OAI.Erdos3.independentProductPMF_selected_split line 179
  20. theorem OAI.Erdos3.independentProductPMF_uniform line 216
  21. theorem OAI.Erdos3.uniformOfFintype_selected_split line 225
  22. theorem OAI.Erdos3.uniformZMod_selected_split line 241