OAI/Analysis/MarkovType/HomogeneousRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.norm_row_sum_le_card line 20
2. theorem OAI.MarkovSuperreflexivity.abs_norm_row_sum_sub_le line 35
3. abbrev OAI.MarkovSuperreflexivity.RowCoefficientGrid line 55
4. abbrev OAI.MarkovSuperreflexivity.RowPalette line 57
5. def OAI.MarkovSuperreflexivity.boundedNormBin line 59
6. theorem OAI.MarkovSuperreflexivity.boundedNormBin_close line 65
7. theorem OAI.MarkovSuperreflexivity.exists_homogeneous_rows line 85