OAI/NumberTheory/Ostmann/Characters/HigherBiasSourceTargetsBoundsBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.HigherBiasSourceTargets.coefficient line 9
2. def OAI.Ostmann.Characters.HigherBiasSourceTargets.pivotTarget line 11
3. def OAI.Ostmann.Characters.HigherBiasSourceTargets.fillerTarget line 14
4. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.coefficient_nonneg line 17
5. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.coefficient_le line 29
6. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.geometric_two_sum line 43
7. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.two_pow_square line 48
8. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.pivotTarget_total_le line 52
9. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.pivotTarget_lower line 69
10. lemma OAI.Ostmann.Characters.HigherBiasSourceTargets.cast_le_four_pow line 88