OAI/NumberTheory/DirichletL/Moments/FirstSeededGaussianPower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentFirstSeededGaussianPower.normalized_source_le_norm line 56
2. lemma OAI.SevenEighths.CenteredMomentFirstSeededGaussianPower.allocated_source_le_norm line 66
3. lemma OAI.SevenEighths.CenteredMomentFirstSeededGaussianPower.active_error_source_le_norm line 77
4. theorem OAI.SevenEighths.CenteredMomentFirstSeededGaussianPower.actual_subsets_seeded_gaussian_power line 90