OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairKernelReplacementBasic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.leftRows line 13
  2. def OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.rightRows line 17
  3. def OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.unitKernel line 21
  4. def OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.mixedKernel line 28
  5. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.unitKernel_old_prime line 35
  6. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.mixedKernel_old_prime line 39
  7. def OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.NoAccidentalFlags line 43
  8. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.minors_zero_iff line 48
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.probability_eq_unitKernel line 55
  10. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.probability_eq_mixedKernel line 70
  11. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.unit_probability_bounds line 89
  12. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.mixed_probability_bounds line 97
  13. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.unitKernel_bounds line 105
  14. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelReplacement.mixedKernel_bounds line 113