OAI/NumberTheory/DirichletL/Moments/NaturalFixedRaySourceInternal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.internalQ line 15
2. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.internalQ_ne_zero line 17
3. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.internalQ_ne_top line 20
4. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.internalQ_coprime line 24
5. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.natural_nonzero_base line 28
6. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.coefficient_forcing_coprime line 33
7. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.energy_split line 38
8. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.internal_exceptional_count line 47
9. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.internal_sector_nonprincipal line 73