OAI/Combinatorics/Progressions/Fourier/AllocatedNormalizedTorusCutoff.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedBufferedTorusCutoff line 20
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedTorusCutoff_range line 28
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedTorusCutoff_lipschitz line 36
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedTorusCutoff_local line 49
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedTorusCutoff_zero_outside_quarter line 57
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedTorusCutoff_eq_siteChart line 71
  7. def OAI.Erdos3.VectorPolynomial.allocatedProductTorusCutoff line 135
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedProductTorusCutoff_range line 139
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedProductTorusCutoff_lipschitz line 148
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedProductTorusCutoff_eq line 184
  11. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedProductTorusCutoff line 238
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedProductTorusCutoff_range line 243
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedProductTorusCutoff_pullback line 251
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedProductTorusCutoff_lipschitz line 268
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_normalized_cutoff_fourier line 281