OAI/NumberTheory/DirichletL/Moments/DetectorPlainExceptional.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentDetectorPlainExceptional.retainedSourceEnergy line 26
2. theorem OAI.SevenEighths.CenteredMomentDetectorPlainExceptional.retained_positive_energy_le_source line 33
3. theorem OAI.SevenEighths.CenteredMomentDetectorPlainExceptional.source_fibers_eventually_retained line 80
4. theorem OAI.SevenEighths.CenteredMomentDetectorPlainExceptional.source_exceptional_energy_eventually_zero line 109
5. theorem OAI.SevenEighths.CenteredMomentDetectorPlainExceptional.source_batch_plain_retained line 122