OAI/NumberTheory/DirichletL/Moments/FirstPhysicalDyadicRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.activeRows line 17
2. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.mem_activeRows line 20
3. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.activeRows_subset line 24
4. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.activeRows_nonzero line 27
5. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.activeRows_norm line 31
6. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.activeRows_scale_gt_one line 37
7. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.activeRows_ball_majorant line 42
8. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.row_log_window line 47
9. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalDyadicRows.block_activeRows line 61