OAI/NumberTheory/DirichletL/Energy/PositiveHighSource.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyPositiveHighSource.balancedInput line 37
2. lemma OAI.SevenEighths.CenteredMomentEnergyPositiveHighSource.balanced_matches line 48
3. lemma OAI.SevenEighths.CenteredMomentEnergyPositiveHighSource.balanced_volume line 53
4. lemma OAI.SevenEighths.CenteredMomentEnergyPositiveHighSource.balanced_volume_bound line 57
5. theorem OAI.SevenEighths.CenteredMomentEnergyPositiveHighSource.actual_positive_source_entry line 74