Count-free dyadic phase coercivity
Abstract
Count-free dyadic phase coercivity.
Theorem 1.1 (Count-free dyadic phase coercivity).
Lean statement: D5/S3/Analytic/Asymptotics/PhaseLawDyadicCoercivity.phase_law_dyadic_coercivity
Proof. Machine-checked in Lean as D5/S3/Analytic/Asymptotics/PhaseLawDyadicCoercivity.phase_law_dyadic_coercivity (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let I be any index type with nonnegative summable weights a(i) and positive frequencies gamma(i). Write delta(t)=sum 2a(i)(1-cos(gamma(i)t)). For fixed alpha>0, B>=0 and 0<T0<=exp(-1), assume the phase estimate abs(delta(t)-alphat^2log(1/t)^2)<=Bt^2*(log(1/t)+1) for every 0<t<=T0.
Put Kinv=2alpha+3B. For every Y>=16/T0, both strict and closed fourth moments are at most 64KinvY^2*(log(Y)+1), and both strict and closed tail masses are at most 32KinvY^(-2)*(log(Y)+1). No moment or tail estimate is assumed.
The exact defect 4delta(u/2)-delta(u) equals the nonnegative sum 4a(i)(1-cos(gamma(i)u/2))^2. Its upper bound Kinvu^2(log(1/u)+1) and the cosine remainder 5/96 force the fourth moment. For high frequencies average the squared kernel over [0,8/Y]. Its mean is at least 15/16. Integrate only finite high subsums under a constant majorant and then take their supremum. Thus no infinite sum-integral interchange or improper logarithmic antiderivative is needed. These bounds supply the Taylor split for phase inversion while preserving arbitrary early and repeated frequencies, zero weights, and infinite bounded-frequency clouds.