OAI/NumberTheory/DirichletL/Descent/FirstLiveCountBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.InverseMomentFirstOriginalProfile.liveNormCap_power_bound line 13
2. lemma OAI.SevenEighths.InverseMomentFirstOriginalProfile.dyadIndex_power_log_bound line 43
3. theorem OAI.SevenEighths.InverseMomentFirstOriginalProfile.live_joint_scalar_log_budget line 72
4. lemma OAI.SevenEighths.InverseMomentFirstOriginalProfile.log_eighth_small_power line 83
5. theorem OAI.SevenEighths.InverseMomentFirstOriginalProfile.live_joint_scalar_small_power line 106
6. theorem OAI.SevenEighths.InverseMomentFirstOriginalProfile.original_live_joint_small_power line 117