OAI/Combinatorics/Progressions/Fourier/StandardJetFourier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.euclideanAmbientTorus_normalized line 13
  2. theorem OAI.Erdos3.normalizedCoveredChart_projection line 32
  3. def OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus line 51
  4. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_continuous line 58
  5. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_chart line 68
  6. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_coefficient line 101
  7. def OAI.Erdos3.VectorPolynomial.jetAmbientCoefficientFrequency line 119
  8. theorem OAI.Erdos3.VectorPolynomial.jetAmbientCoefficientFrequency_character line 125
  9. theorem OAI.Erdos3.VectorPolynomial.jetAmbientCoefficientFrequency_bound line 154
  10. def OAI.Erdos3.VectorPolynomial.rowSiteAmbientTorus line 193
  11. theorem OAI.Erdos3.VectorPolynomial.rowSiteAmbientTorus_lipschitz line 198
  12. theorem OAI.Erdos3.VectorPolynomial.coveredRowsSiteValue_ambient line 222
  13. theorem OAI.Erdos3.BooleanCubeKernel.standardPhysicalSite_apply line 241
  14. theorem OAI.Erdos3.BooleanCubeKernel.boundedSiteMatrix_standard line 245
  15. theorem OAI.Erdos3.BooleanCubeKernel.boundedCoefficientJetMatrix_standard line 257
  16. theorem OAI.Erdos3.BooleanCubeKernel.coefficientExponent_support_card_le line 267
  17. def OAI.Erdos3.BooleanCubeKernel.standardJetFrequency line 275
  18. theorem OAI.Erdos3.BooleanCubeKernel.standardJetFrequency_apply line 281
  19. theorem OAI.Erdos3.BooleanCubeKernel.standardJetFrequency_bound line 298
  20. theorem OAI.Erdos3.BooleanCubeKernel.standardJetFrequency_character line 307