OAI/Combinatorics/SquareDifference/OrderedRates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.source_d_loss line 13
2. lemma OAI.SquareDifference.ordered_exponent_gaps line 21
3. lemma OAI.SquareDifference.cutoff_pow_upper line 43
4. lemma OAI.SquareDifference.cutoff_negative_upper line 50
5. def OAI.SquareDifference.orderedError line 55
6. def OAI.SquareDifference.orderedErrorConstant line 60
7. lemma OAI.SquareDifference.orderedError_bound line 63