OAI/NumberTheory/DirichletL/Energy/FirstSourceParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.sourceEpsilon line 18
2. def OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.maskEpsilon line 19
3. def OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.columnLoss line 20
4. lemma OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.source_cap_mono line 23
5. theorem OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.parameter_gates line 33
6. lemma OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.columnLoss_physical line 57
7. theorem OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.eventually_actual_four_fit line 63
8. theorem OAI.SevenEighths.CenteredMomentEnergyFirstSourceParameters.ready_budget_final line 97