OAI/Probability/GaussianInformation/Kernel/RowConcatenation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RowConcat.index line 11
2. def OAI.RowConcat.join line 13
3. lemma OAI.RowConcat.join_apply line 18
4. lemma OAI.RowConcat.join_bound line 26
5. lemma OAI.RowConcat.join_add line 34
6. lemma OAI.RowConcat.join_rows line 40
7. lemma OAI.RowConcat.join_measurePreserving line 47
8. lemma OAI.RowConcat.join_volume_measurePreserving line 54