OAI/NumberTheory/DirichletL/Detector/DetectorMomentPrimeGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_physical_scale line 17
2. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_separation_eventually line 21
3. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_fixedBase_norm_one line 47
4. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_primeProfile_norm line 55
5. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_tuple_quotient line 72
6. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_live_disjoint line 81
7. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_live_denominator line 94
8. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_live_quotient_norm line 107
9. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_capacity_eventually line 121
10. theorem OAI.SevenEighths.ProbeHighRowFamily.sourceMoment_fiber_prime_geometry_eventually line 158