OAI/NumberTheory/Ostmann/Characters/PrimeDyadicCoverSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.PrimeDyadicCover.sourceUpper line 11
2. theorem OAI.Ostmann.Characters.PrimeDyadicCover.sourceUpper_pos line 13
3. theorem OAI.Ostmann.Characters.PrimeDyadicCover.log_sourceUpper_le line 17
4. theorem OAI.Ostmann.Characters.PrimeDyadicCover.le_sourceUpper_of_log line 22
5. theorem OAI.Ostmann.Characters.PrimeDyadicCover.prime_shell_covers_of_le line 28
6. theorem OAI.Ostmann.Characters.PrimeDyadicCover.source_shell_covers line 35
7. theorem OAI.Ostmann.Characters.PrimeDyadicCover.source_shell_binary_cost_le_exp line 44
8. theorem OAI.Ostmann.Characters.PrimeDyadicCover.source_prime_binary_cost_le_exp line 58