Eventual uniform Schur inverse and quadratic lower bound
ProvedErdos390.Full.PaperBridgeFit.BridgeData.eventually_exists_uniform_actualBandSchurEquiv_and_quadratic_compactWrite , , , and . Fix nonempty finite head and band sets, physical intervals with , , a cutoff , radius , and constants . Let satisfy . Eventually in , consider any bridge of size and cutoff with these physical endpoints and a barycentric target of cell-mass margin at least supplying its baseline. Suppose that throughout the effective ball its full projected operator is a continuous linear equivalence with inverse norm at most , every band center is at least , and every nuisance-valuation covariance is at most in absolute value. Set to the canonical nuisance gap for and the target, to the source nuisance marked Schur rate at , and . For every point in the ball, the actual band Schur operator is a linear equivalence, and
Here is the paper sharp norm, is the source raw diagonal lower weight, is total sharp weight, and is the full band-regression score.
The eventual threshold is uniform in all later bridges and inverse families, and the retained inverse constant is at most twice the full inverse constant.
This compact declaration is definitionally identical to the original fully quantified statement; the named proposition preserves every hypothesis.
import Definitions.Def_erdos390_analytic_compact_goals universe u_1 u_2
theorem Erdos390.Full.PaperBridgeFit.BridgeData.eventually_exists_uniform_actualBandSchurEquiv_and_quadratic_compact : Erdos390.AnalyticCompactGoal002.{u_1, u_2} := by sorry