OAI/Combinatorics/Progressions/Sampling/AllocatedLongGridIntegral.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedLongScalarEquiv line 29
  2. def OAI.Erdos3.VectorPolynomial.allocatedLongRealScalarEquiv line 36
  3. def OAI.Erdos3.VectorPolynomial.allocatedLongIntegerScalarEquiv line 41
  4. def OAI.Erdos3.VectorPolynomial.allocatedLongGridEquiv line 46
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridEquiv_apply line 53
  6. def OAI.Erdos3.VectorPolynomial.allocatedLongGridMask line 99
  7. def OAI.Erdos3.VectorPolynomial.allocatedLongGridDensityTest line 103
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridDensityTest_eq line 110
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridDensityTest_proxy line 120
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridMask_bound line 134
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridDensityTest_comparison line 158
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedLongScalarEquiv_measurePreserving line 213
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedLongRealScalarEquiv_measurePreserving line 231
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedLongIntegerScalarEquiv_measurePreserving line 238
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridEquiv_measurePreserving line 245
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridEquiv_coe line 268
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedLongRowsFromGrid_measurePreserving line 276
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedLongRowsFromGrid_integral line 285
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedLongRowsFromGrid_integrable_iff line 295
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedLongRowsFromGrid_integral_finset line 304
  21. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_long_grid_comparison line 343
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedLongRowsFromGrid_zero_off_indices line 474
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedLongGridDensityTest_integral line 486