OAI/NumberTheory/Ostmann/Characters/SourceTemplateNormInputs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.sourcePrimeShells_subset line 15
2. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.scheduled_sourcePrimeShells_subset line 24
3. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.configuration_chosenPrime_shell line 31
4. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.fixedConfiguration_chosenPrime_shell line 47
5. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.fixedConfiguration_scheduled_unit_norm line 55
6. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.fixedConfiguration_scheduled_nonprincipal line 63
7. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.fixedConfiguration_scheduled_shell_subset line 73
8. theorem OAI.Ostmann.Characters.HigherBiasSource.SourceTemplate.fixedConfiguration_scheduled_log_bounds line 80