OAI/Combinatorics/Progressions/Sampling/GridNormalizationTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.grid_rescale_coordinate line 11
2. theorem OAI.Erdos3.grid_normalization_identity line 17
3. theorem OAI.Erdos3.grid_normalization_error line 22
4. theorem OAI.Erdos3.complex_lipschitz_rescale line 32
5. theorem OAI.Erdos3.grid_site_coefficient_norm line 43
6. theorem OAI.Erdos3.grid_site_normalization_error line 48