OAI/Combinatorics/Progressions/Linear/SmallKernelAllSites.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.matrixSupCLM_smul line 15
  2. theorem OAI.Erdos3.scalar_identity_inverse_bound line 22
  3. theorem OAI.Erdos3.matrix_inverse_near_scalar_identity line 45
  4. def OAI.Erdos3.kernelColumnCenter line 79
  5. def OAI.Erdos3.kernelSpatialAnchor line 84
  6. def OAI.Erdos3.kernelSpatialWidths line 90
  7. theorem OAI.Erdos3.kernelSpatialWidths_pos line 97
  8. def OAI.Erdos3.normalizedKernelBlock line 110
  9. theorem OAI.Erdos3.kernelSpatial_kernel_error line 128
  10. theorem OAI.Erdos3.kernelSpatial_nonkernel_bound line 144
  11. theorem OAI.Erdos3.kernelSpatial_column_bound line 159
  12. theorem OAI.Erdos3.scaled_coordinate_product_bound line 183
  13. theorem OAI.Erdos3.kernelSpatial_nonkernel_displacement line 194
  14. theorem OAI.Erdos3.kernelSpatial_kernel_inverse line 227
  15. theorem OAI.Erdos3.kernelSpatial_site_deviation line 242
  16. theorem OAI.Erdos3.kernelSpatial_site_mem_box line 276
  17. theorem OAI.Erdos3.translatedKernelSpatial_support line 306
  18. def OAI.Erdos3.kernelAnchorScale line 351
  19. def OAI.Erdos3.kernelNoiseScale line 354
  20. theorem OAI.Erdos3.kernelSpatial_scales line 357
  21. theorem OAI.Erdos3.kernelSpatialWidths_lower_bound line 387
  22. theorem OAI.Erdos3.kernelNoiseScale_reciprocal line 435
  23. theorem OAI.Erdos3.kernelNoiseScale_reciprocal_le line 442
  24. theorem OAI.Erdos3.kernelSpatial_relative_width_budget line 457
  25. theorem OAI.Erdos3.kernelSpatial_rounding_scale line 473
  26. theorem OAI.Erdos3.two_div_kernelAnchorScale line 509
  27. theorem OAI.Erdos3.kernelNoiseScale_nonkernel_cap line 515
  28. theorem OAI.Erdos3.kernelSpatial_early_widths_independent line 527
  29. theorem OAI.Erdos3.canonicalKernelSpatial_support line 533
  30. def OAI.Erdos3.smallKernelSpatialAnchor line 584
  31. def OAI.Erdos3.smallKernelSpatialWidths line 588
  32. theorem OAI.Erdos3.smallKernelSpatialWidths_pos line 592
  33. theorem OAI.Erdos3.smallKernelSpatialWidths_le line 598
  34. theorem OAI.Erdos3.smallKernelSpatial_column_identity line 614
  35. theorem OAI.Erdos3.smallKernelSpatial_column_bound line 633
  36. theorem OAI.Erdos3.smallKernelSpatial_site_bound line 648
  37. theorem OAI.Erdos3.smallKernelSpatial_trim_margin line 688
  38. theorem OAI.Erdos3.smallKernelSpatialWidths_lower_bound line 711
  39. theorem OAI.Erdos3.smallKernelSpatial_relative_width_budget line 725
  40. theorem OAI.Erdos3.smallKernelSpatial_rounding_scale line 742
  41. theorem OAI.Erdos3.smallKernelSpatial_kernel_inverse line 784
  42. theorem OAI.Erdos3.smallKernelSpatial_nonkernel_displacement line 815
  43. theorem OAI.Erdos3.smallKernelSpatial_base_mem_box line 837
  44. theorem OAI.Erdos3.translatedSmallKernelSpatial_support line 853
  45. theorem OAI.Erdos3.BooleanCubeKernel.exists_small_kernel_near_uniform_sampler line 905
  46. theorem OAI.Erdos3.BooleanCubeKernel.exists_small_kernel_all_sites_sampler line 1190