PrimeNumberTheoremAnd

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

A removable analytic quotient for divisorCanonicalProduct m f univ z / (z - z₀)^k, where k is the divisor fiber cardinality at z₀. -/ 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]

/-!

Exact multiplicity of the divisor canonical product

At each z₀, the zero multiplicity of divisorCanonicalProduct equals the fiber cardinality card (divisorZeroIndex₀_fiberFinset z₀).

A removable analytic quotient for divisorCanonicalProduct m f univ z / (z - z₀)^k, where k is the divisor fiber cardinality at z₀. -/ 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]

/-!

Exact multiplicity of the divisor canonical product

At each z₀, the zero multiplicity of divisorCanonicalProduct equals the fiber cardinality card (divisorZeroIndex₀_fiberFinset z₀). -/

theorem analyticOrderNatAt_divisorCanonicalProduct_eq_fiber_card (m : ℕ) (f : ℂ → ℂ) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) => ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) (z₀ : ℂ) : analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z₀ = (divisorZeroIndex₀_fiberFinset (f := f) z₀).card := by set k : ℕ := (divisorZeroIndex₀_fiberFinset (f := f) z₀).card let F : ℂ → ℂ := divisorCanonicalProduct m f (Set.univ : Set ℂ) let q0 : ℂ → ℂ := fun z => F z / (z - z₀) ^ k rcases exists_analyticAt_divisorCanonicalProduct_quotient (m := m) (f := f) (h_sum := h_sum) (z₀ := z₀) with ⟨q, hqA, hq_self, hq_ne⟩ have hdiff_univ : DifferentiableOn ℂ F (Set.univ : Set ℂ) := differentiableOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum have han : AnalyticAt ℂ F z₀ := by refine (Complex.analyticAt_iff_eventually_differentiableAt).2 ?_ refine Filter.Eventually.of_forall ?_ intro z have : DifferentiableWithinAt ℂ F (Set.univ : Set ℂ) z := hdiff_univ z (by simp) exact this.differentiableAt (by simp) rcases exists_ball_eq_divisorCanonicalProduct_div_pow_eq (m := m) (f := f) (h_sum := h_sum) (z₀ := z₀) with ⟨ε, hε, u, huA, hu0, hEq⟩ let g : ℂ → ℂ := fun z => (divisorComplementCanonicalProduct m f z₀ z) * u z have hcompDiff : DifferentiableOn ℂ (divisorComplementCanonicalProduct m f z₀) (Set.univ : Set ℂ) := differentiableOn_divisorComplementCanonicalProduct_univ (m := m) (f := f) (z₀ := z₀) h_sum have hcompCont : ContinuousAt (divisorComplementCanonicalProduct m f z₀) z₀ := (hcompDiff z₀ (by simp)).differentiableAt (by simp) |>.continuousAt have hgCont : ContinuousAt g z₀ := (hcompCont.mul huA.continuousAt) have hg0 : g z₀ ≠ 0 := by have hcomp0 : divisorComplementCanonicalProduct m f z₀ z₀ ≠ 0 := divisorComplementCanonicalProduct_ne_zero_at (m := m) (f := f) (z₀ := z₀) h_sum exact mul_ne_zero hcomp0 hu0 have hne_mem : ∀ᶠ z in 𝓝[≠] z₀, z ∈ (({z₀} : Set ℂ)ᶜ) := Filter.eventually_of_mem (self_mem_nhdsWithin : (({z₀} : Set ℂ)ᶜ) ∈ 𝓝[≠] z₀) (fun _ hz => hz) have hne : ∀ᶠ z in 𝓝[≠] z₀, z ≠ z₀ := by filter_upwards [hne_mem] with z hz simpa [Set.mem_compl_singleton_iff] using hz have ht_q0 : Tendsto q0 (𝓝[≠] z₀) (𝓝 (g z₀)) := by have hball : ∀ᶠ z in 𝓝[≠] z₀, z ∈ Metric.ball z₀ ε := Filter.eventually_of_mem (mem_nhdsWithin_of_mem_nhds (Metric.ball_mem_nhds z₀ hε)) (fun _ hz => hz) have heq : q0 =ᶠ[𝓝[≠] z₀] g := by filter_upwards [hball, hne] with z hz hzne have hq := hEq z hz hzne simpa [q0, F, k, g, smul_eq_mul] using hq exact (hgCont.continuousWithinAt.tendsto.congr' heq.symm) have hlim : limUnder (𝓝[≠] z₀) q0 = g z₀ := ht_q0.limUnder_eq have hq0 : q z₀ ≠ 0 := by have hq_self' : q z₀ = limUnder (𝓝[≠] z₀) q0 := by simpa [q0, F, k] using hq_self have : q z₀ = g z₀ := hq_self'.trans hlim exact this.symm ▸ hg0 have heq_punct : (fun z : ℂ => F z) =ᶠ[𝓝[≠] z₀] fun z : ℂ => (z - z₀) ^ k • q z := by filter_upwards [hne] with z hz have hzpow : (z - z₀) ^ k ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hz) have hq : q z = q0 z := by simpa [q0, F, k] using hq_ne z hz have hmul : (z - z₀) ^ k * q0 z = F z := by calc (z - z₀) ^ k * q0 z = (((z - z₀) ^ k) * F z) / ((z - z₀) ^ k) := by simp [q0, div_eq_mul_inv, mul_assoc] _ = F z := by simpa [mul_assoc] using (mul_div_cancel_left₀ (F z) hzpow) have : F z = (z - z₀) ^ k * q z := by calc F z = (z - z₀) ^ k * q0 z := hmul.symm _ = (z - z₀) ^ k * q z := by simp [hq] simpa [smul_eq_mul] using this have hcontF : ContinuousAt F z₀ := (hdiff_univ z₀ (by simp)).differentiableAt (by simp) |>.continuousAt have hcontq : ContinuousAt q z₀ := hqA.continuousAt have h_at_z0 : F z₀ = (z₀ - z₀) ^ k • q z₀ := by have ht1 : Tendsto F (𝓝[≠] z₀) (𝓝 (F z₀)) := hcontF.continuousWithinAt.tendsto have hpow : Tendsto (fun z : ℂ => (z - z₀) ^ k) (𝓝[≠] z₀) (𝓝 ((z₀ - z₀) ^ k)) := ((continuousAt_id.sub continuousAt_const).pow k).continuousWithinAt.tendsto have ht2 : Tendsto (fun z : ℂ => (z - z₀) ^ k • q z) (𝓝[≠] z₀) (𝓝 ((z₀ - z₀) ^ k • q z₀)) := hpow.mul (hcontq.continuousWithinAt.tendsto) have ht2' : Tendsto F (𝓝[≠] z₀) (𝓝 ((z₀ - z₀) ^ k • q z₀)) := ht2.congr' heq_punct.symm exact tendsto_nhds_unique ht1 ht2' have hfac : ∀ᶠ z in 𝓝 z₀, F z = (z - z₀) ^ k • q z := by have hball1 : Metric.ball z₀ 1 ∈ 𝓝 z₀ := Metric.ball_mem_nhds z₀ (by norm_num) have hball1' : ∀ᶠ z in 𝓝 z₀, z ∈ Metric.ball z₀ 1 := Filter.eventually_of_mem hball1 (fun _ hz => hz) filter_upwards [hball1'] with z _hz by_cases hz0 : z = z₀ · subst hz0 simpa using h_at_z0 · have hzpow : (z - z₀) ^ k ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hz0) have hq : q z = q0 z := by simpa [q0, F, k] using hq_ne z hz0 have hmul : (z - z₀) ^ k * q0 z = F z := by calc (z - z₀) ^ k * q0 z = (((z - z₀) ^ k) * F z) / ((z - z₀) ^ k) := by simp [q0, div_eq_mul_inv, mul_assoc] _ = F z := by simpa [mul_assoc] using (mul_div_cancel_left₀ (F z) hzpow) have : F z = (z - z₀) ^ k * q z := by calc F z = (z - z₀) ^ k * q0 z := hmul.symm _ = (z - z₀) ^ k * q z := by simp [hq] simpa [smul_eq_mul] using this have hk' : analyticOrderAt F z₀ = k := (han.analyticOrderAt_eq_natCast (n := k)).2 ⟨q, hqA, hq0, hfac⟩ have hkNat : analyticOrderNatAt F z₀ = k := by simp [analyticOrderNatAt, hk'] simpa [F, k] using hkNat

/-!

Canonical product has the same analytic order as f away from the origin

Away from 0, the analytic order of the divisor-indexed canonical product agrees with that of f (for differentiable f), assuming the standard summability hypothesis.