OAI/Probability/SignedSweeps/PermutationRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.finiteProb_real_kernel_apply line 12
2. lemma OAI.SignedSweeps.finiteMean_comm line 22
3. lemma OAI.SignedSweeps.finiteMean_mono line 29
4. def OAI.SignedSweeps.maskedPermutationKernel line 45
5. lemma OAI.SignedSweeps.maskedPermutationKernel_nonneg line 49
6. lemma OAI.SignedSweeps.maskedPermutationKernel_le line 57
7. lemma OAI.SignedSweeps.maskedPermutationKernel_transpose_sum line 64
8. theorem OAI.SignedSweeps.maskedPermutationKernel_square_row_le line 80
9. lemma OAI.SignedSweeps.nonnegative_kernel_restricted_row_le line 101