SaddleAnalysis

Saddle contours, Gaussian profiles, and source estimates.

Sign-indexed saddle data

The plus and minus saddle constructions differ only in their polynomial factor (plusPolynomial versus minusPolynomial). SaddleSign selects one of the two, and the dictionary below transports the facts both constructions share, so that the remaining analysis is carried out once for both signs.

theorem CohnElkies.tendsto_saddleResidue_dimension_half : Filter.Tendsto (fun (d : ℕ) => ↑d / 2) Filter.atTop Filter.atTop

The saddle residue dimension is asymptotic to half the ambient dimension.