OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairPolynomialKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.flags_polynomial_nonzero line 13
2. def OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.unitKernel line 26
3. def OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.mixedKernel line 33
4. def OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.NoAccidentalFlags line 40
5. theorem OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.polynomial_family_nonzero line 49
6. theorem OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.probability_eq_unitKernel line 58
7. theorem OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.probability_eq_mixedKernel line 68
8. theorem OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.unitKernel_bounds line 83
9. theorem OAI.Ostmann.Arithmetic.HistoryPairPolynomialKernel.mixedKernel_bounds line 89