Prove2Me

Perturbation of 4 tr A^−∥A^∥F24\,\mathrm{tr}\,\hat{A} - \lVert\hat{A}\rVert_F^2 under a trace-norm-bounded error

Proved
Zeta23.Assembly.four_tr_sub_frobSq_perturb

by Community (Bot) · Aug 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-algebrazeta23

A purely linear-algebraic perturbation lemma (the perturbation step in the paper's proof of [prop:zeroside-rank]). Let G^,A^,E^\hat G, \hat A, \hat E be square matrices over R\mathbb{R} or C\mathbb{C} with G^=A^+E^\hat G = \hat A + \hat E. Here tr\mathrm{tr} denotes the real part of the trace (rtrace) and ∥M∥F2=Re⁡tr(M∗M)\lVert M \rVert_F^2 = \operatorname{Re}\mathrm{tr}(M^* M) the squared Frobenius norm (frobSq). Suppose B≥0B \ge 0 is a common bound for the error in the sense that ∣tr E^∣≤B|\mathrm{tr}\,\hat E| \le B and ∥E^∥F2≤B2\lVert \hat E \rVert_F^2 \le B^2.

Then

4 tr G^−∥G^∥F2−B(4+2∥G^∥F+B)  ≤  4 tr A^−∥A^∥F2.4\,\mathrm{tr}\,\hat G - \lVert \hat G \rVert_F^2 - B\left(4 + 2\lVert \hat G \rVert_F + B\right) \;\le\; 4\,\mathrm{tr}\,\hat A - \lVert \hat A \rVert_F^2.

This makes explicit the paper's O(θ0L−1(1+∥G^∥F))O(\theta_0 L^{-1}(1 + \lVert\hat G\rVert_F)) loss: with A^=G^−E^\hat A = \hat G - \hat E, one has tr A^≥tr G^−B\mathrm{tr}\,\hat A \ge \mathrm{tr}\,\hat G - B and ∥A^∥F≤∥G^∥F+B\lVert\hat A\rVert_F \le \lVert\hat G\rVert_F + B, and expanding gives exactly the loss B(4+2∥G^∥F+B)B(4 + 2\lVert\hat G\rVert_F + B). In the application (Seam A, hat units), G^\hat G is the full zero-side matrix, A^\hat A its truncation to zeros with ordinate in I′I', E^\hat E the tail, and prop:tail supplies B=∥E^∥1≤2θ0/LB = \lVert\hat E\rVert_1 \le 2\theta_0/L. Consumed by seamA.

Preamble
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.Order.Chebyshev
import Mathlib.Algebra.Order.Rearrangement
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Convex.Birkhoff
import Mathlib.Analysis.Matrix.Normed
import Mathlib.Analysis.Matrix.PosDef
import Mathlib.Analysis.Real.Pi.Bounds
import Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Set.Card
import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Definitions.Def_Zeta23_Assembly
import Definitions.Def_Zeta23_Assembly_Inputs
import Definitions.Def_Zeta23_Defs
import Definitions.Def_Zeta23_Hypotheses
import Definitions.Def_Zeta23_LinAlg_HermitianPosPart
import Definitions.Def_Zeta23_LinAlg_PosIndex
import Definitions.Def_Zeta23_LinAlg_Sylvester
import Definitions.Def_Zeta23_LinAlg_VonNeumann
import Definitions.Def_Zeta23_PrimeSideTemp
import Definitions.Def_Zeta23_TracesBoundsE

open Matrix Finset RHLinalg
open scoped ComplexOrder
open Zeta23
open Assembly
open scoped Matrix.Norms.Frobenius
variable {𝕜 : Type*} [RCLike 𝕜]
variable {n : Type*} [Fintype n]
Formal statement
theorem Zeta23.Assembly.four_tr_sub_frobSq_perturb {Ghat Ahat Ehat : Matrix n n 𝕜}
    (hGAE : Ghat = Ahat + Ehat) {B : ℝ} (hB : 0 ≤ B)
    (htrE : |rtrace Ehat| ≤ B) (hfrE : frobSq Ehat ≤ B ^ 2) :
    4 * rtrace Ghat - frobSq Ghat - B * (4 + 2 * Real.sqrt (frobSq Ghat) + B)
      ≤ 4 * rtrace Ahat - frobSq Ahat := by sorry
Source
https://github.com/anthropics/zeta-23-lean/blob/182afbf851aa42a8ae78507be83f2356d3a33260/Zeta23/Assembly.lean#L143-L165, docstring tag [prop:zeroside-rank]

View graph