Source indexedtheorem · leanprover/lean4:v4.32.0

logDerivResidue'

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:312 to 413

Source documentation

We know that $f(s) = \frac{A}{s-p} + O(1)$ near $p$ , so we can write $f(s) = \left(f(s) - \frac{A}{s-p}\right) + \frac{A}{s-p}.$ The first term is bounded, say by $M$ , and the second term goes to $\infty$ as $s \to p$ . Therefore, there exists a neighborhood $V$ of $p$ such that for all $s \in V \setminus \{p\}$ , we have $f(s) \neq 0$ . -/)] theorem nonZeroOfBddAbove {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ} (U_in_nhds : U ∈ 𝓝 p) {A : ℂ} (A_ne_zero : A ≠ 0) (f_near_p : BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (U \ {p}))) : ∃ V ∈ 𝓝 p, IsOpen V ∧ ∀ s ∈ V \ {p}, f s ≠ 0 := by

-- Step 1: Rewrite f as the sum of two parts have h_decomp : ∀ s, f s = (f s - A * (s - p)⁻¹) + A * (s - p)⁻¹ := by intro s ring -- Get a bound for the first summand obtain ⟨M, hM⟩ := f_near_p -- Step 2: The second summand A * (s - p)⁻¹ goes to ∞ as s → p -- We need to find a neighborhood where |A * (s - p)⁻¹| > M + 1 have A_norm_pos : 0 < ‖A‖ := norm_pos_iff.mpr A_ne_zero -- Choose δ such that for |s - p| < δ, we have |A * (s - p)⁻¹| > M + 1 let δ := ‖A‖ / (‖M‖ + 1) have δ_pos : 0 < δ := by refine div_pos A_norm_pos (add_pos_of_nonneg_of_pos (norm_nonneg M) one_pos) -- Find an open neighborhood V contained in both U and the δ-ball around p obtain ⟨V, hV_open, hV_mem, hV_sub⟩ : ∃ V, IsOpen V ∧ p ∈ V ∧ V ⊆ U ∩ Metric.ball p δ := by -- rw [mem_nhds_iff] at U_in_nhds obtain ⟨W, hW_sub, hW_open, hW_mem⟩ := mem_nhds_iff.mp U_in_nhds let V := W ∩ Metric.ball p δ have VNp : V ∈ 𝓝 p := (𝓝 p).inter_mem (IsOpen.mem_nhds hW_open hW_mem) (Metric.ball_mem_nhds p δ_pos) exact ⟨V, IsOpen.inter hW_open Metric.isOpen_ball, mem_of_mem_nhds VNp, inter_subset_inter_left _ hW_sub⟩ use V, mem_nhds_iff.mpr ⟨V, subset_refl V, hV_open, hV_mem⟩, hV_open -- Show f ≠ 0 on V intro s hs have hs_in_U : s ∈ U := hV_sub hs.1 |>.1 have hs_near_p : dist s p < δ := hV_sub hs.1 |>.2 have hs_ne_p : s ≠ p := hs.2 -- Step 3: Therefore the sum of the two terms has large norm rw [h_decomp s] -- The first summand is bounded have bound_first : ‖f s - A * (s - p)⁻¹‖ ≤ M := by apply hM exact ⟨s, ⟨hs_in_U, hs_ne_p⟩, rfl⟩ -- The second summand has large norm have large_second : ‖M‖ + 1 < ‖A * (s - p)⁻¹‖ := by rw [norm_mul, norm_inv, ← div_eq_mul_inv] rw [lt_div_iff₀ (norm_pos_iff.mpr (sub_ne_zero.mpr hs_ne_p))] rw [mul_comm, ← lt_div_iff₀ (add_pos_of_nonneg_of_pos (norm_nonneg M) one_pos)] rw [dist_eq_norm_sub] at hs_near_p exact hs_near_p -- Step 4: Therefore the sum is nonzero near p by_contra h_zero -- If f s = 0, then the two summands are negatives of each other rw [add_eq_zero_iff_eq_neg] at h_zero rw [h_zero, norm_neg] at bound_first -- But this contradicts our bounds have : ‖M‖ + 1 < ‖M‖ := (lt_of_lt_of_le (lt_of_lt_of_le large_second bound_first) (Real.le_norm_self M)) norm_num at this

/- The set should be open so that f'(p) = O(1) for all p ∈ U

Exact Lean statement

theorem logDerivResidue' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ}
    (U_is_open : IsOpen U)
    (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0)
    (holc : HolomorphicOn f (U \ {p}))
    (U_in_nhds : U ∈ 𝓝 p) {A : ℂ} (A_ne_zero : A ≠ 0)
    (f_near_p : BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (U \ {p}))) :
    (deriv f * f⁻¹ + (fun s ↦ (s - p)⁻¹)) =O[𝓝[≠] p] (1 : ℂ → ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem logDerivResidue' {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ}    (U_is_open : IsOpen U)    (non_zero : ∀ x ∈ U \ {p}, f x ≠ 0)    (holc : HolomorphicOn f (U \ {p}))    (U_in_nhds : U ∈ 𝓝 p) {A : ℂ} (A_ne_zero : A ≠ 0)    (f_near_p : BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (U \ {p}))) :    (deriv f * f⁻¹ + (fun s ↦ (s - p)⁻¹)) =O[𝓝[≠] p] (1 : ℂ → ℂ) := by    have simpleHolo : HolomorphicOn (fun s ↦ A / (s - p)) (U \ {p}) := by    apply DifferentiableOn.mono (t := {p}ᶜ)    · apply DifferentiableOn.div      · exact differentiableOn_const _      · exact DifferentiableOn.sub differentiableOn_id (differentiableOn_const _)      · exact fun x hx => by rw [sub_ne_zero]; exact hx    · rintro s ⟨_, hs⟩ ; exact hs   have f_minus_pole_is_holomorphic : HolomorphicOn (f - (fun s ↦ A * (s - p)⁻¹)) (U \ {p}) := by    exact (DifferentiableOn.sub_iff_right holc).mpr simpleHolo   let ⟨g, ⟨g_is_holomorphic, g_is_f_minus_pole⟩⟩ := existsDifferentiableOn_of_bddAbove    U_in_nhds f_minus_pole_is_holomorphic f_near_p       /- TODO: Assert that the derivatives match too -/   let h := (fun _ ↦ A) + g * (fun (s : ℂ) ↦ (s - p))    have linear_is_holomorphic : HolomorphicOn (fun (s : ℂ ) ↦ (s - p)) U := by    exact DifferentiableOn.sub_const differentiableOn_id p   have h_is_holomorphic : HolomorphicOn h U := by    have T := DifferentiableOn.mul g_is_holomorphic linear_is_holomorphic    exact DifferentiableOn.const_add A T   have h_continuous : ContinuousOn h U :=    by exact DifferentiableOn.continuousOn h_is_holomorphic   have deriv_h_identity : ∀x ∈ (U \ {p}), (deriv h) x = f x + (deriv f x) * (x - p) := by    intro x x_in_u_not_p    have x_in_u : x ∈ U := by exact Set.mem_of_mem_sdiff x_in_u_not_p    have x_not_p : x ≠ p := by      exact ((Set.mem_sdiff x).mp x_in_u_not_p).2     have weird : U ∈ 𝓝 x := by      exact IsOpen.mem_nhds (U_is_open) (x_in_u)     rw [derivative_const_plus_product, ← g_is_f_minus_pole x_in_u_not_p,      ← deriv_eqOn_of_eqOn_punctured _ _ U p U_is_open g_is_f_minus_pole x_in_u_not_p,      deriv_f_minus_A_inv_sub_clean]    · simp only [Pi.sub_apply]      have := sub_ne_zero_of_ne x_not_p      field_simp      ring    · apply holc.differentiableAt      exact Filter.inter_mem weird <| compl_singleton_mem_nhds x_not_p    · exact x_not_p    · exact g_is_holomorphic.differentiableAt weird  have h_identity : ∀x ∈ (U \ {p}), h x = (f x) * (x - p)  := by    intro x x_in_u_not_p    have hyp_x_not_p : x ≠ p := by      exact ((Set.mem_sdiff x).mp x_in_u_not_p).2    simp only [h, Pi.add_apply, Pi.mul_apply]    rw [← g_is_f_minus_pole x_in_u_not_p]    simp only [Pi.sub_apply]    field [sub_ne_zero.mpr hyp_x_not_p]  have log_deriv_f_plus_pole_equal_log_deriv_h :      EqOn (deriv f * f⁻¹ + fun s ↦ (s - p)⁻¹) ((deriv h) * h⁻¹) (U \ {p}) := by    simp only [Set.mem_sdiff, mem_singleton_iff, ne_eq, and_imp, Function.comp_apply, Pi.sub_apply,      DifferentiableOn.sub_iff_right, differentiableOn_const, DifferentiableOn.fun_sub_iff_left,      holc] at *    intro x hyp_x    have x_not_p : x ≠ p := by      exact ((Set.mem_sdiff x).mp hyp_x).2    have x_in_u : x ∈ U := by exact Set.mem_of_mem_sdiff hyp_x    simp only [Pi.add_apply, Pi.mul_apply, Pi.inv_apply]    rw [deriv_h_identity _ x_in_u x_not_p, h_identity _ x_in_u x_not_p]     /- This is just an identity at this point -/    field [sub_ne_zero.mpr x_not_p, non_zero x (x_in_u) x_not_p]  have h_inv_bounded :      h⁻¹ =O[𝓝[≠] p] (1 : ℂ → ℂ) := by    have : ContinuousAt h⁻¹ p := by      apply ContinuousOn.continuousAt h_continuous U_in_nhds |>.inv₀      simp [h, A_ne_zero]    exact Asymptotics.IsBigO.mono (this.norm.isBoundedUnder_le.isBigO_one ℂ) inf_le_left   have h_deriv_bounded :        (deriv h) =O[𝓝[≠] p] (1 : ℂ → ℂ) :=          analytic_deriv_bounded_near_point h U_is_open            (by exact mem_of_mem_nhds U_in_nhds) h_is_holomorphic    have h_log_deriv_bounded :    ((deriv h) * h⁻¹) =O[𝓝[≠] p] (1 : ℂ → ℂ)  := by      have T := Asymptotics.IsBigO.mul h_deriv_bounded h_inv_bounded      exact IsBigO.of_const_mul_right T   have u_not_p_in_filter : U \ {p} ∈ 𝓝[≠] p := by    exact sdiff_mem_nhdsWithin_compl U_in_nhds {p}  have T := Set.EqOn.eventuallyEq_of_mem log_deriv_f_plus_pole_equal_log_deriv_h u_not_p_in_filter  exact EventuallyEq.trans_isBigO T h_log_deriv_bounded