OAI/Combinatorics/Progressions/Lattices/SmoothResidueWindowMass.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.selectedResidueDensityMass line 13
  2. theorem OAI.Erdos3.selectedResidueDensityMass_complex line 18
  3. def OAI.Erdos3.selectedResidueDensityPMF line 26
  4. theorem OAI.Erdos3.selectedResidueDensityPMF_toReal line 36
  5. theorem OAI.Erdos3.selectedResidueDensityPMF_complexMean line 48
  6. theorem OAI.Erdos3.selectedResidueDensityPMF_error line 61
  7. theorem OAI.Erdos3.selectedResidueDensityMass_integral line 85
  8. theorem OAI.Erdos3.selectedResidueDensityPMF_zero_off line 106
  9. theorem OAI.Erdos3.selectedResidueDensityPMF_zero_of_density_zero line 118
  10. theorem OAI.Erdos3.selectedResidueDensityPMF_domination line 128
  11. def OAI.Erdos3.selectedResidueFiniteLaw line 154
  12. theorem OAI.Erdos3.selectedResidueFiniteLaw_complexMean line 163
  13. theorem OAI.Erdos3.selectedResidueFiniteLaw_mean line 171
  14. theorem OAI.Erdos3.selectedResidueFiniteLaw_densityMass line 182
  15. theorem OAI.Erdos3.selectedResidueDensityPMF_mean line 191
  16. def OAI.Erdos3.columnResidueReduction line 211
  17. theorem OAI.Erdos3.columnResidueReduction_pattern line 216
  18. def OAI.Erdos3.selectedResidueRefinement line 223
  19. theorem OAI.Erdos3.mem_selectedResidueRefinement line 229
  20. theorem OAI.Erdos3.selectedResidueSmoothWeight_refinement line 237
  21. theorem OAI.Erdos3.selectedResidueSmoothMass_refinement line 246
  22. theorem OAI.Erdos3.selectedResidueSmoothPMF_refinement line 254
  23. theorem OAI.Erdos3.selectedResidueRefinement_nonempty line 267
  24. def OAI.Erdos3.selectedResidueExtraRefinement line 279
  25. def OAI.Erdos3.refinedColumnExtraResidue line 285
  26. theorem OAI.Erdos3.refinedColumnExtraResidue_of_pattern line 290
  27. theorem OAI.Erdos3.refinedResidueLatticeArray_extraResidue line 297
  28. theorem OAI.Erdos3.selectedResidueDensityMass_refinement line 307
  29. theorem OAI.Erdos3.selectedResidueDensityPMF_refinement line 315
  30. theorem OAI.Erdos3.selectedResidueDensityPMF_raw_error line 342
  31. theorem OAI.Erdos3.selectedResidueDensityPMF_singleton_complexMean_congr line 374
  32. theorem OAI.Erdos3.smoothProbabilityProfile_plateau line 403
  33. theorem OAI.Erdos3.selectedResidueSmoothWeight_plateau line 411
  34. theorem OAI.Erdos3.selectedResidueDensityMass_window_bound line 425
  35. theorem OAI.Erdos3.selectedResidueSmoothWeight_singleton_mass_upper line 444
  36. theorem OAI.Erdos3.selectedResidueDensityMass_singleton_window_bound line 470