Complex.Hadamard.bddAbove_norm_divisorCanonicalProduct_div_pow_annulus

The Hadamard quotient is an entire zero-free function when the canonical product has the required convergence. The hypothesis hnot excludes the identically zero function, for which the discrete divisor/order bookkeeping used by Hadamard factorization is not the intended API. -/ theorem exists_entire_nonzero_hadamardQuotient (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hnot : ∃ z : ℂ, f z ≠ 0) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) => ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) : ∃ H : ℂ → ℂ, Differentiable ℂ H ∧ (∀ z, H z ≠ 0) ∧ ∀ z : ℂ, f z = H z * z ^ (analyticOrderNatAt f 0) * divisorCanonicalProduct m f (Set.univ : Set ℂ) z := by let denom : ℂ → ℂ := hadamardDenom m f let q : ℂ → ℂ := fun z => f z / denom z have hden_entire : Differentiable ℂ denom := differentiable_hadamardDenom (m := m) f h_sum have hq_mero : MeromorphicOn q (Set.univ : Set ℂ) := by intro z hzU have hf_m : MeromorphicAt f z := (hf.analyticAt z).meromorphicAt have hden_m : MeromorphicAt denom z := (hden_entire.analyticAt z).meromorphicAt simpa [q, denom, div_eq_mul_inv] using! (hf_m.mul hden_m.inv) let H : ℂ → ℂ := toMeromorphicNFOn q (Set.univ : Set ℂ) have hNF : MeromorphicNFOn H (Set.univ : Set ℂ) := meromorphicNFOn_toMeromorphicNFOn q (Set.univ : Set ℂ) have hdivH : MeromorphicOn.divisor H (Set.univ : Set ℂ) = 0 := by have hdivq : MeromorphicOn.divisor q (Set.univ : Set ℂ) = 0 := divisor_hadamardQuotient_eq_zero (m := m) (f := f) (hf := hf) (hnot := hnot) (h_sum := h_sum) simpa [H, hdivq] using (MeromorphicOn.divisor_of_toMeromorphicNFOn (f := q) (U := (Set.univ : Set ℂ)) hq_mero) have hA : AnalyticOnNhd ℂ H (Set.univ : Set ℂ) := by have : (0 : Function.locallyFinsuppWithin (Set.univ : Set ℂ) ℤ) ≤ MeromorphicOn.divisor H (Set.univ : Set ℂ) := by simp [hdivH] exact (MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd (h₁f := hNF)).1 (by simp [hdivH]) have hH_entire : Differentiable ℂ H := by intro z exact (hA z (by simp)).differentiableAt rcases hnot with ⟨z1, hz1⟩ have hden1 : denom z1 ≠ 0 := hadamardDenom_ne_zero_at (m := m) (f := f) hf ⟨z1, hz1⟩ h_sum hz1 have hqA1 : AnalyticAt ℂ q z1 := by have hdenA1 : AnalyticAt ℂ denom z1 := hden_entire.analyticAt z1 exact (hf.analyticAt z1).div hdenA1 hden1 have hqNF1 : MeromorphicNFAt q z1 := hqA1.meromorphicNFAt have htoEq : toMeromorphicNFAt q z1 = q := (toMeromorphicNFAt_eq_self (f := q) (x := z1)).2 hqNF1 have hH1 : H z1 = q z1 := by have hx : z1 ∈ (Set.univ : Set ℂ) := by simp have : toMeromorphicNFOn q (Set.univ : Set ℂ) z1 = toMeromorphicNFAt q z1 z1 := (toMeromorphicNFOn_eq_toMeromorphicNFAt (f := q) (U := (Set.univ : Set ℂ)) hq_mero hx) simpa [H, htoEq] using this have hH1_ne : H z1 ≠ 0 := by have : q z1 ≠ 0 := div_ne_zero hz1 hden1 simpa [hH1] using this have hH_not_top : ∀ z : ℂ, analyticOrderAt H z ≠ ⊤ := by exact analyticOrderAt_ne_top_of_exists_ne_zero (hf := hH_entire) ⟨z1, hH1_ne⟩ have hH_orderNat_zero : ∀ z : ℂ, analyticOrderNatAt H z = 0 := by intro z have hzdiv : (MeromorphicOn.divisor H (Set.univ : Set ℂ)) z = (analyticOrderNatAt H z : ℤ) := by simpa using (divisor_univ_eq_analyticOrderNatAt_int (f := H) hH_entire z) have : (MeromorphicOn.divisor H (Set.univ : Set ℂ)) z = 0 := by simp [hdivH] have : (analyticOrderNatAt H z : ℤ) = 0 := by simpa [hzdiv] using this exact_mod_cast this have hH_ne : ∀ z : ℂ, H z ≠ 0 := by intro z have hcast : (analyticOrderNatAt H z : ℕ∞) = analyticOrderAt H z := Nat.cast_analyticOrderNatAt (f := H) (z₀ := z) (hH_not_top z) have : analyticOrderAt H z = 0 := by have : (analyticOrderNatAt H z : ℕ∞) = 0 := by exact_mod_cast (hH_orderNat_zero z) simpa [hcast] using this exact ((hA z (by simp)).analyticOrderAt_eq_zero).1 this have hfA : AnalyticOnNhd ℂ f (Set.univ : Set ℂ) := fun z hzU => hf.analyticAt z have hdenA : AnalyticOnNhd ℂ denom (Set.univ : Set ℂ) := fun z hzU => hden_entire.analyticAt z have hprodA : AnalyticOnNhd ℂ (fun z => H z * denom z) (Set.univ : Set ℂ) := (hA.mul hdenA) have hlocal : f =ᶠ[𝓝 z1] fun z => H z * denom z := by have hden_ne : ∀ᶠ z in 𝓝 z1, denom z ≠ 0 := (hden_entire.differentiableAt.continuousAt.ne_iff_eventually_ne continuousAt_const).1 hden1 have hH_eq_q : H =ᶠ[𝓝 z1] q := by have hx : z1 ∈ (Set.univ : Set ℂ) := by simp have hloc : toMeromorphicNFOn q (Set.univ : Set ℂ) =ᶠ[𝓝 z1] toMeromorphicNFAt q z1 := by simpa [H] using (toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds (f := q) (U := (Set.univ : Set ℂ)) hq_mero hx) simpa [H, htoEq] using hloc filter_upwards [hden_ne, hH_eq_q] with z hzden hHz have hcancel : q z * denom z = f z := by dsimp [q] field_simp [hzden] calc f z = q z * denom z := hcancel.symm _ = H z * denom z := by simp [hHz] have hglob : f = fun z => H z * denom z := AnalyticOnNhd.eq_of_eventuallyEq (hf := hfA) (hg := hprodA) hlocal refine ⟨H, hH_entire, hH_ne, ?_⟩ intro z have hglobz : f z = H z * denom z := congrArg (fun g => g z) hglob simpa [denom, hadamardDenom, mul_assoc, mul_left_comm, mul_comm] using hglobz

/-!

Boundedness on compact annuli (away from z₀)

On any compact set separated from z₀, the quotient by (z - z₀)^k is bounded.