OAI/Analysis/Triangular/Signs/SineGridAnalytic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AtomicTriangular.Construction.realP line 10
2. lemma OAI.AtomicTriangular.Construction.P_ofReal line 11
3. lemma OAI.AtomicTriangular.Construction.realP_nonneg line 17
4. lemma OAI.AtomicTriangular.Construction.realP_periodic line 18
5. lemma OAI.AtomicTriangular.Construction.sin_abs_local line 25
6. lemma OAI.AtomicTriangular.Construction.abs_cell_le line 35
7. lemma OAI.AtomicTriangular.Construction.cell_factor_lower line 43
8. lemma OAI.AtomicTriangular.Construction.realP_cell_lower line 66