OAI/Combinatorics/Progressions/Sampling/AllocatedGridNaturalWindow.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.count_finset_indicator_data line 12
  2. def OAI.Erdos3.VectorPolynomial.allocatedGridWindowFactor line 41
  3. def OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight line 49
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowFactor_nonneg line 57
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight_nonneg line 69
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowFactor_measurable line 77
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight_measurable line 91
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowFactor_mass_data line 100
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight_mass_data line 126
  10. def OAI.Erdos3.VectorPolynomial.allocatedSelectedGridMass line 163
  11. def OAI.Erdos3.VectorPolynomial.allocatedRemainingGridMass line 169
  12. def OAI.Erdos3.VectorPolynomial.allocatedPartialGridApproximation line 175
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedRemainingGridMass_nonneg line 183
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedGridMass_mul_remaining line 195
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedRemainingGridMass_measurable line 207
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedPartialGridApproximation_measurable line 216
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight_inside line 224
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight_outside line 238
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedPartialGridApproximation_error line 250
  20. def OAI.Erdos3.VectorPolynomial.allocatedSelectedGridExtension line 314
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedGridExtension_measurable line 318
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedGridExtension_error line 325
  23. def OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalScale line 359
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalScale_pos line 363
  25. def OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalRadius line 371
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalRadius_nonneg line 375
  27. def OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalWindow line 383
  28. def OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalVolume line 389
  29. def OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalWindowVolume line 393
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalWindow_card_le line 397
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalVolume_pos line 408
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedNaturalWindowVolume_nonneg line 417
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenNaturalWindow_selected_card_le line 426