OAI/NumberTheory/DirichletL/Reflection/FixedLevel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.reflectionSourceConductor line 11
2. lemma OAI.SevenEighths.InverseReflectedPhase.reflectionSourceConductor_span line 14
3. lemma OAI.SevenEighths.InverseReflectedPhase.reflectionSourceConductor_ne_zero line 18
4. def OAI.SevenEighths.InverseReflectedPhase.reflectionSourceLevel line 24
5. lemma OAI.SevenEighths.InverseReflectedPhase.reflectionSourceLevel_ne_zero line 26
6. lemma OAI.SevenEighths.InverseReflectedPhase.reflectionSourceGeometry_level line 29
7. lemma OAI.SevenEighths.InverseReflectedPhase.reflectionSourceLevel_original_period line 35
8. lemma OAI.SevenEighths.InverseReflectedPhase.reflectionSourceLevel_ray_finite line 41