OAI/NumberTheory/DirichletL/Moments/NaturalFixedRaySourceAllocatedErrorMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.naturalSlot_ideal_bound line 16
2. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.naturalSlot_height_bound line 44
3. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.natural_remaining_sq_bound line 56
4. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.allocated_profile_supnorm line 95
5. lemma OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.errorConstant_height line 105
6. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.allocated_natural_error_point line 116
7. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.allocated_natural_radial_error_mass line 148
8. theorem OAI.SevenEighths.CenteredMomentNaturalFixedRaySource.radialEnergy_le_absolute_mass line 194