OAI/NumberTheory/DirichletL/Moments/FiniteProfileExceptionalPair.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.Profiles line 14
2. def OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.Profiles.control line 18
3. lemma OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.Profiles.control_nonneg line 21
4. def OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.ProfileAdmissible line 25
5. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.paired_amplitude_source_control line 33