Complex.Hadamard.eventually_exists_analyticAt_eq_pow_smul_divisorComplementPartialProduct
PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:309 to 345
Source documentation
At a nonzero divisor index, the canonical product has the same multiplicity as the original function. -/ theorem analyticOrderAt_divisorCanonicalProduct_at_index (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) => ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) : analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) (divisorZeroIndex₀_val p) = (analyticOrderNatAt f (divisorZeroIndex₀_val p) : ℕ∞) := by have horder := analyticOrderAt_divisorCanonicalProduct_eq_fiber_card (m := m) (f := f) (h_sum := h_sum) (z₀ := divisorZeroIndex₀_val p) have hfiber : (divisorZeroIndex₀_fiberFinset (f := f) (divisorZeroIndex₀_val p)).card = analyticOrderNatAt f (divisorZeroIndex₀_val p) := divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt (hf := hf) (z₀ := divisorZeroIndex₀_val p) p.property simpa [hfiber] using horder
/-!
Refining the factorization: factoring out (z - z₀)^k using the fiber-only product
When s contains the fiber finset, we can write the partial product as
divisorPartialProduct s = (z - z₀)^k • (divisorComplementPartialProduct s * u)
where u is the analytic quotient coming from the fiber-only product.
Exact Lean statement
theorem eventually_exists_analyticAt_eq_pow_smul_divisorComplementPartialProduct
(m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) :
∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _),
∃ u : ℂ → ℂ, AnalyticAt ℂ u z₀ ∧ u z₀ ≠ 0 ∧ (fun z : ℂ => divisorPartialProduct m f s z)
=ᶠ[𝓝 z₀] fun z : ℂ => (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card •
(divisorComplementPartialProduct m f z₀ s z * u z)Complete declaration
Lean source
theorem eventually_exists_analyticAt_eq_pow_smul_divisorComplementPartialProduct (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) : ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in (Filter.atTop : Filter _), ∃ u : ℂ → ℂ, AnalyticAt ℂ u z₀ ∧ u z₀ ≠ 0 ∧ (fun z : ℂ => divisorPartialProduct m f s z) =ᶠ[𝓝 z₀] fun z : ℂ => (z - z₀) ^ (divisorZeroIndex₀_fiberFinset (f := f) z₀).card • (divisorComplementPartialProduct m f z₀ s z * u z) := by let fiber : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := divisorZeroIndex₀_fiberFinset (f := f) z₀ have hfib : ∃ u : ℂ → ℂ, AnalyticAt ℂ u z₀ ∧ u z₀ ≠ 0 ∧ (fun z : ℂ => divisorPartialProduct m f fiber z) =ᶠ[𝓝 z₀] fun z : ℂ => (z - z₀) ^ fiber.card • u z := by simpa [fiber, divisorPartialProduct] using (exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber (m := m) (f := f) (z₀ := z₀) (s := fiber) (by rfl : fiber ⊆ fiber)) rcases hfib with ⟨u, huA, hu0, huEq⟩ refine (eventually_atTop_subset_fiberFinset (f := f) z₀).mono ?_ intro s hs refine ⟨u, huA, hu0, ?_⟩ have hmul : ∀ z : ℂ, divisorPartialProduct m f s z = divisorPartialProduct m f fiber z * divisorComplementPartialProduct m f z₀ s z := by intro z simpa [fiber] using (divisorPartialProduct_eq_fiber_mul_complement_of_subset (m := m) (f := f) (z₀ := z₀) (z := z) (s := s) hs) have hmul_ev : (fun z : ℂ => divisorPartialProduct m f s z) =ᶠ[𝓝 z₀] fun z : ℂ => ((z - z₀) ^ fiber.card • u z) * divisorComplementPartialProduct m f z₀ s z := by filter_upwards [huEq] with z hz have hsplit_z : divisorPartialProduct m f s z = divisorPartialProduct m f fiber z * divisorComplementPartialProduct m f z₀ s z := hmul z calc divisorPartialProduct m f s z = divisorPartialProduct m f fiber z * divisorComplementPartialProduct m f z₀ s z := hsplit_z _ = (((z - z₀) ^ fiber.card • u z) * divisorComplementPartialProduct m f z₀ s z) := by simpa [mul_assoc] using congrArg (fun t => t * divisorComplementPartialProduct m f z₀ s z) hz filter_upwards [hmul_ev] with z hz simpa [smul_eq_mul, mul_assoc, mul_left_comm, mul_comm, fiber] using hz