claimroutineinferred_dep

Many heavy indices force approximation saving

Many heavy indices give saving −ν(A(1−η)−bˉ)-\nu(A(1-\eta)-\bar b); bounds log⁡∣ΔH∣/(MH)\log|\Delta_H|/(MH)
approximation case; yields the uniform upper bound
Claim·§3.4 A comparison with two alternatives·inside propDeterminant comparison with two savings

Statement (paper)

If more than (1−η)M(1-\eta)M of the indices satisfy wa>AHwa>AH, then ∑ρwaρ≥MHA(1−η)\sum_\rho wa_\rho\ge MHA(1-\eta), and after discarding the nonpositive collision term each row-term choice has normalized logarithm at most −ν(A(1−η)−bˉ)+Ean+ρH-\nu(A(1-\eta)-\bar b)+E_{\rm an}+\rho_H. Together with the first case, this gives, uniformly over the row-term choices, log⁡∣ΔH∣MH≤Ean+εH+max⁡{−cLH,−ν(A(1−η)−bˉ)}\frac{\log|\Delta_H|}{MH}\le E_{\rm an}+\varepsilon_H+\max\{-cL_H,-\nu(A(1-\eta)-\bar b)\}, where εH=ρH+log⁡QHH→0\varepsilon_H=\rho_H+\frac{\log Q_H}{H}\to0.

In plain English

If more than (1−η)M(1-\eta)M of the indices satisfy wa>AHwa>AH, then ∑ρwaρ≥MHA(1−η)\sum_\rho wa_\rho\ge MHA(1-\eta), and each row-term choice has normalized logarithm at most −ν(A(1−η)−bˉ)+Ean+ρH-\nu(A(1-\eta)-\bar b)+E_{\rm an}+\rho_H. Combined with the many-light-indices case, log⁡∣ΔH∣MH≤Ean+εH+max⁡{−cLH,−ν(A(1−η)−bˉ)}\frac{\log|\Delta_H|}{MH}\le E_{\rm an}+\varepsilon_H+\max\{-cL_H,-\nu(A(1-\eta)-\bar b)\} uniformly over row-term choices, where εH=ρH+log⁡QHH→0\varepsilon_H=\rho_H+\frac{\log Q_H}{H}\to0.

Why it's here

This is the second case of the dichotomy on term choices. When most indices are heavy, the scalar factors from the translation expansion give an exponential saving in ∑waρ\sum wa_\rho, so the collision term can be dropped as nonpositive. Together with the light-index case this bounds every term choice, and the factor QHMQ_H^M from the expansion is absorbed into εH\varepsilon_H, giving the single upper bound on log⁡∣ΔH∣\log|\Delta_H| for the comparison proposition.
Classified routine:
This follows by summing the weights of the heavy indices, dropping the nonpositive collision term, and combining the resulting bound with the earlier light-index case. The factor counting row-term choices is then absorbed into the stated error term.

Uses

claimSimplex counts calibrate expanded determinantclaimMany light indices force collisionslemRows reduce to entire-function rows

Used by

claimEither saving defeats arithmetic lower bound

Sources

PaperOpen
Section
§3.4 A comparison with two alternatives
Page
—
Label
—
Line
sections/determinant.tex:403
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Many heavy indices force approximation saving" rests on claim-det-comparison-1
  • info
    inferred_dep
    outline: "Many heavy indices force approximation saving" rests on claim-det-comparison-2
  • info
    inferred_dep
    outline: "Many heavy indices force approximation saving" rests on det:translation