OAI/NumberTheory/DirichletL/Reflection/RawTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.InverseReflectedPhase.RawTailIndex line 11
2. def OAI.SevenEighths.InverseReflectedPhase.rawTailWeight line 13
3. lemma OAI.SevenEighths.InverseReflectedPhase.rawTailWeight_nonneg line 16
4. lemma OAI.SevenEighths.InverseReflectedPhase.rawTailWeight_summable line 20
5. lemma OAI.SevenEighths.InverseReflectedPhase.tail_power_gain line 30
6. theorem OAI.SevenEighths.InverseReflectedPhase.raw_kernel_tail line 37