RadialConstruction

Construction of radial admissible witnesses and sharp asymptotics.

theorem CohnElkies.tendsto_of_even_and_odd {X : Type u_1} [TopologicalSpace X] {f : ℕ → X} {x : X} (heven : Filter.Tendsto (fun (k : ℕ) => f (2 * k)) Filter.atTop (nhds x)) (hodd : Filter.Tendsto (fun (k : ℕ) => f (2 * k + 1)) Filter.atTop (nhds x)) : Filter.Tendsto f Filter.atTop (nhds x)

A sequence converges when its even and odd subsequences have the same limit.