OAI/Combinatorics/Progressions/Fourier/AllocatedJetFourierData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.sitePullbackFrequency_unit_bound line 12
  2. theorem OAI.Erdos3.BooleanCubeKernel.standardPhysicalSite_bound line 40
  3. theorem OAI.Erdos3.BooleanCubeKernel.standardSiteFrequency_bound line 44
  4. def OAI.Erdos3.BooleanCubeKernel.retainedSiteCoefficient line 51
  5. theorem OAI.Erdos3.BooleanCubeKernel.retainedSiteCoefficient_norm_sum line 57
  6. theorem OAI.Erdos3.BooleanCubeKernel.retainedSiteFourierSum_standard line 67
  7. theorem OAI.Erdos3.BooleanCubeKernel.sampled_density_standard_fourier line 93
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fixed_positive_fourier line 133
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_uniform_jet_fourier line 231
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_jet_fourier_data line 325