OAI/Combinatorics/Progressions/Lattices/SelectedResidueRefinementMean.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.selectedResidueCellWeight line 13
  2. theorem OAI.Erdos3.selectedResidueCellWeight_nonneg line 18
  3. theorem OAI.Erdos3.selectedResidueCellWeight_sum line 30
  4. theorem OAI.Erdos3.selectedResidueSmoothPMF_bounded_mixture line 37
  5. theorem OAI.Erdos3.selectedResidue_bounded_mixture_error line 60
  6. theorem OAI.Erdos3.residueProfile_center_ratio line 92
  7. theorem OAI.Erdos3.residueSmoothIndexPMF_recenter_test line 100
  8. theorem OAI.Erdos3.residueSmoothPMF_recenter_test line 114
  9. theorem OAI.Erdos3.boundedResidueSmoothPMF_recenter_test line 128
  10. theorem OAI.Erdos3.selectedResidueSmoothPMF_recenter_test line 152
  11. theorem OAI.Erdos3.selectedResidueSmoothPMF_bind_toReal_mixture line 182
  12. theorem OAI.Erdos3.selectedResidueSmoothPMF_bind_le_of_cells line 200
  13. theorem OAI.Erdos3.selectedResidueDensityMass_bounded_mixture line 231
  14. theorem OAI.Erdos3.selectedResidueDensityNumerator_bounded_mixture line 249
  15. theorem OAI.Erdos3.selectedResidueDensityPMF_bounded_mixture_ratio line 266
  16. theorem OAI.Erdos3.selectedResidueSmoothWeight_singleton line 288
  17. theorem OAI.Erdos3.selectedResidueSmoothWeight_mass_pos_of_singletons line 295
  18. theorem OAI.Erdos3.selectedResidueSmoothPMF_singleton_mixture line 304
  19. theorem OAI.Erdos3.selectedResidueDensityMass_singleton_mixture line 327
  20. theorem OAI.Erdos3.selectedResidueDensityNumerator_singleton_mixture line 343
  21. theorem OAI.Erdos3.selectedResidueDensityPMF_singleton_mixture_ratio line 357
  22. theorem OAI.Erdos3.selectedResidueDensityPMF_singleton_mixture_error line 375
  23. theorem OAI.Erdos3.selectedResidueSmoothPMF_singleton_residue_mean line 447
  24. theorem OAI.Erdos3.selectedResidueRefinement_weighted_mean line 470