OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairKernelProductReplacementMatchedOriginalSamples.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.matchedReferenceSample line 24
2. def OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.RightRootSupported line 30
3. def OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.rightRootSupportIndicator line 36
4. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.rightRootSupportIndicator_bounds line 41
5. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.rightRootSupportIndicator_ne_zero_iff line 48
6. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.rightRootSupported_of_assignment line 55
7. theorem OAI.Ostmann.Arithmetic.HistoryPairKernelProductReplacement.matched_originalDrawMass_smallSourceSamples line 67