Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Many-low ordinary inverse on the arithmetic raw gauge

Proved
Erdos390.Full.ContinuumCellGraph.ArithmeticGaugeOrdinary.IntervalMesh.ordinary_split_arithmetic_projected_raw_bound_compact

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

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

Let a finite nonempty interval mesh be split into Low and nonempty High. Assume the covariance kernel product bound Cst, a positive interior quotient gap κ, positive high anchor mass A, high centers between a_min>0 and a_max≥0, low centers at most c₀≥0, and low and total lengths at most L₀,L≥0. Let positive arithmetic weights H_i and centers α_i≤α_max define the raw gauge. Assume the mixed low/high gauge ratio is bounded by g; low continuum diagonal error is at most d<1; continuum row residual is bounded by r≥0; arithmetic-versus-continuum raw row error is bounded by e‖b‖ with e≥0. With S=∑H_iα_i², assume α_max∑H_iα_i≤RS, R≥0, and α_max∑|H_iα_i−M.harmonicMass_i M.center_i|≤ρS with ρ≤1/2. Define ε=(r+Cc₀L)/(1−d), c=(1−d)⁻¹ and C₀=max(c,a_max[2(κA)⁻¹(a_min⁻¹+CL₀c)+gc]). Assume max(ε,a_max[2(κA)⁻¹(Cc₀L₀/a_min+CL₀ε)+gε])≤1/2 and 4C₀(1+R)(e+r)≤1/2. Then the projected arithmetic raw operator T satisfies the following bound. It is independent of the number and least center of the low cells.

∥b∥∞≤8C0∥Tb∥∞.\|b\|_\infty\le 8C_0\|Tb\|_\infty.∥b∥∞​≤8C0​∥Tb∥∞​.

This compact declaration is definitionally identical to the original fully quantified statement; the named proposition preserves every hypothesis.

Preamble
import Definitions.Def_erdos390_analytic_compact_goals

universe u_1 u_2 u_3
Formal statement
theorem Erdos390.Full.ContinuumCellGraph.ArithmeticGaugeOrdinary.IntervalMesh.ordinary_split_arithmetic_projected_raw_bound_compact : Erdos390.AnalyticCompactGoal001.{u_1, u_2, u_3} := by sorry
Source
https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/Full/ContinuumManyLowArithmeticGaugeOrdinary.lean#L192-L637

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me