OAI/Analysis/Mahler/PlanarErrorRate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.planarErrorConstant line 9
2. lemma OAI.SymmetricMahler.planarErrorConstant_pos line 12
3. theorem OAI.SymmetricMahler.planarError_rate line 18

   Source documentation

   The explicit uniform error has inverse-square-root-log rate, with a constant independent of the point and the vertical section.

   theorem planarError_rate {m : ℝ} (hm : 3 ≤ m) :
       planarError m ≤ planarErrorConstant/sqrt (log m) := by
   …

   Mentions: OAI.SymmetricMahler.planarError, OAI.SymmetricMahler.planarErrorConstant

4. lemma OAI.SymmetricMahler.planarError_nat_tendsto_zero line 47