OAI/Combinatorics/Progressions/Sampling/IntegralGridFunctional.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.coordinateGridModule line 13
2. theorem OAI.Erdos3.mem_coordinateGridModule line 30
3. theorem OAI.Erdos3.scaled_basis_mem_coordinateGridModule line 33
4. theorem OAI.Erdos3.coordinateGrid_bracket_divisible line 41
5. theorem OAI.Erdos3.coordinateGridModule_map_of_basis line 80
6. theorem OAI.Erdos3.linearFunctional_coordinate_height line 107
7. theorem OAI.Erdos3.coordinateGrid_functional_integral line 119