OAI/NumberTheory/Ostmann/Characters/HigherBiasSourceHalfMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.HigherBiasSource.sourceHalfMask line 13
2. lemma OAI.Ostmann.Characters.HigherBiasSource.sourceHalfMask_bounds line 16
3. lemma OAI.Ostmann.Characters.HigherBiasSource.sourceHalf_subsets line 22
4. theorem OAI.Ostmann.Characters.HigherBiasSource.sourceHalfMean_lower line 36