OAI/NumberTheory/DirichletL/Moments/AmplificationAllocationCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentAmplificationAllocationCost.allocation_slot_one line 15
2. theorem OAI.SevenEighths.CenteredMomentAmplificationAllocationCost.allocation_plain_product line 28
3. theorem OAI.SevenEighths.CenteredMomentAmplificationAllocationCost.allocation_plain_injective line 38
4. theorem OAI.SevenEighths.CenteredMomentAmplificationAllocationCost.idealDivisors_prime_power_card line 55
5. theorem OAI.SevenEighths.CenteredMomentAmplificationAllocationCost.actual_amplification_allocations_card line 64
6. theorem OAI.SevenEighths.CenteredMomentAmplificationAllocationCost.actual_error_allocations_card line 78