OAI/NumberTheory/DirichletL/Reflection/ShellDomains.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.reflectedNDyad line 12
2. def OAI.SevenEighths.InverseReflectedPhase.reflectedBDyad line 15
3. lemma OAI.SevenEighths.InverseReflectedPhase.reflectedNDyad_bounds line 18
4. lemma OAI.SevenEighths.InverseReflectedPhase.reflectedBDyad_bounds line 23
5. lemma OAI.SevenEighths.InverseReflectedPhase.double_sum_coe line 28
6. lemma OAI.SevenEighths.InverseReflectedPhase.sum_dual_mask line 35
7. theorem OAI.SevenEighths.InverseReflectedPhase.literalDyadicBlock_eq_filtered_source line 49