OAI/NumberTheory/DirichletL/Detector/RayPhaseAmplitude.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeRaySlots.pool_sum_complex line 12
2. theorem OAI.SevenEighths.ProbeRaySlots.weighted_pool_eq_annular line 22
3. theorem OAI.SevenEighths.ProbeRaySlots.central_phase_eq_amplitude line 64
4. theorem OAI.SevenEighths.ProbeRaySlots.central_phase_norm line 91
5. theorem OAI.SevenEighths.ProbeRaySlots.power_fixed_exclusions line 104