OAI/Probability/SKGap/Localization/RealParameterIncrement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.ComplexMatrix.kChange line 12
2. lemma OAI.SKGap.ComplexMatrix.kChange_nonneg line 14
3. lemma OAI.SKGap.ComplexMatrix.kMixed_nonneg line 21
4. lemma OAI.SKGap.ComplexMatrix.truncatedK_parameter line 28
5. lemma OAI.SKGap.RealComplex.liftedSand_hermitian line 50
6. lemma OAI.SKGap.RealComplex.realTruncatedK_parameter line 53
7. lemma OAI.SKGap.RealComplex.realTruncatedK_four_point line 64
8. def OAI.SKGap.ComplexMatrix.parameterGC line 87
9. def OAI.SKGap.ComplexMatrix.parameterGM line 89
10. def OAI.SKGap.ComplexMatrix.parameterKC line 91
11. def OAI.SKGap.ComplexMatrix.parameterKM line 93
12. theorem OAI.SKGap.ComplexMatrix.cutoff_parameter_constants line 96