Source indexedlemma · leanprover/lean4:v4.32.0

tendsto_div_two_pi_atTop_cocompact

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:347 to 358

Source documentation

The scaled positive-frequency ray T / (2π) tends to the cocompact filter.

Exact Lean statement

lemma tendsto_div_two_pi_atTop_cocompact :
    Filter.Tendsto (fun T : ℝ => T / (2 * π)) Filter.atTop (Filter.cocompact ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_div_two_pi_atTop_cocompact :    Filter.Tendsto (fun T : ℝ => T / (2 * π)) Filter.atTop (Filter.cocompact ℝ) := by  refine tendsto_cocompact_of_tendsto_dist_comp_atTop (0 : ℝ) ?_  have h : Filter.Tendsto (fun T : ℝ => (1 / (2 * π)) * T) Filter.atTop      Filter.atTop := by    exact (Filter.tendsto_const_mul_atTop_of_pos      (by positivity : 0 < (1 / (2 * π) : ℝ))).2 Filter.tendsto_id  have h' : Filter.Tendsto (fun T : ℝ => T / (2 * π)) Filter.atTop Filter.atTop := by    simpa [one_div, div_eq_mul_inv, mul_comm] using h  simpa [dist_eq_norm, Function.comp_def, norm_div,    abs_of_pos (by positivity : 0 < (2 * π : ℝ))]    using tendsto_norm_atTop_atTop.comp h'