OAI/LinearAlgebra/MatrixFields/Certificates/NativeSharp.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.capacityABalls line 141
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.capacityABalls_sound line 165
3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLABall line 212
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLABall_sound_0 line 213
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLABall_sound_1 line 218
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLABall_sound_2 line 223
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLABall_sound line 228
8. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_stageA_positive line 232
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.capacityBBalls line 236
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.capacityBBalls_sound line 260
11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLBBall line 307
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLBBall_sound_0 line 308
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLBBall_sound_1 line 313
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLBBall_sound_2 line 318
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeLBBall_sound line 323
16. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_stageB_positive line 327
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeCstarBall line 350
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeCstarBall_sound line 351
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeCBall line 363
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeCBall_sound line 364
21. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_stageC_feasible line 371
22. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_stageC_balanced_positive line 378
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeGapBall line 383
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.nativeGapBall_sound line 384
25. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_sharp_gap line 403
26. theorem OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.native_sharp_rate_bound line 408