OAI/NumberTheory/DirichletL/Detector/RayNormalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.ProbeRayNormalization.log_power_absorption line 13
2. theorem OAI.SevenEighths.ProbeRayNormalization.principalScalar_inverse_of_slot_bounds line 36
3. theorem OAI.SevenEighths.ProbeRayNormalization.ray_slot_subpower_lower line 70
4. theorem OAI.SevenEighths.ProbeRayNormalization.ray_principalScalar_inverse_subpower line 82