OAI/NumberTheory/DirichletL/Moments/AllocatedCenteredCapped.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentAllocatedCenteredCapped.plain_norm_le_reduction line 19
2. lemma OAI.SevenEighths.CenteredMomentAllocatedCenteredCapped.allocated_lower line 32
3. lemma OAI.SevenEighths.CenteredMomentAllocatedCenteredCapped.remaining_volume line 41
4. theorem OAI.SevenEighths.CenteredMomentAllocatedCenteredCapped.actual_allocated_capped_energy line 49