Prove2Me

Second ψ\psi-integral of [eq:psiints]: ∫Rψ2≤8L\int_{\mathbb{R}} \psi^2 \le 8L

Proved
Zeta23.Taper.integral_psi_sq_le

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

analysiszeta23

Let ϱ\varrho be a taper profile with constant cϱ:=4∥ϱ′∥∞+4∥ϱ′′∥1c_\varrho := 4\|\varrho'\|_\infty + 4\|\varrho''\|_1, and let ψ(r):=min⁡(L, 2/∣r∣, cϱ/(wr2))\psi(r) := \min\big(L,\ 2/|r|,\ c_\varrho/(w r^2)\big) (with ψ(0)=L\psi(0) = L) be the decay majorant of [eq:psidef] for support length LL and ramp width ww.

Assuming 1≤w1 \le w and 8w≤L8w \le L, the theorem asserts

∫Rψ(r)2 dr  ≤  8L.\int_{\mathbb{R}} \psi(r)^2\,dr \;\le\; 8L.

The proof uses only the two-term bound ψ≤min⁡(L, 2/∣r∣)\psi \le \min(L,\ 2/|r|): by evenness, ∫R=2∫0∞≤2(∫02/LL2+∫2/L∞4r−2)=2(2L+2L)\int_{\mathbb{R}} = 2\int_0^\infty \le 2\big(\int_0^{2/L} L^2 + \int_{2/L}^{\infty} 4 r^{-2}\big) = 2(2L + 2L).

In the project this is one of the ψ\psi-moments of [eq:psiints] consumed by Zeta23.PrimeSide.localHyps_concrete when verifying the concrete local hypotheses on the prime side of the second-moment computation.

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_sq_le (hϱ : TaperProfile ϱ) (hw : 1 ≤ w) (hwL : 8 * w ≤ L) :
    ∫ r, psi ϱ L w r ^ 2 ≤ 8 * L := by sorry
Source
https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/Taper/Decay.lean#L782-L845, docstring tag [eq:psiints]

View graph