OAI.TotientAsymptotic.weighted_totient_asymptotic

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that, for every natural number k ≥ 1, the following hold, where V(x) counts the totient values v ≤ x, ell(v) is the least positive n with φ(n)=v (set to 0 if v is not a totient value), and N_k(x) counts totient values v ≤ x whose least preimage satisfies kx < ell(v) ≤ (k+1)x. Write f_k(r) = min(1,(k+1)/r) − min(1,k/r). First, the finite-H approximations AH_H(f_k), built from the renewal-type constants ρ and γ, tail-prime witness data and an inclusion-exclusion sum over sets of witnesses, converge uniformly on s in [0,1) as H → ∞ to the limit A(f_k)(s). Second, the count N_k(x), normalized by dividing by (x/log x)·G(x,m(x)), differs from A(f_k)(θ(x)) by an amount tending to 0 as x → ∞, where θ(x) is the fractional-part-like quantity ψ(log log x) − ⌊ψ(log log x)⌋. Third, if some totient value d satisfies k·d < ell(d), then there exist positive constants c₋ and c₊ with c₋ ≤ A(f_k)(s) ≤ c₊ for all s in [0,1), the ratio N_k(x)/((x/log x)·G(x,m(x))·A(f_k)(θ(x))) tends to 1, and eventually in x one has (c₋/c₊)·V(x) ≤ N_k(x) ≤ V(x). Fourth, if no totient value d satisfies k·d < ell(d), then N_k(x)=0 for every x>0 and A(f_k)(s)=0 for all s in [0,1).

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/TotientAsymptotic.lean; bytes 4349..5105
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_TotientAsymptotic

namespace OAI

noncomputable section

open scoped BigOperators Topology

open Filter

namespace TotientAsymptotic

Formal statement

theorem weighted_totient_asymptotic
    (k : ℕ) (hk : 1≤k) :
    TendstoUniformlyOn (fun H => AH H (fk k)) (A (fk k)) atTop (Set.Ico (0 : ℝ) 1) ∧
    Tendsto (fun x => normalizedCount (N k) x-A (fk k) (theta x)) atTop (nhds 0) ∧
    ((∃ d : ℕ, IsTotient d ∧ k*d<ell d) →
      ∃ cMinus cPlus : ℝ, 0<cMinus ∧ 0<cPlus ∧
        (∀ s∈Set.Ico (0 : ℝ) 1, cMinus≤A (fk k) s ∧ A (fk k) s≤cPlus) ∧
        Tendsto (fun x => N k x/(tupleNormalization x*A (fk k) (theta x))) atTop (nhds 1) ∧
        ∀ᶠ x : ℝ in atTop, (cMinus/cPlus)*V x≤N k x ∧ N k x≤V x) ∧
    ((¬∃ d : ℕ, IsTotient d ∧ k*d<ell d) →
      (∀ x : ℝ, 0<x → N k x=0) ∧ (∀ s∈Set.Ico (0 : ℝ) 1, A (fk k) s=0)) := by
  sorry

end TotientAsymptotic
end
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/TotientAsymptotic.lean

View graph