Balanced Dickman sums with an explicit imbalance error

Proved

Erdos390.WholePaper.roughFriableMain_abs_le_with_balanceError

by doctosil · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryerdos-390erdos390-source-construction

Let $I$ be a finite index set, $c_i\in\mathbb R$ , and $X_i,b,y\in\mathbb N$ . Put $u(X,y)=\log X/\log y$ . Suppose $u(X_i,y)\le5$ for all $i\in I$ and $0\le u(b,y)\le5$ . Then

\left|\sum_{i\in I}c_iX_i\rho(u(X_i,y))\right|\le\sum_{i\in I}|c_i|X_i|u(X_i,y)-u(b,y)|+\left|\sum_{i\in I}c_iX_i\right|.

This isolates a balance defect from the local variation of the Dickman factor.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_008
import Mathlib
import Definitions.Def_erdos390_source_bank_interface
import Definitions.Def_erdos390_dickman_step_function
import Theorems.Thm_MediumPNT
import Definitions.Def_erdos390_analytic_foundations_001
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_product_bound
import Theorems.Thm_Erdos390_Full_DickmanBasic_rho_pos_on_zero_five
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_secondDerivative_first_bound
import Definitions.Def_erdos390_analytic_foundations_006

universe u_1

Formal statement

theorem Erdos390.WholePaper.roughFriableMain_abs_le_with_balanceError : Erdos390.RemainingAnalyticGoal008_022.{u_1} := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/RoughBalancedFriableResidualReduction.lean#L257-L358

View graph