Compare commits

..

No commits in common. "b0d663530bb8be3ee84dae013af3d0286ef9b710" and "8a62e60b1584064ea814e58d61aec55946a6f234" have entirely different histories.

1 changed files with 79 additions and 34 deletions

View File

@ -100,44 +100,89 @@ theorem AnalyticOn.order_eq_nat_iff'
{U : Set } {U : Set }
{A : Finset U} {A : Finset U}
(hf : AnalyticOn f U) (hf : AnalyticOn f U)
(n : ) : (n : 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 := by ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a → ∃ (g : ), AnalyticOn g U ∧ (∀ a, g a ≠ 0) ∧ ∀ z, f z = (∏ 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
-- case empty let a : A := by sorry
simp let b : := by sorry
use f let u : U := by sorry
simp
exact hf
-- case insert let X := n a
intro b₀ B hb iHyp have : a = (3 : ) := by sorry
intro hBinsert have : b ∈ ↑A := by sorry
obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha)) have : ↑a ∈ U := by exact Subtype.coe_prop a.val
have : (h₁g₀ b₀ b₀.2).order = n b₀ := by sorry let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
use g₁ --∀ a : A, (hf (ha a)).order = ↑(n a) →
intro hn
obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
-- Define a candidate function
let g : := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
-- Describe g near z₀
have g_near_z₀ : ∀ᶠ (z : ) in nhds z₀, g z = gloc z := by
rw [eventually_nhds_iff]
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
use t
constructor constructor
· exact h₁g₁ · intro y h₁y
by_cases h₂y : y = z₀
· dsimp [g]; simp [h₂y]
· dsimp [g]; simp [h₂y]
rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
exact h₁t y h₁y
norm_num
rw [sub_eq_zero]
tauto
· constructor · constructor
· intro a h₁a · assumption
by_cases h₂a : a = b₀ · assumption
· rwa [h₂a]
· let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a -- Describe g near points z₁ different from z₀
let B' := h₃g₁ a have g_near_z₁ {z₁ : } : z₁ ≠ z₀ → ∀ᶠ (z : ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
let C' := h₂g₀ a A' intro hz₁
rw [B'] at C' rw [eventually_nhds_iff]
exact right_ne_zero_of_smul C' use {z₀}ᶜ
· intro z constructor
let A' := h₃g₀ z · intro y hy
rw [h₃g₁ z] at A' simp at hy
rw [A'] simp [g, hy]
rw [← smul_assoc] · exact ⟨isOpen_compl_singleton, hz₁⟩
congr
-- Use g and show that it has all required properties
use g
constructor
· -- AnalyticOn g U
intro z h₁z
by_cases h₂z : z = z₀
· rw [h₂z]
apply AnalyticAt.congr h₁gloc
exact Filter.EventuallyEq.symm g_near_z₀
· simp_rw [eq_comm] at g_near_z₁
apply AnalyticAt.congr _ (g_near_z₁ h₂z)
apply AnalyticAt.div
exact hf z h₁z
apply AnalyticAt.pow
apply AnalyticAt.sub
apply analyticAt_id
apply analyticAt_const
simp simp
rw [Finset.prod_insert] rw [sub_eq_zero]
ring tauto
exact hb · constructor
· simp [g]; tauto
· intro z
by_cases h₂z : z = z₀
· rw [h₂z, g_near_z₀.self_of_nhds]
exact h₃gloc.self_of_nhds
· rw [(g_near_z₁ h₂z).self_of_nhds]
simp [h₂z]
rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
simp; norm_num
rw [sub_eq_zero]
tauto