SourceFinitePhaseInterpolation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniformly in the finite phase count, the good-set small-imaginary vertex estimate suffices for the actual source family. The linear node envelope proves integrability and the large imaginary bound, Gaussian damping covers the remaining vertex tube, and the established analytic interpolation supplies the diagonal.

theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_diagonal_finite_phases_ae line 19