Three-dimensional adjacent-cell integration identity

Proved

Erdos390.WholePaper.BankPaperRealization.fourFiveMovingSimplexIteratedRealCellProductThree_eq_activePhysical

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

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

Let $A,Y,y\in\mathbb N$ satisfy $2\le y\le A\le Y$ , and let $u\in\mathbb R$ . Write $d(x)$ for the log-log Lebesgue density and $K_3(x,z,w)$ for the source real moving-simplex kernel with parameters $A,y,u$ . Then

\sum_{p,q,r=A+1}^{Y}\int_{p-1}^p\int_{q-1}^q\int_{r-1}^r d(x)d(z)d(w)K_3(x,z,w)\,dw\,dz\,dx=\int_A^Y\int_A^Y\int_A^Yd(x)d(z)d(w)K_3(x,z,w)\,dw\,dz\,dx.

The identity identifies the iterated cell-product model with the active physical integral.

Preamble

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_009

Formal statement

theorem Erdos390.WholePaper.BankPaperRealization.fourFiveMovingSimplexIteratedRealCellProductThree_eq_activePhysical :
∀ {A Y y : Nat} {u : Real},
  LE.le.{0} (2 : Nat) y →
    LE.le.{0} y A →
      LE.le.{0} A Y →
        Eq.{1} (Erdos390.WholePaper.BankPaperRealization.fourFiveMovingSimplexIteratedRealCellProductThree A Y y u)
          (Erdos390.WholePaper.BankPaperRealization.fourFiveMovingSimplexActivePhysicalIntegralThree A Y y u) := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperFourFiveMovingSimplexCellIdentification.lean#L2279-L2379

View graph