OAI/Combinatorics/Progressions/Probability/CommonSectionAmbientDensityMultiple.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.coefficientResidualAmbientDensity line 20
  2. theorem OAI.Erdos3.VectorPolynomial.coefficientResidualAmbientDensity_eq line 28
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientResidualAmbientDensity_bounds line 41
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientResidualAmbientDensity_lipschitz line 56
  5. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_density_projected_fourier line 100
  6. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_euclidean_density_projected_fourier line 209
  7. theorem OAI.Erdos3.VectorPolynomial.unitAddCircle_coe_sum line 299
  8. def OAI.Erdos3.VectorPolynomial.coefficientAmbientSiteSection line 306
  9. def OAI.Erdos3.VectorPolynomial.coefficientAmbientSiteEvaluation line 312
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientSiteSection_lipschitz line 317
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientSiteSection_residual line 343
  12. def OAI.Erdos3.VectorPolynomial.coefficientSectionAmbientDensity line 374
  13. theorem OAI.Erdos3.VectorPolynomial.coefficientSectionAmbientDensity_lipschitz line 379
  14. theorem OAI.Erdos3.VectorPolynomial.coefficientSectionAmbientDensity_bounds line 388
  15. theorem OAI.Erdos3.VectorPolynomial.coefficientSectionAmbientDensity_eq line 395
  16. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_ambient_density line 429
  17. theorem OAI.Erdos3.BooleanCubeKernel.exists_fixed_kernel_ambient_density_multiple line 531