Source indexedlemma · leanprover/lean4:v4.32.0

IsBigO_to_BddAbove

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:661 to 678

Mathematical statement

Exact Lean statement

lemma IsBigO_to_BddAbove {f : ℂ → ℂ} {p : ℂ}
    (f_near_p : f =O[𝓝[≠] p] (1 : ℂ → ℂ)) :
    ∃ U ∈ 𝓝 p, BddAbove (norm ∘ f '' (U \ {p}))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma IsBigO_to_BddAbove {f : ℂ → ℂ} {p : ℂ}    (f_near_p : f =O[𝓝[≠] p] (1 : ℂ → ℂ)) :    ∃ U ∈ 𝓝 p, BddAbove (norm ∘ f '' (U \ {p})) := by  simp only [isBigO_iff, Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one] at f_near_p  obtain ⟨c, hc⟩ := f_near_p  dsimp [Filter.Eventually, nhdsWithin] at hc  rw [mem_inf_principal'] at hc  obtain ⟨U, hU, ⟨U_is_open, p_in_U⟩⟩ := mem_nhds_iff.mp hc  use U  constructor  · exact IsOpen.mem_nhds U_is_open p_in_U  · refine bddAbove_def.mpr ?_    use c    intro y hy    simp only [Function.comp_apply, mem_image, Set.mem_sdiff, mem_singleton_iff] at hy    obtain ⟨x, ⟨x_in_U, x_not_p⟩, fxy⟩ := hy    rw [← fxy]    simpa [x_not_p] using hU x_in_U