OAI/Combinatorics/Progressions/Sampling/PatchKernelGridBudget.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.patchKernelGridRadius line 13
  2. theorem OAI.Erdos3.patchKernelGridRadius_pos line 15
  3. theorem OAI.Erdos3.patchKernelGridRadius_small line 20
  4. def OAI.Erdos3.gridPatchKernel line 29
  5. theorem OAI.Erdos3.gridPatchKernel_translate line 50
  6. theorem OAI.Erdos3.gridPatchKernel_original_support line 56
  7. theorem OAI.Erdos3.PatchKernel.grid_approx line 72
  8. theorem OAI.Erdos3.exists_positive_combination_term line 98
  9. def OAI.Erdos3.PolynomialPatch.gridKernelReplacement line 117
  10. theorem OAI.Erdos3.PolynomialPatch.gridKernelReplacement_value line 121
  11. theorem OAI.Erdos3.PolynomialPatch.gridKernelReplacement_approx line 128
  12. theorem OAI.Erdos3.PolynomialPatch.gridKernelReplacement_score line 143
  13. theorem OAI.Erdos3.PolynomialPatch.exists_gridKernelReplacement_score line 175
  14. theorem OAI.Erdos3.exists_patch_kernel_mesh line 203