OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkPrincipalKernelReplacementMatchedFinite.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Arithmetic.HistoryBulkPrincipalKernelReplacementMatched.sampledJacobian_nonneg line 24
2. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalKernelReplacementMatched.weightedFlags line 30
3. lemma OAI.Ostmann.Arithmetic.HistoryBulkPrincipalKernelReplacementMatched.weightedFlags_nonneg line 38
4. lemma OAI.Ostmann.Arithmetic.HistoryBulkPrincipalKernelReplacementMatched.mean_eq_sum_weightedFlags line 46
5. lemma OAI.Ostmann.Arithmetic.HistoryBulkPrincipalKernelReplacementMatched.principalFlagMean_nonneg line 52
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalKernelReplacementMatched.principalDifferenceMean_le_of_pointwise line 58