OAI/NumberTheory/DirichletL/Energy/ZeroComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyZeroComparison.smallScale line 22
2. lemma OAI.SevenEighths.CenteredMomentEnergyZeroComparison.smallScale_pos line 24
3. lemma OAI.SevenEighths.CenteredMomentEnergyZeroComparison.smallScale_le_one line 26
4. lemma OAI.SevenEighths.CenteredMomentEnergyZeroComparison.smallScale_strict line 31
5. def OAI.SevenEighths.CenteredMomentEnergyZeroComparison.zeroData line 38
6. def OAI.SevenEighths.CenteredMomentEnergyZeroComparison.zeroInput line 45
7. lemma OAI.SevenEighths.CenteredMomentEnergyZeroComparison.zeroInput_volume line 50
8. lemma OAI.SevenEighths.CenteredMomentEnergyZeroComparison.comparison_row_zero line 54
9. lemma OAI.SevenEighths.CenteredMomentEnergyZeroComparison.comparison_energy_zero line 65
10. theorem OAI.SevenEighths.CenteredMomentEnergyZeroComparison.actual_zero_comparison_entry line 74
11. theorem OAI.SevenEighths.CenteredMomentEnergyZeroComparison.zero_comparison_scale_caps line 89