Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original ring centers and elevated corrections

Abstract

One initial degree controls every original ring center; elevated corrections have a uniform advantage.

Use the common-grid center C(tau,b,r,f,k), normalized Bernstein coefficients c(D,J,P), and endpoint scale delta of the imported Lorentz modules. The ring scale is s(j)=xstar*b^(-j/2). All centers retain the original Q initialization and residual recurrence. Complex-valued and signed inputs are allowed.

For r<rho<r+1 a threshold B at least 2 is chosen first. For each b at least B there is one positive K, independent of tau,f,c,M,A,H,s,k,J. Assume tau>0, r<=tau, f is C^r on [0,1], M,A,H are nonnegative, s>0, |f-c|<=M, derivatives of orders nu=1,…,r have modulus at most As^(-nu), and the top Holder seminorm is at most H. Every degree taub^k+r coefficient of C(tau,b,r,f,k), after subtracting c, has modulus at most M+KAsum(nu=1,…,r; tau^(-nu/2)s^(-nu))+KH*tau^(-rho/2). The initial derivative estimate uses nu/2, without claiming the sharper ceiling(nu/2) exponent.

Consequently, for any xstar>0, A,H>=0 and epsilon>0, one N at least 3*r+1 works for all rings j, inputs f, centers c, nonnegative M and stages k when the derivative and Holder bounds use s(j). Every center coefficient is within M+epsilon of c. This is a center margin, not a full envelope or cost theorem.

The same source module contains the consumed hypergeometric elevation interface. Its weight is choose(K,k)choose(N-K,n-k)/choose(N,n), its lift sums these weights against an array, its sample is k(K-k)/K^3, and its correction is theta/K^rho+sample^(rho/2), with natural subtraction in K-k. The finite-moment helpers retain the TauCeti source attribution and Apache license already specified in the Lean source. These auxiliaries organize existing identities; the common-center estimate supplies the substantive dependency.

Theorem 1.1 (Residual coefficient control).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.residual_coefficient_control

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.residual_coefficient_control (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

For rho>r there is K>0 uniform in n,b,f,P,A and J. If n>0, r<=nb, b>=1, A>=0 and every residual derivative through r is bounded by Adelta(n,x)^(rho-nu), then the degree nb+r coefficient of Q(nb,r,f-P) is bounded by KA(b*(r+1))^rhodelta(nb,J/(n*b+r))^rho.

Theorem 1.2 (Delta upper).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.delta_upper

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.delta_upper (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

For n>0 and x in [0,1], delta(n,x)<=n^(-1/2), including the reciprocal-degree endpoint floor.

Theorem 1.3 (Center coefficient control).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.center_coefficient_control

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.center_coefficient_control (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

The common coefficient estimate in the introduction holds for every stage and legal coefficient, using one K for each allowed refinement b.

Theorem 1.4 (Ring scale cancel).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.ring_scale_cancel

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.ring_scale_cancel (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

For N,b positive, xstar>0, every natural j and real e, (N*b^j)^(-e/2)*s(j)^(-e)=N^(-e/2)*xstar^(-e). This normalization is consumed by the uniform ring budgets.

Theorem 1.5 (Uniform ring center margin).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.uniform_ring_center_margin

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.uniform_ring_center_margin (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

A single initial N controls all ring indices, all admissible inputs and all stages with the stated M+epsilon margin.

Theorem 1.6 (Weight sum).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.weight_sum

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.weight_sum (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

When K<=N and n<=N, the sum of the hypergeometric weights for k=0,…,n equals one, including degenerate legal parameters.

Theorem 1.7 (Correction lift lower).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_lower

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_lower (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

For K<=N, n<=N, K>=2 and rho>=2, the elevated correction is at least theta/K^rho+[p*(1-p)/(2*K)]^(rho/2), where p=n/N. Theta is any real number.

Theorem 1.8 (Correction lift upper).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_upper

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_upper (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

For 0<K<=N<=2K, n<=N and rho>=0, the elevated correction is at most theta/K^rho+[4p*(1-p)/K]^(rho/2), where p=n/N. Theta is any real number.

Theorem 1.9 (Correction lift pos).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_pos

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_pos (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

For 0<K<=N, t<=N and theta>0, the elevated correction at t is strictly positive for every real rho.

Theorem 1.10 (Correction lift advantage).

Lean statement: D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_advantage

Proof. Machine-checked in Lean as D5/S3/Analytic/SeriesInequalities/OriginalRingEnvelopeScale.correction_lift_advantage (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Olga Holtz; Fedor Nazarov; Yuval Peres (2011). New Coins from Old, Smoothly. DOI: 10.1007/s00365-010-9108-5. URL: https://arxiv.org/abs/0808.1936v3.

Commentary.

If n>=2, m>=16*n, r<=m, t<=m+r, rho>=2 and theta>=0, twice the correction on degree m elevated to m+r is at most the degree-n correction elevated first to n+r and then to m+r. If theta>0, the new correction is strictly less than this twice-elevated old correction.

References