Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.exists_analyticAt_divisorCanonicalProduct_quotient

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientRemovable.lean:154 to 184

Source documentation

A removable analytic quotient for divisorCanonicalProduct m f univ z / (z - z₀)^k, where k is the divisor fiber cardinality at z₀.

Exact Lean statement

theorem exists_analyticAt_divisorCanonicalProduct_quotient
    (m : ℕ) (f : ℂ → ℂ)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))
    (z₀ : ℂ) :
    ∃ q : ℂ → ℂ,
      AnalyticAt ℂ q z₀ ∧
        q z₀ =
          limUnder (𝓝[≠] z₀) (fun z : ℂ =>
            (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /
              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card) ∧
        ∀ z : ℂ, z ≠ z₀ →
          q z =
            (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /
              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem exists_analyticAt_divisorCanonicalProduct_quotient    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) :    ∃ q : ℂ → ℂ,      AnalyticAt ℂ q z₀ ∧        q z₀ =          limUnder (𝓝[≠] z₀) (fun z : ℂ =>            (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card) ∧        ∀ z : ℂ, z ≠ z₀ →          q z =            (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /              (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card := by  let q : ℂ → ℂ :=    Function.update      (fun z : ℂ =>        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)      z₀      (limUnder (𝓝[≠] z₀) fun z : ℂ =>        (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) /          (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card)  refine ⟨q, ?_, ?_, ?_⟩  · simpa [q] using      analyticAt_update_limUnder_divisorCanonicalProduct_div_pow        (m := m) (f := f) (h_sum := h_sum) (z₀ := z₀)  · simp [q]  · intro z hz    simp [q, Function.update_of_ne hz]