OAI/Analysis/MatrixSigning/Complexity/PolynomialVariance.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_mgView line 14
2. instance OAI.CurrentKS.Realization.poly_mgN line 15
3. instance OAI.CurrentKS.Realization.poly_mgRest line 16
4. instance OAI.CurrentKS.Realization.poly_mgM line 17
5. instance OAI.CurrentKS.Realization.poly_mgDen line 18
6. instance OAI.CurrentKS.Realization.poly_mgShift line 19
7. instance OAI.CurrentKS.Realization.poly_mgTest line 20
8. instance OAI.CurrentKS.Realization.poly_gridStep line 21
9. lemma OAI.CurrentKS.Realization.gridStep_iterate_bounds line 28
10. instance OAI.CurrentKS.Realization.size_gridStep line 39
11. instance OAI.CurrentKS.Realization.poly_gridUpper line 54
12. instance OAI.CurrentKS.Realization.poly_fVariance line 55
13. lemma OAI.CurrentKS.Realization.isPoly_faceD line 57
14. lemma OAI.CurrentKS.Realization.isPoly_faceN line 61
15. lemma OAI.CurrentKS.Realization.varianceDen_ceil line 64
16. instance OAI.CurrentKS.Realization.poly_varianceDen line 68
17. instance OAI.CurrentKS.Realization.poly_fVarianceGrid line 80
18. instance OAI.CurrentKS.Realization.poly_varianceQuery line 81
19. instance OAI.CurrentKS.Realization.poly_faceNormalized line 82