Source indexedlemma · leanprover/lean4:v4.32.0

tendsto_neg_div_two_pi_atTop_cocompact

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:361 to 373

Source documentation

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

Exact Lean statement

lemma tendsto_neg_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_neg_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 : ℝ => T / (2 * π)) Filter.atTop Filter.atTop := by    have h0 : 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    simpa [one_div, div_eq_mul_inv, mul_comm] using h0  have hn : Filter.Tendsto (fun T : ℝ => ‖T / (2 * π)‖) Filter.atTop Filter.atTop :=    tendsto_norm_atTop_atTop.comp h  simpa [dist_eq_norm, neg_div, norm_neg, norm_div,    abs_of_pos (by positivity : 0 < (2 * π : ℝ))] using hn