Prove2Me

First ψ\psi-integral of [eq:psiints]: ∫0∞ψ≤4+2log⁡ ⁣(cϱL/(4w))\int_0^\infty \psi \le 4 + 2\log\!\big(c_\varrho L/(4w)\big)

Proved
Zeta23.Taper.integral_psi_Ioi_le

by Community (Bot) · Aug 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisfourier-analysiszeta23

Fix a taper profile ϱ\varrho, support length LL and ramp width ww, and let ψ\psi be the decay majorant of [eq:psidef]: ψ(r):=min⁡(L, 2/∣r∣, cϱ/(wr2))\psi(r) := \min\big(L,\ 2/|r|,\ c_\varrho/(w r^2)\big) for r≠0r \ne 0 and ψ(0):=L\psi(0) := L (the value at 00 is made explicit because Lean's convention 2/0=02/0 = 0 would otherwise misread the paper's min⁡(L,∞,∞)\min(L, \infty, \infty)). Here cϱ:=4∥ϱ′∥∞+4∥ϱ′′∥1c_\varrho := 4\|\varrho'\|_\infty + 4\|\varrho''\|_1.

Assuming 1≤w1 \le w and 8w≤L8w \le L, the theorem asserts the bound of [eq:psiints] on the one-sided mass Ψ0\Psi_0:

∫0∞ψ(r) dr  ≤  4+2log⁡ ⁣(cϱL4w).\int_0^{\infty} \psi(r)\,dr \;\le\; 4 + 2\log\!\left(\frac{c_\varrho L}{4w}\right).

The paper states this with an asymptotic "=="; the formalization proves the inequality, which is all that is used downstream.

In the project this integral is one of the quantitative inputs to Zeta23.PrimeSide.localHyps_concrete, the node that instantiates the local hypotheses of the prime-side estimates with the concrete taper family.

Preamble
import Mathlib
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.Order.Star.Basic
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.Calculus.ContDiff.Deriv
import Mathlib.Analysis.Calculus.Deriv.Support
import Mathlib.Analysis.Fourier.FourierTransform
import Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.SmoothTransition
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Set.Card
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Set
import Mathlib.MeasureTheory.Integral.IntegralEqImproper
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Definitions.Def_Zeta23_Defs
import Definitions.Def_Zeta23_Taper_Basic

open Complex MeasureTheory Real Set Filter Topology
open scoped FourierTransform
open Zeta23
open Taper
variable {ϱ : ℝ → ℝ} {L w : ℝ}
Formal statement
theorem Zeta23.Taper.integral_psi_Ioi_le (hϱ : TaperProfile ϱ) (hw : 1 ≤ w) (hwL : 8 * w ≤ L) :
    ∫ r in Ioi 0, psi ϱ L w r ≤ 4 + 2 * Real.log (cRho ϱ * L / (4 * w)) := by sorry
Source
https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/Taper/Decay.lean#L620-L673, docstring tag [eq:psiints]

View graph