Update analyticAt.lean

Nevanlinna/analyticAt.lean

@@ -3,12 +3,13 @@ import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Analytic.Linear
 
 
+
 theorem AnalyticAt.order_mul
   {f₁ f₂ : ℂ → ℂ}
   {z₀ : ℂ}
   (hf₁ : AnalyticAt ℂ f₁ z₀)
   (hf₂ : AnalyticAt ℂ f₂ z₀) :
-  (AnalyticAt.mul hf₁ hf₂).order = hf₁.order + hf₂.order := by
+  (hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
   by_cases h₂f₁ : hf₁.order = ⊤
   · simp [h₂f₁]
     rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
@@ -77,6 +78,22 @@ theorem AnalyticAt.order_eq_zero_iff
       · simp
 
 
+theorem AnalyticAt.order_pow
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  {n : ℕ}
+  (hf : AnalyticAt ℂ f z₀) :
+  (hf.pow n).order = n * hf.order := by
+
+  induction' n with n hn
+  · simp; rw [AnalyticAt.order_eq_zero_iff]; simp
+  · simp
+    simp_rw [add_mul, pow_add]
+    simp
+    rw [AnalyticAt.order_mul (hf.pow n) hf]
+    rw [hn]
+
+
 theorem AnalyticAt.supp_order_toNat
   {f : ℂ → ℂ}
   {z₀ : ℂ}
@@ -147,36 +164,36 @@ theorem AnalyticAt.order_comp_CLE
     rw [AnalyticAt.order_eq_nat_iff] at hn
     obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
     have A := eventually_nhds_comp_composition h₃g ℓ.continuous
-    simp only [Function.comp_apply] at A
+
-    have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by apply analyticAt_const
+    have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by
+      sorry
     rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
     simp
-    rw [AnalyticAt.order_mul]
+    have t₀ : AnalyticAt ℂ (fun z => (ℓ z - ℓ z₀) ^ n) z₀ := by
+      sorry
 
+    rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]
 
+    have t₁ : AnalyticAt ℂ (fun z => ℓ z - ℓ z₀) z₀ := by
+      sorry
+    have : t₁.order = (1 : ℕ) := by
+      rw [AnalyticAt.order_eq_nat_iff]
+      use (fun z ↦ ℓ 1)
+      simp
+      constructor
+      · exact analyticAt_const
+      · apply Filter.Eventually.of_forall
+        intro x
+        sorry
 
+    have : t₀.order = n := by
+      rw [AnalyticAt.order_pow t₁, this]
+      simp
 
-    --rw [hn, AnalyticAt.order_eq_nat_iff]
+    rw [this]
-    rw [AnalyticAt.order_eq_nat_iff] at hn
-    obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
-    use g ∘ ℓ
-    constructor
-    · exact h₁g.comp (ℓ.analyticAt z₀)
-    · constructor
-      · exact h₂g
-      · rw [eventually_nhds_iff]
-        rw [eventually_nhds_iff] at h₃g
-        obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₃g
-        use ℓ⁻¹' t
-        constructor
-        · intro y hy
-          simp
-          rw [h₁t (ℓ y) hy]
 
+    have : (comp h₁g (ContinuousLinearEquiv.analyticAt ℓ z₀)).order = 0 := by
+      rwa [AnalyticAt.order_eq_zero_iff]
+    rw [this]
 
-          sorry
+    simp
-        · constructor
-          · apply IsOpen.preimage
-            exact ContinuousLinearEquiv.continuous ℓ
-            exact h₂t
-          · exact h₃t