OAI/NumberTheory/DirichletL/Moments/NaturalFixedRaySourceAllocatedProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.detectorPlain line 13
2. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.detectorPlain_profile_apply line 21
3. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.detectorPlain_profile_support line 34
4. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.detectorPlain_profile_seminorm line 47
5. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.detectorPlain_profile_uniform line 65
6. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.detectorPlain_volumeControl_uniform line 77
7. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.allocated_detector_profiles_uniform line 107