From b0d663530bb8be3ee84dae013af3d0286ef9b710 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 20 Aug 2024 09:14:54 +0200 Subject: [PATCH] Update analyticOn_zeroSet.lean --- Nevanlinna/analyticOn_zeroSet.lean | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean index fc8de57..87bb5ff 100644 --- a/Nevanlinna/analyticOn_zeroSet.lean +++ b/Nevanlinna/analyticOn_zeroSet.lean @@ -101,9 +101,9 @@ theorem AnalyticOn.order_eq_nat_iff' {A : Finset U} (hf : AnalyticOn ℂ f U) (n : ℂ → ℕ) : - (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a : A, g a ≠ 0) ∧ ∀ z, f z = (∏ a : A, (z - a) ^ (n a)) • g z := by + (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by - apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a : A, g a ≠ 0) ∧ ∀ z, f z = (∏ a : A, (z - a) ^ (n a)) • g z) + apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z) -- case empty simp @@ -115,3 +115,29 @@ theorem AnalyticOn.order_eq_nat_iff' intro b₀ B hb iHyp intro hBinsert obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha)) + + have : (h₁g₀ b₀ b₀.2).order = n b₀ := by sorry + obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this + + use g₁ + constructor + · exact h₁g₁ + · constructor + · intro a h₁a + by_cases h₂a : a = b₀ + · rwa [h₂a] + · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a + let B' := h₃g₁ a + let C' := h₂g₀ a A' + rw [B'] at C' + exact right_ne_zero_of_smul C' + · intro z + let A' := h₃g₀ z + rw [h₃g₁ z] at A' + rw [A'] + rw [← smul_assoc] + congr + simp + rw [Finset.prod_insert] + ring + exact hb