FormalConjectures.OEIS.«102722»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Floor of sum of ${n/k}$

Given $n$, sum all division remainders ${n/k}$, with $k=1,\dots,n$. The value $a(n)$ is given by the floor of that sum. Note that ${x}:=x-[x]$. Conjecture: a(n) ~ (1-EulerGamma)n.

References:

A102722

namespace OeisA102722open BigOperators Finset Int Asymptotics Filter

The primary defining sequence a. a n is the floor of the sum of all division remainders ${n/k}$, with $k=1,\dots,n$. $$a(n) = \left\lfloor \sum_{k=1}^n \left{ \frac{n}{k} \right} \right\rfloor$$

noncomputable def a (n : ℕ) : ℕ :=
  let sumOfFractParts : ℝ :=
    (Icc 1 n).sum fun k : ℕ =>
      -- Int.fract is the fractional part function {x}.
      fract ((n : ℝ) / (k : ℝ))
  (floor sumOfFractParts).toNat



@[category API, AMS 11]
lemma a_sum_1 (f : ℕ → ℝ) : (Icc 1 1).sum f = f 1 := byf:ℕ → ℝ⊢ (Icc 1 1).sum f = f 1
  have h : Icc 1 1 = {1} := rflf:ℕ → ℝh:Icc 1 1 = {1}⊢ (Icc 1 1).sum f = f 1
  rw [h,f:ℕ → ℝh:Icc 1 1 = {1}⊢ {1}.sum f = f 1All goals completed! 🐙 Finset.sum_singletonf:ℕ → ℝh:Icc 1 1 = {1}⊢ f 1 = f 1All goals completed! 🐙]All goals completed! 🐙



@[category API, AMS 11]
lemma a_sum_2 (f : ℕ → ℝ) : (Icc 1 2).sum f = f 1 + f 2 := byf:ℕ → ℝ⊢ (Icc 1 2).sum f = f 1 + f 2
  have h : Icc 1 2 = {1, 2} := rflf:ℕ → ℝh:Icc 1 2 = {1, 2}⊢ (Icc 1 2).sum f = f 1 + f 2
  rw [h,f:ℕ → ℝh:Icc 1 2 = {1, 2}⊢ {1, 2}.sum f = f 1 + f 2All goals completed! 🐙 Finset.sum_insert (byf:ℕ → ℝh:Icc 1 2 = {1, 2}⊢ 1 ∉ {2}All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙), Finset.sum_singletonf:ℕ → ℝh:Icc 1 2 = {1, 2}⊢ f 1 + f 2 = f 1 + f 2All goals completed! 🐙]All goals completed! 🐙



@[category API, AMS 11]
lemma a_sum_3 (f : ℕ → ℝ) : (Icc 1 3).sum f = f 1 + f 2 + f 3 := byf:ℕ → ℝ⊢ (Icc 1 3).sum f = f 1 + f 2 + f 3
  have h : Icc 1 3 = {1, 2, 3} := rflf:ℕ → ℝh:Icc 1 3 = {1, 2, 3}⊢ (Icc 1 3).sum f = f 1 + f 2 + f 3
  rw [h,f:ℕ → ℝh:Icc 1 3 = {1, 2, 3}⊢ {1, 2, 3}.sum f = f 1 + f 2 + f 3All goals completed! 🐙 Finset.sum_insert (byf:ℕ → ℝh:Icc 1 3 = {1, 2, 3}⊢ 1 ∉ {2, 3}All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙), Finset.sum_insert (byf:ℕ → ℝh:Icc 1 3 = {1, 2, 3}⊢ 2 ∉ {3}All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙), Finset.sum_singleton,f:ℕ → ℝh:Icc 1 3 = {1, 2, 3}⊢ f 1 + (f 2 + f 3) = f 1 + f 2 + f 3All goals completed! 🐙
    add_assocf:ℕ → ℝh:Icc 1 3 = {1, 2, 3}⊢ f 1 + (f 2 + f 3) = f 1 + (f 2 + f 3)All goals completed! 🐙]All goals completed! 🐙



@[category API, AMS 11]
lemma a_sum_4 (f : ℕ → ℝ) : (Icc 1 4).sum f = f 1 + f 2 + f 3 + f 4 := byf:ℕ → ℝ⊢ (Icc 1 4).sum f = f 1 + f 2 + f 3 + f 4
  have h : Icc 1 4 = {1, 2, 3, 4} := rflf:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ (Icc 1 4).sum f = f 1 + f 2 + f 3 + f 4
  rw [h,f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ {1, 2, 3, 4}.sum f = f 1 + f 2 + f 3 + f 4f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4 Finset.sum_insert (byf:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ 1 ∉ {2, 3, 4}f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4), Finset.sum_insert (byf:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ 2 ∉ {3, 4}f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4),
    Finset.sum_insert (byf:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ 3 ∉ {4}f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4), Finset.sum_singletonf:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4]f:ℕ → ℝh:Icc 1 4 = {1, 2, 3, 4}⊢ f 1 + (f 2 + (f 3 + f 4)) = f 1 + f 2 + f 3 + f 4
  abelAll goals completed! 🐙



@[category API, AMS 11]
lemma a_sum_5 (f : ℕ → ℝ) : (Icc 1 5).sum f = f 1 + f 2 + f 3 + f 4 + f 5 := byf:ℕ → ℝ⊢ (Icc 1 5).sum f = f 1 + f 2 + f 3 + f 4 + f 5
  have h : Icc 1 5 = {1, 2, 3, 4, 5} := rflf:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ (Icc 1 5).sum f = f 1 + f 2 + f 3 + f 4 + f 5
  rw [h,f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ {1, 2, 3, 4, 5}.sum f = f 1 + f 2 + f 3 + f 4 + f 5f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5 Finset.sum_insert (byf:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ 1 ∉ {2, 3, 4, 5}f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5), Finset.sum_insert (byf:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ 2 ∉ {3, 4, 5}f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5),
    Finset.sum_insert (byf:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ 3 ∉ {4, 5}f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5), Finset.sum_insert (byf:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ 4 ∉ {5}f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5 decideAll goals completed! 🐙f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5), Finset.sum_singletonf:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5]f:ℕ → ℝh:Icc 1 5 = {1, 2, 3, 4, 5}⊢ f 1 + (f 2 + (f 3 + (f 4 + f 5))) = f 1 + f 2 + f 3 + f 4 + f 5
  abelAll goals completed! 🐙

macro "eval_a" : tactic => `(tactic| (
  delta a
  simp only [a_sum_1, a_sum_2, a_sum_3, a_sum_4, a_sum_5]
  norm_num
))

Term theorems verifying the first few values of the sequence against the official OEIS b-file

@[category test, AMS 11]
theorem a_1 : a 1 = 0 := by⊢ a 1 = 0 eval_aAll goals completed! 🐙

@[category test, AMS 11]
theorem a_2 : a 2 = 0 := by⊢ a 2 = 0 eval_aAll goals completed! 🐙

@[category test, AMS 11]
theorem a_3 : a 3 = 0 := by⊢ a 3 = 0 eval_aAll goals completed! 🐙

@[category test, AMS 11]
theorem a_4 : a 4 = 0 := by⊢ a 4 = 0 eval_aAll goals completed! 🐙

@[category test, AMS 11]
theorem a_5 : a 5 = 1 := by⊢ a 5 = 1 eval_aAll goals completed! 🐙

A102722 Conjecture: $a(n) \sim (1-\gamma)n$.

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://github.com/KitaKen1/oeis-102722-asymptotic/blob/0e3bf1bc6dfd04627f926b07fb8d25f4395a5072/lean/OEIS102722FC.lean#L18-L24"]
theorem conjecture :
    (fun n : ℕ => (a n : ℝ)) ~[atTop]
      (fun n : ℕ => (1 - Real.eulerMascheroniConstant) * (n : ℝ)) := by⊢ (fun n ↦ ↑(a n)) ~[atTop] fun n ↦ (1 - Real.eulerMascheroniConstant) * ↑n
  sorryAll goals completed! 🐙

end OeisA102722