OAI/NumberTheory/ShortEgyptian/MomentDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ShortEgyptian.primeRecipBound_mono line 10
2. theorem OAI.ShortEgyptian.moment_band_nonpos line 20