OAI/NumberTheory/DirichletL/Moments/FirstPhysicalDyadicCountSource.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicCount.local_frequency_radius_cap line 16
2. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicCount.original_local_blocks_subpower line 35
3. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicCount.input_radius_cap line 55
4. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicCount.original_input_local_blocks_subpower line 79
5. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicCount.input_radius_pos_of_live line 97