OAI/Combinatorics/SquareDifference/TransferRates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.source_exponent_gap_third line 13
2. lemma OAI.SquareDifference.eventual_cutoff_rpow_lower line 31
3. lemma OAI.SquareDifference.transfer_error_bound line 39
4. def OAI.SquareDifference.transferFactor line 74
5. lemma OAI.SquareDifference.transferFactor_nonneg line 77
6. lemma OAI.SquareDifference.transferFactor_limit line 79
7. lemma OAI.SquareDifference.child_factor_le line 89