OAI/Combinatorics/Progressions/Sampling/FixedPathSlicedGridMeshBudget.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarCubeGridHistogram line 13
  2. def OAI.Erdos3.scalarCubeGridBoundaryConstant line 17
  3. theorem OAI.Erdos3.scalarCubeGridHistogram_eq line 20
  4. theorem OAI.Erdos3.scalarCubeGridHistogram_integrable line 25
  5. theorem OAI.Erdos3.scalarCubeGridHistogram_point_error line 29
  6. theorem OAI.Erdos3.scalarCubeGridHistogram_l1_error line 51
  7. theorem OAI.Erdos3.scalarCubeGridHistogram_mass_error line 72
  8. theorem OAI.Erdos3.scalarCubeGridHistogram_mass_pos line 81
  9. theorem OAI.Erdos3.scalarCubeGridHistogram_normalized_l1 line 89
  10. def OAI.Erdos3.scalarCubeGridSet line 125
  11. theorem OAI.Erdos3.mem_scalarCubeGridSet line 130
  12. theorem OAI.Erdos3.scalarCubeGridHistogram_finite line 145
  13. theorem OAI.Erdos3.scalarCubeGridHistogram_mass line 157
  14. theorem OAI.Erdos3.scalarCubeGridSet_nonempty line 163
  15. theorem OAI.Erdos3.scalarCubeGridHistogram_mean line 171
  16. theorem OAI.Erdos3.scalarCubeIndicator_test line 180
  17. theorem OAI.Erdos3.scalarCubeGrid_comparison line 209
  18. theorem OAI.Erdos3.fixedPathSlicedGrid_ratio_le line 242
  19. theorem OAI.Erdos3.fixedPathSlicedGrid_sum_ratio_le line 251
  20. def OAI.Erdos3.fixedPathSlicedGridMeshLog line 264
  21. def OAI.Erdos3.fixedPathSlicedGridMeshFloor line 267
  22. theorem OAI.Erdos3.fixedPathSlicedGridMeshFloor_lower line 270
  23. theorem OAI.Erdos3.fixedPathSlicedGridMeshFloor_pos line 274
  24. theorem OAI.Erdos3.fixedPathSlicedGridMeshFloor_le_exp line 278
  25. theorem OAI.Erdos3.fixedPathSlicedGridMeshLog_le line 296
  26. theorem OAI.Erdos3.fixedPathSlicedGridMeshFloor_le_exp_of_prefactor line 316
  27. theorem OAI.Erdos3.fixedPathSlicedGridMesh_prefactor line 325
  28. theorem OAI.Erdos3.fixedPathSlicedGridMesh_of_floor line 350