OAI/Analysis/Cotype/ChebyshevTruncation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.chebyshevTruncation line 10
2. theorem OAI.Cotype.card_low_indices_le line 13
3. theorem OAI.Cotype.chebyshevTruncation_bound line 25
4. theorem OAI.Cotype.chebyshevRemainder_bound line 46