Logarithmic growth of the translation term count is sublinear
ProvedOAI.PiExponent.DeterminantContradiction.translationTermCount_log_div_tendsto_zeronumber-theoryopenai-pi-exponent-017
For any fixed natural exponent and positive real scale, the logarithm of the translation term count divided by H tends to zero as H tends to positive infinity.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData open scoped BigOperators Topology open Filter open OAI.PiExponent
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.translationTermCount_log_div_tendsto_zero
(m : ℕ) {v : ℝ} (hv : 0 < v) :
Tendsto (fun H : ℝ =>
Real.log (translationTermCount m v H : ℝ) / H) atTop (𝓝 0) := by sorrySource