Source indexedtheorem · leanprover/lean4:v4.32.0

analytic_deriv_bounded_near_point

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:206 to 219

Source documentation

From \texttt{riemannZeta_residue_one} (in Mathlib), we know that $(s-1)\zeta(s)$ goes to $1$ as $s\to1$ . Now apply Theorem \ref{ResidueOfTendsTo}. (This can also be done using $\zeta_0$ below, which is expressed as $1/(s-1)$ plus things that are holomorphic for $\Re(s)>0$ ...) -/)] theorem riemannZetaResidue : ∃ U ∈ 𝓝 1, BddAbove (norm ∘ (ζ - (fun s ↦ (s - 1)⁻¹)) '' (U \ {1})) := by have zeta_holc : HolomorphicOn ζ (univ \ {1}) := by intro y hy exact DifferentiableAt.differentiableWithinAt <| differentiableAt_riemannZeta hy.2 convert ResidueOfTendsTo univ_mem zeta_holc riemannZeta_residue_one using 6 simp

-- Main theorem: if functions agree on a punctured set, their derivatives agree there too theorem deriv_eqOn_of_eqOn_punctured (f g : ℂ → ℂ) (U : Set ℂ) (p : ℂ) (hU_open : IsOpen U) (h_eq : EqOn f g (U \ {p})) : EqOn (deriv f) (deriv g) (U \ {p}) := by intro x hx apply EventuallyEq.deriv_eq filter_upwards [IsOpen.mem_nhds (hU_open.sdiff isClosed_singleton) hx] with t ht using h_eq ht

/- New two theorems to be proven

Exact Lean statement

theorem analytic_deriv_bounded_near_point
    (f : ℂ → ℂ) {U : Set ℂ} {p : ℂ} (hU : IsOpen U) (hp : p ∈ U) (hf : HolomorphicOn f U) :
    (deriv f) =O[𝓝[≠] p] (1 : ℂ → ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem analytic_deriv_bounded_near_point    (f : ℂ → ℂ) {U : Set ℂ} {p : ℂ} (hU : IsOpen U) (hp : p ∈ U) (hf : HolomorphicOn f U) :    (deriv f) =O[𝓝[≠] p] (1 : ℂ → ℂ) := by  have U_in_filter : U ∈ 𝓝 p := by    exact IsOpen.mem_nhds hU hp  have T := (analyticOn_iff_differentiableOn hU).mpr hf  have T2 : ContDiffOn ℂ 1 f U :=      DifferentiableOn.contDiffOn hf hU  have T3 : ContinuousOn (fun x ↦ ((deriv f) x)) U := by    apply T2.continuousOn_deriv_of_isOpen hU (by simp)  have T4 := T3.continuousAt U_in_filter  have T5 : (deriv f) =O[𝓝 p] (1 : ℂ → ℂ) :=    T4.norm.isBoundedUnder_le.isBigO_one ℂ  exact Asymptotics.IsBigO.mono T5 inf_le_left