OAI/Combinatorics/SumProduct/Alignment/FejerDetection01.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FejerDetection.mean_near_one line 16
2. lemma OAI.FejerDetection.near_integer_phase line 30
3. lemma OAI.FejerDetection.energy_identity line 45
4. theorem OAI.FejerDetection.detect line 66
5. lemma OAI.LagrangeBounds.basis_bound line 134
6. theorem OAI.LagrangeBounds.interpolate_error line 157
7. lemma OAI.DenseIntegerNodes.strictMono_int_gap line 187
8. theorem OAI.DenseIntegerNodes.separated line 203
9. theorem OAI.DenseIntegerNodes.separated_of_density line 257