OAI/Combinatorics/Progressions/Fourier/UniformEmbeddedFourier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.integerGridMixture line 14
2. theorem OAI.Erdos3.integerGridMixture_eq_sum line 22
3. theorem OAI.Erdos3.integerGridMixture_coefficient_mass line 36
4. theorem OAI.Erdos3.integerGridMixture_approximation line 53
5. theorem OAI.Erdos3.IntegerFourierBudget.mixture_approximation line 83
6. def OAI.Erdos3.retainedImageMass line 129
7. theorem OAI.Erdos3.FiniteProbabilityWeights.embedded_cell_image_mass line 135
8. theorem OAI.Erdos3.FiniteProbabilityWeights.embedded_cell_fourier_approximation line 151
9. theorem OAI.Erdos3.IntegerFourierBudget.embedded_mixture_approximation line 193