OAI/Analysis/Cotype/RankWalsh.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.character_binary_sum line 13
2. def OAI.Cotype.blockCoordinates line 20
3. def OAI.Cotype.rankSubstitute line 23
4. theorem OAI.Cotype.rankSubstitute_bit line 26
5. theorem OAI.Cotype.rankSubstitute_character line 31
6. theorem OAI.Cotype.GrowthPairingData.coefficient_rank_walsh_bound line 78