OAI/NumberTheory/DirichletL/PrimeRows/CoarsePhysical.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.ProbeHighRowFamily.buffered_denominator_polynomial_growth line 13
2. def OAI.SevenEighths.ProbeHighRowFamily.coarsePrimeCost line 42
3. lemma OAI.SevenEighths.ProbeHighRowFamily.coarsePrimeCost_nonneg line 44
4. theorem OAI.SevenEighths.ProbeHighRowFamily.calibrated_physicalRow_buffered_polynomial_growth line 48
5. theorem OAI.SevenEighths.ProbeHighRowFamily.calibrated_physicalRow_first_joint_polynomial_growth line 107