OAI/Combinatorics/Progressions/Linear/FixedKernelEuclideanDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_site_residual line 11
  2. theorem OAI.Erdos3.VectorPolynomial.exists_bounded_residual_cover_budget line 72
  3. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_bounded_section line 89
  4. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_bounded_section_multiple line 164
  5. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_covered_density line 226
  6. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_euclidean_density line 300