Rename file

Nevanlinna/analyticAt.lean

@@ -0,0 +1,226 @@
+import Mathlib.Analysis.Analytic.IsolatedZeros
+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₀) :
+  (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]
+    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁
+    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
+    use t
+    constructor
+    · intro y hy
+      rw [h₁t y hy]
+      ring
+    · exact ⟨h₂t, h₃t⟩
+  · by_cases h₂f₂ : hf₂.order = ⊤
+    · simp [h₂f₂]
+      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
+      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂
+      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
+      use t
+      constructor
+      · intro y hy
+        rw [h₁t y hy]
+        ring
+      · exact ⟨h₂t, h₃t⟩
+    · obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁))
+      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂))
+      rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add]
+      rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)]
+      use g₁ * g₂
+      constructor
+      · exact AnalyticAt.mul h₁g₁ h₁g₂
+      · constructor
+        · simp; tauto
+        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁
+          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂
+          rw [eventually_nhds_iff]
+          use t₁ ∩ t₂
+          constructor
+          · intro y hy
+            rw [h₁t₁ y hy.1, h₁t₂ y hy.2]
+            simp; ring
+          · constructor
+            · exact IsOpen.inter h₂t₁ h₂t₂
+            · exact Set.mem_inter h₃t₁ h₃t₂
+
+
+theorem AnalyticAt.order_eq_zero_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀) :
+  hf.order = 0 ↔ f z₀ ≠ 0 := by
+
+  have : (0 : ENat) = (0 : Nat) := by rfl
+  rw [this, AnalyticAt.order_eq_nat_iff hf 0]
+
+  constructor
+  · intro hz
+    obtain ⟨g, _, h₂g, h₃g⟩ := hz
+    simp at h₃g
+    rw [Filter.Eventually.self_of_nhds h₃g]
+    tauto
+  · intro hz
+    use f
+    constructor
+    · exact hf
+    · constructor
+      · exact hz
+      · 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₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀) :
+  hf.order.toNat ≠ 0 → f z₀ = 0 := by
+
+  contrapose
+  intro h₁f
+  simp [hf.order_eq_zero_iff.2 h₁f]
+
+
+theorem ContinuousLinearEquiv.analyticAt
+  (ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀
+
+
+theorem eventually_nhds_comp_composition
+  {f₁ f₂ ℓ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : ∀ᶠ (z : ℂ) in nhds (ℓ z₀), f₁ z = f₂ z)
+  (hℓ : Continuous ℓ) :
+  ∀ᶠ (z : ℂ) in nhds z₀, (f₁ ∘ ℓ) z = (f₂ ∘ ℓ) z := by
+  obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hf
+  apply eventually_nhds_iff.2
+  use ℓ⁻¹' t
+  constructor
+  · intro y hy
+    exact h₁t (ℓ y) hy
+  · constructor
+    · apply IsOpen.preimage
+      exact hℓ
+      exact h₂t
+    · exact h₃t
+
+
+theorem AnalyticAt.order_congr
+  {f₁ f₂ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf₁ : AnalyticAt ℂ f₁ z₀)
+  (hf : f₁ =ᶠ[nhds z₀] f₂) :
+  hf₁.order = (hf₁.congr hf).order := by
+
+  by_cases h₁f₁ : hf₁.order = ⊤
+  rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
+  rw [AnalyticAt.order_eq_top_iff] at h₁f₁
+  exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
+  --
+  let n := hf₁.order.toNat
+  have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
+  rw [hn, eq_comm, AnalyticAt.order_eq_nat_iff]
+  rw [AnalyticAt.order_eq_nat_iff] at hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
+  use g
+  constructor
+  · assumption
+  · constructor
+    · assumption
+    · exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
+
+
+theorem AnalyticAt.order_comp_CLE
+  (ℓ : ℂ ≃L[ℂ] ℂ)
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f (ℓ z₀)) :
+  hf.order = (hf.comp (ℓ.analyticAt z₀)).order := by
+
+  by_cases h₁f : hf.order = ⊤
+  · rw [h₁f]
+    rw [AnalyticAt.order_eq_top_iff] at h₁f
+    let A := eventually_nhds_comp_composition h₁f ℓ.continuous
+    simp at A
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
+
+    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by
+      apply analyticAt_const
+    have : this.order = ⊤ := by
+      rw [AnalyticAt.order_eq_top_iff]
+      simp
+    rw [this]
+  · let n := hf.order.toNat
+    have hn : hf.order = n := Eq.symm (ENat.coe_toNat h₁f)
+    rw [hn]
+    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
+
+    have t₁ : AnalyticAt ℂ (fun z => ℓ z - ℓ z₀) z₀ := by
+      apply AnalyticAt.sub
+      exact ContinuousLinearEquiv.analyticAt ℓ z₀
+      exact analyticAt_const
+    have t₀ : AnalyticAt ℂ (fun z => (ℓ z - ℓ z₀) ^ n) z₀ := by
+      exact pow t₁ n
+    have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by
+      apply AnalyticAt.mul
+      exact t₀
+      apply AnalyticAt.comp h₁g
+      exact ContinuousLinearEquiv.analyticAt ℓ z₀
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
+    simp
+
+    rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]
+
+    have : t₁.order = (1 : ℕ) := by
+      rw [AnalyticAt.order_eq_nat_iff]
+      use (fun _ ↦ ℓ 1)
+      simp
+      constructor
+      · exact analyticAt_const
+      · apply Filter.Eventually.of_forall
+        intro x
+        calc ℓ x - ℓ z₀
+        _ = ℓ (x - z₀) := by
+          exact Eq.symm (ContinuousLinearEquiv.map_sub ℓ x z₀)
+        _ = ℓ ((x - z₀) * 1) := by
+          simp
+        _ = (x - z₀) * ℓ 1 := by
+          rw [← smul_eq_mul, ← smul_eq_mul]
+          exact ContinuousLinearEquiv.map_smul ℓ (x - z₀) 1
+
+    have : t₀.order = n := by
+      rw [AnalyticAt.order_pow t₁, this]
+      simp
+
+    rw [this]
+
+    have : (comp h₁g (ContinuousLinearEquiv.analyticAt ℓ z₀)).order = 0 := by
+      rwa [AnalyticAt.order_eq_zero_iff]
+    rw [this]
+
+    simp

Nevanlinna/analyticOn_zeroSet.lean

@@ -1,21 +1,25 @@
 import Mathlib.Analysis.Analytic.Constructions
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Complex.Basic
+import Nevanlinna.analyticAt
+
+
+noncomputable def AnalyticOn.order
+  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
 
 
 theorem AnalyticOn.order_eq_nat_iff
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  {z₀ : ℂ}
+  {z₀ : U}
   (hf : AnalyticOn ℂ f U)
-  (hz₀ : z₀ ∈ U)
   (n : ℕ) :
-  (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
+  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
 
   constructor
   -- Direction →
   intro hn
-  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
+  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ z₀.2) n).1 hn
 
   -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the
   -- removable singularity removed
@@ -44,7 +48,7 @@ theorem AnalyticOn.order_eq_nat_iff
   have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
     intro hz₁
     rw [eventually_nhds_iff]
-    use {z₀}ᶜ
+    use {z₀.1}ᶜ
     constructor
     · intro y hy
       simp at hy
@@ -87,59 +91,20 @@ theorem AnalyticOn.order_eq_nat_iff
   -- direction ←
   intro h
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
+  dsimp [AnalyticOn.order]
   rw [AnalyticAt.order_eq_nat_iff]
   use g
-  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
+  exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
 
 
-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
-  by_cases h₂f₁ : hf₁.order = ⊤
-  · simp [h₂f₁]
-    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
-    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
-    use t
-    constructor
-    · intro y hy
-      rw [h₁t y hy]
-      ring
-    · exact ⟨h₂t, h₃t⟩
-  · by_cases h₂f₂ : hf₂.order = ⊤
-    · simp [h₂f₂]
-      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
-      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂
-      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
-      use t
-      constructor
-      · intro y hy
-        rw [h₁t y hy]
-        ring
-      · exact ⟨h₂t, h₃t⟩
-    · obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁))
-      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂))
-      rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add]
-      rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)]
-      use g₁ * g₂
-      constructor
-      · exact AnalyticAt.mul h₁g₁ h₁g₂
-      · constructor
-        · simp; tauto
-        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁
-          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂
-          rw [eventually_nhds_iff]
-          use t₁ ∩ t₂
-          constructor
-          · intro y hy
-            rw [h₁t₁ y hy.1, h₁t₂ y hy.2]
-            simp; ring
-          · constructor
-            · exact IsOpen.inter h₂t₁ h₂t₂
-            · exact Set.mem_inter h₃t₁ h₃t₂
+theorem AnalyticOn.support_of_order₁
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOn ℂ f U) :
+  Function.support hf.order = U.restrict f⁻¹' {0} := by
+  ext u
+  simp [AnalyticOn.order]
+  rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
 
 
 theorem AnalyticOn.eliminateZeros
@@ -147,8 +112,8 @@ theorem AnalyticOn.eliminateZeros
   {U : Set ℂ}
   {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
+  (n : U → ℕ) :
+  (∀ a ∈ A, hf.order a = 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)
 
@@ -167,7 +132,7 @@ theorem AnalyticOn.eliminateZeros
 
     rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
 
-    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
+    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a)
 
     have : f = fun z ↦ φ z * g₀ z := by
       funext z
@@ -208,8 +173,7 @@ theorem AnalyticOn.eliminateZeros
     rw [h₂φ]
     simp
 
-
-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
 
   use g₁
   constructor
@@ -259,14 +223,14 @@ theorem discreteZeros
   (hU : IsPreconnected U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
+  DiscreteTopology ((U.restrict f)⁻¹' {0}) := by
 
   simp_rw [← singletons_open_iff_discrete]
   simp_rw [Metric.isOpen_singleton_iff]
 
   intro z
 
-  let A := XX hU h₁f h₂f z.2.1
+  let A := XX hU h₁f h₂f z.1.2
   rw [eq_comm] at A
   rw [AnalyticAt.order_eq_nat_iff] at A
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
@@ -311,9 +275,9 @@ theorem discreteZeros
     _ < min ε₁ ε₂ := by assumption
     _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
 
-
   have F := h₂ε₂ y.1 h₂y
-  rw [y.2.2] at F
+  have : f y = 0 := by exact y.2
+  rw [this] at F
   simp at F
 
   have : g y.1 ≠ 0 := by
@@ -331,19 +295,19 @@ theorem finiteZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Set.Finite ↑(U ∩ f⁻¹' {0}) := by
+  Set.Finite (U.restrict f⁻¹' {0}) := by
 
-  have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
-    apply IsCompact.of_isClosed_subset h₂U
-    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
-    exact IsCompact.isClosed h₂U
+  have closedness : IsClosed (U.restrict f⁻¹' {0}) := by
+    apply IsClosed.preimage
+    apply continuousOn_iff_continuous_restrict.1
+    exact h₁f.continuousOn
     exact isClosed_singleton
-    exact Set.inter_subset_left
 
-  apply hinter.finite
-  apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
+  have : CompactSpace U := by
+    exact isCompact_iff_compactSpace.mp h₂U
+
+  apply (IsClosed.isCompact closedness).finite
   exact discreteZeros h₁U h₁f h₂f
-  rfl
 
 
 theorem AnalyticOnCompact.eliminateZeros
@@ -353,32 +317,20 @@ theorem AnalyticOnCompact.eliminateZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f a a.2).order.toNat) • g z := by
+  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
 
-  let ι : U → ℂ := Subtype.val
+  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
-  let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
-
-  have : A₁.Finite := by
-    apply Set.Finite.preimage
-    exact Set.injOn_subtype_val
-    exact finiteZeros h₁U h₂U h₁f h₂f
-  let A := this.toFinset
-
-  let n : ℂ → ℕ := by
-    intro z
-    by_cases hz : z ∈ U
-    · exact (h₁f z hz).order.toNat
-    · exact 0
+  let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat
 
   have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
     intro a _
-    dsimp [n]
-    simp
+    dsimp [n, AnalyticOn.order]
     rw [eq_comm]
     apply XX h₁U
     exact h₂f
 
+
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
   use g
   use A
@@ -386,11 +338,6 @@ theorem AnalyticOnCompact.eliminateZeros
   have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
     intro z
     rw [h₃g z]
-    congr
-    funext a
-    congr
-    dsimp [n]
-    simp [a.2]
 
   constructor
   · exact h₁g
@@ -400,15 +347,115 @@ theorem AnalyticOnCompact.eliminateZeros
       · exact h₂g ⟨z, h₁z⟩ h₂z
       · have : f z ≠ 0 := by
           by_contra C
-          have : ⟨z, h₁z⟩ ∈ ↑A₁ := by
-            dsimp [A₁, ι]
-            simp
-            exact C
           have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
             dsimp [A]
             simp
-            exact this
+            exact C
           tauto
         rw [inter z] at this
         exact right_ne_zero_of_smul this
     · exact inter
+
+
+theorem AnalyticOnCompact.eliminateZeros₂
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U)
+  (h₂U : IsCompact U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
+
+  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
+
+  let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat
+
+  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
+    intro a _
+    dsimp [n, AnalyticOn.order]
+    rw [eq_comm]
+    apply XX h₁U
+    exact h₂f
+
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
+  use g
+
+  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
+    intro z
+    rw [h₃g z]
+
+  constructor
+  · exact h₁g
+  · constructor
+    · intro z h₁z
+      by_cases h₂z : ⟨z, h₁z⟩  ∈ ↑A.toSet
+      · exact h₂g ⟨z, h₁z⟩ h₂z
+      · have : f z ≠ 0 := by
+          by_contra C
+          have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
+            dsimp [A]
+            simp
+            exact C
+          tauto
+        rw [inter z] at this
+        exact right_ne_zero_of_smul this
+    · exact h₃g
+
+
+theorem AnalyticOnCompact.eliminateZeros₁
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsPreconnected U)
+  (h₂U : IsCompact U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ u ∈ U, f u ≠ 0) :
+  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
+
+  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
+
+  let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat
+
+  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
+    intro a _
+    dsimp [n, AnalyticOn.order]
+    rw [eq_comm]
+    apply XX h₁U
+    exact h₂f
+
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
+  use g
+
+  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
+    intro z
+    rw [h₃g z]
+
+  constructor
+  · exact h₁g
+  · constructor
+    · intro z h₁z
+      by_cases h₂z : ⟨z, h₁z⟩  ∈ ↑A.toSet
+      · exact h₂g ⟨z, h₁z⟩ h₂z
+      · have : f z ≠ 0 := by
+          by_contra C
+          have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
+            dsimp [A]
+            simp
+            exact C
+          tauto
+        rw [inter z] at this
+        exact right_ne_zero_of_smul this
+    · intro z
+
+      let φ : U → ℂ := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat
+      have hφ : Function.mulSupport φ ⊆ A := by
+        intro x hx
+        simp [φ] at hx
+        have : (h₁f.order x).toNat ≠ 0 := by
+          by_contra C
+          rw [C] at hx
+          simp at hx
+        simp [A]
+        exact AnalyticAt.supp_order_toNat (h₁f x x.2) this
+      rw [finprod_eq_prod_of_mulSupport_subset φ hφ]
+      rw [inter z]
+      rfl

Nevanlinna/analyticOn_zeroSet2.lean

@@ -1,449 +0,0 @@
-import Mathlib.Analysis.Analytic.Constructions
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Mathlib.Analysis.Complex.Basic
-
-
-theorem AnalyticOn.order_eq_nat_iff
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticOn ℂ f U)
-  (hz₀ : z₀ ∈ U)
-  (n : ℕ) :
-  (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
-
-  constructor
-  -- Direction →
-  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; this is (f z) / (z - z₀) ^ n with the
-  -- removable singularity removed
-  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
-    · 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
-      · assumption
-      · assumption
-
-  -- Describe g near points z₁ that are different from z₀
-  have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
-    intro hz₁
-    rw [eventually_nhds_iff]
-    use {z₀}ᶜ
-    constructor
-    · intro y hy
-      simp at hy
-      simp [g, hy]
-    · exact ⟨isOpen_compl_singleton, hz₁⟩
-
-  -- 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
-      rw [sub_eq_zero]
-      tauto
-  · 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
-
-  -- direction ←
-  intro h
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
-  rw [AnalyticAt.order_eq_nat_iff]
-  use g
-  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
-
-
-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
-  by_cases h₂f₁ : hf₁.order = ⊤
-  · simp [h₂f₁]
-    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
-    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
-    use t
-    constructor
-    · intro y hy
-      rw [h₁t y hy]
-      ring
-    · exact ⟨h₂t, h₃t⟩
-  · by_cases h₂f₂ : hf₂.order = ⊤
-    · simp [h₂f₂]
-      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
-      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂
-      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
-      use t
-      constructor
-      · intro y hy
-        rw [h₁t y hy]
-        ring
-      · exact ⟨h₂t, h₃t⟩
-    · obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁))
-      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂))
-      rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add]
-      rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)]
-      use g₁ * g₂
-      constructor
-      · exact AnalyticAt.mul h₁g₁ h₁g₂
-      · constructor
-        · simp; tauto
-        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁
-          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂
-          rw [eventually_nhds_iff]
-          use t₁ ∩ t₂
-          constructor
-          · intro y hy
-            rw [h₁t₁ y hy.1, h₁t₂ y hy.2]
-            simp; ring
-          · constructor
-            · exact IsOpen.inter h₂t₁ h₂t₂
-            · exact Set.mem_inter h₃t₁ h₃t₂
-
-
-theorem AnalyticOn.eliminateZeros
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {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
-
-  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
-  use f
-  simp
-  exact hf
-
-  -- case insert
-  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
-
-    rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
-
-    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
-
-    have : f = fun z ↦ φ z * g₀ z := by
-      funext z
-      rw [h₃g₀ z]
-      rfl
-    simp_rw [this]
-
-    have h₁φ : AnalyticAt ℂ φ b₀ := by
-      dsimp [φ]
-      apply Finset.analyticAt_prod
-      intro b _
-      apply AnalyticAt.pow
-      apply AnalyticAt.sub
-      apply analyticAt_id ℂ
-      exact analyticAt_const
-
-    have h₂φ : h₁φ.order = (0 : ℕ) := by
-      rw [AnalyticAt.order_eq_nat_iff h₁φ 0]
-      use φ
-      constructor
-      · assumption
-      · constructor
-        · dsimp [φ]
-          push_neg
-          rw [Finset.prod_ne_zero_iff]
-          intro a ha
-          simp
-          have : ¬ (b₀.1 - a.1 = 0) := by
-            by_contra C
-            rw [sub_eq_zero] at C
-            rw [SetCoe.ext C] at hb
-            tauto
-          tauto
-        · simp
-
-    rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)]
-
-    rw [h₂φ]
-    simp
-
-
-  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
-
-
-theorem XX
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by
-
-  intro hu
-  apply ENat.coe_toNat
-  by_contra C
-  rw [(h₁f u hu).order_eq_top_iff] at C
-  rw [← (h₁f u hu).frequently_zero_iff_eventually_zero] at C
-  obtain ⟨u₁, h₁u₁, h₂u₁⟩ := h₂f
-  rw [(h₁f.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hu C) h₁u₁] at h₂u₁
-  tauto
-
-
-theorem discreteZeros
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by
-
-  simp_rw [← singletons_open_iff_discrete]
-  simp_rw [Metric.isOpen_singleton_iff]
-
-  intro z
-
-  let A := XX hU h₁f h₂f z.2.1
-  rw [eq_comm] at A
-  rw [AnalyticAt.order_eq_nat_iff] at A
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := A
-
-  rw [Metric.eventually_nhds_iff_ball] at h₃g
-  have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by
-    have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g
-    have : {0}ᶜ ∈ nhds (g z) := by
-      exact compl_singleton_mem_nhds_iff.mpr h₂g
-
-    let F := h₄g.preimage_mem_nhds this
-    rw [Metric.mem_nhds_iff] at F
-    obtain ⟨ε, h₁ε, h₂ε⟩ := F
-    use ε
-    constructor; exact h₁ε
-    intro y hy
-    let G := h₂ε hy
-    simp at G
-    exact G
-  obtain ⟨ε₁, h₁ε₁⟩ := this
-
-  obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
-  use min ε₁ ε₂
-  constructor
-  · have : 0 < min ε₁ ε₂ := by
-      rw [lt_min_iff]
-      exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
-    exact this
-
-  intro y
-  intro h₁y
-
-  have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by
-    simp
-    calc dist y z
-    _ < min ε₁ ε₂ := by assumption
-    _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
-
-  have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by
-    simp
-    calc dist y z
-    _ < min ε₁ ε₂ := by assumption
-    _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
-
-
-  have F := h₂ε₂ y.1 h₂y
-  rw [y.2.2] at F
-  simp at F
-
-  have : g y.1 ≠ 0 := by
-    exact h₁ε₁.2 y h₃y
-  simp [this] at F
-  ext
-  rw [sub_eq_zero] at F
-  tauto
-
-
-theorem finiteZeros
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U)
-  (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Set.Finite ↑(U ∩ f⁻¹' {0}) := by
-
-  have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
-    apply IsCompact.of_isClosed_subset h₂U
-    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
-    exact IsCompact.isClosed h₂U
-    exact isClosed_singleton
-    exact Set.inter_subset_left
-
-  apply hinter.finite
-  apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
-  exact discreteZeros h₁U h₁f h₂f
-  rfl
-
-
-theorem AnalyticOnCompact.eliminateZeros
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U)
-  (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f a a.2).order.toNat) • g z := by
-
-  let ι : U → ℂ := Subtype.val
-
-  let A₁ := ι⁻¹' (U ∩ f⁻¹' {0})
-
-  have : A₁.Finite := by
-    apply Set.Finite.preimage
-    exact Set.injOn_subtype_val
-    exact finiteZeros h₁U h₂U h₁f h₂f
-  let A := this.toFinset
-
-  let n : ℂ → ℕ := by
-    intro z
-    by_cases hz : z ∈ U
-    · exact (h₁f z hz).order.toNat
-    · exact 0
-
-  have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
-    intro a _
-    dsimp [n]
-    simp
-    rw [eq_comm]
-    apply XX h₁U
-    exact h₂f
-
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
-  use g
-  use A
-
-  have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
-    intro z
-    rw [h₃g z]
-    congr
-    funext a
-    congr
-    dsimp [n]
-    simp [a.2]
-
-  constructor
-  · exact h₁g
-  · constructor
-    · intro z h₁z
-      by_cases h₂z : ⟨z, h₁z⟩  ∈ ↑A.toSet
-      · exact h₂g ⟨z, h₁z⟩ h₂z
-      · have : f z ≠ 0 := by
-          by_contra C
-          have : ⟨z, h₁z⟩ ∈ ↑A₁ := by
-            dsimp [A₁, ι]
-            simp
-            exact C
-          have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by
-            dsimp [A]
-            simp
-            exact this
-          tauto
-        rw [inter z] at this
-        exact right_ne_zero_of_smul this
-    · exact inter
-
-
-noncomputable def AnalyticOn.order
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  ℂ → ℕ∞ := by
-  intro z
-  if hz : z ∈ U then
-    exact (hf z hz).order
-  else
-    exact 0
-
-
-theorem AnalyticOnCompact.eliminateZeros₁
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U)
-  (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
-  (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ u, (z - u) ^ (h₁f.order u).toNat) • g z := by
-
-  obtain ⟨g, A, h₁g, h₂g, h₃g⟩ := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
-
-  use g
-  constructor
-  · exact h₁g
-  · constructor
-    · exact h₂g
-    · intro z
-      rw [h₃g z]
-      congr
-
-      sorry

Nevanlinna/diffOpGrothendieck.lean

@@ -1,9 +0,0 @@
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
-
-/-
-
-Here we would like to define differential operators, following EGA 4-1, §20.
-This is work to be done in the future.
-
--/

Nevanlinna/holomorphicAt.lean

@@ -125,6 +125,23 @@ theorem HolomorphicAt.analyticAt
   exact IsOpen.mem_nhds h₁s h₂s
 
 
+theorem AnalyticAt.holomorphicAt
+  [CompleteSpace F]
+  {f : ℂ → F}
+  {x : ℂ} :
+  AnalyticAt ℂ f x → HolomorphicAt f x := by
+  intro hf
+  rw [HolomorphicAt_iff]
+  use {x : ℂ | AnalyticAt ℂ f x}
+  constructor
+  · exact isOpen_analyticAt ℂ f
+  · constructor
+    · simpa
+    · intro z hz
+      simp at hz
+      exact differentiableAt hz
+
+
 theorem HolomorphicAt.contDiffAt
   [CompleteSpace F]
   {f : ℂ → F}

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,172 +1,449 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
 
+open Real
+
+
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  (h₂f : f 0 ≠ 0)
-  (S : Finset ℕ)
-  (a : S → ℂ)
-  (ha : ∀ s, a s ∈ Metric.ball 0 1)
-  (F : ℂ → ℂ)
-  (h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z)
-  (h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0)
-  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s)) :
-  Real.log ‖f 0‖ = -∑ s, Real.log (‖a s‖⁻¹) + (2 * Real.pi)⁻¹ * ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖f (circleMap 0 1 x)‖ := by
+  (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1))
+  (h₂f : f 0 ≠ 0) :
+  log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
 
-  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by sorry
-  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := by sorry
-  have h₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1) := by sorry
-  have h₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by sorry
+  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
+    (convex_closedBall (0 : ℂ) 1).isPreconnected
 
-  let α := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
-  obtain ⟨g, A, h'₁g, h₂g, h₃g⟩ := α
-  have h₁g : ∀ z ∈ Metric.closedBall 0 1, HolomorphicAt F z := by sorry
+  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
+    isCompact_closedBall 0 1
 
+  have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
+    use 0; simp; exact h₂f
 
+  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
 
-  let logAbsF := fun w ↦ Real.log ‖F w‖
+  have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
+    intro z h₁z
+    apply AnalyticAt.holomorphicAt
+    exact h₁F z h₁z
 
-  have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
-    intro z hz
-    apply logabs_of_holomorphicAt_is_harmonic
-    apply h₁F z hz
-    exact h₂F z hz
+  let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖
 
-  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
-    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
-
-  have t₂ : ∀ s, f (a s) = 0 := by
-    intro s
-    rw [h₃F]
-    simp
-    right
-    apply Finset.prod_eq_zero_iff.2
-    use s
-    simp
-
-  let logAbsf := fun w ↦ Real.log ‖f w‖
-  have s₀ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
+  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
     intro z h₁z h₂z
-    dsimp [logAbsf]
-    rw [h₃F]
-    simp_rw [Complex.abs.map_mul]
-    rw [Complex.abs_prod]
+
+    conv =>
+      left
+      arg 1
+      rw [h₃F]
+      rw [smul_eq_mul]
+      rw [norm_mul]
+      rw [norm_prod]
+      left
+      arg 2
+      intro b
+      rw [norm_pow]
+    simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
     rw [Real.log_mul]
     rw [Real.log_prod]
-    rfl
-    intro s hs
-    simp
-    by_contra ha'
-    rw [ha'] at h₂z
-    exact h₂z (t₂ s)
+    conv =>
+      left
+      left
+      arg 2
+      intro s
+      rw [Real.log_pow]
+    dsimp [G]
+    abel
+
+    -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
+    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
+      intro s hs
+      simp at hs
+      simp
+      intro h₂s
+      rw [h₂s] at h₂z
+      tauto
+    exact this
+
+    -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
+    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
+      intro s hs
+      simp at hs
+      simp
+      intro h₂s
+      rw [h₂s] at h₂z
+      tauto
+    rw [Finset.prod_ne_zero_iff]
+    exact this
+
     -- Complex.abs (F z) ≠ 0
     simp
     exact h₂F z h₁z
-    -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
-    by_contra h'
-    obtain ⟨s, h's, h''⟩ := Finset.prod_eq_zero_iff.1 h'
-    simp at h''
-    rw [h''] at h₂z
-    let A := t₂ s
-    exact h₂z A
 
-  have s₁ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
-    intro z h₁z h₂z
-    rw [s₀ z h₁z]
+
+  have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
+
+    rw [intervalIntegral.integral_congr_ae]
+    rw [MeasureTheory.ae_iff]
+    apply Set.Countable.measure_zero
     simp
-    assumption
 
-  have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp
-  rw [s₁ 0 this h₂f] at t₁
+    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
+      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
+      intro a ha
+      simp at ha
+      simp
+      by_contra C
+      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
+        circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
+      exact ha.2 (decompose_f (circleMap 0 1 a) this C)
 
-  have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
-    rw [h₃F]
+    apply Set.Countable.mono t₀
+    apply Set.Countable.preimage_circleMap
+    apply Set.Finite.countable
+    let A := finiteZeros h₁U h₂U h₁f h'₂f
+
+    have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
+      ext z
+      simp
+      tauto
+    rw [this]
+    exact Set.Finite.image Subtype.val A
+    exact Ne.symm (zero_ne_one' ℝ)
+
+
+  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
+    = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
+        + ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
+    dsimp [G]
+    rw [intervalIntegral.integral_add]
+    rw [intervalIntegral.integral_finset_sum]
+    simp_rw [intervalIntegral.integral_const_mul]
+
+    --  ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset,
+    --  IntervalIntegrable (fun x => (h'₁f.order i).toNat *
+    --    log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
+    intro i _
+    apply IntervalIntegrable.const_mul
+    --simp at this
+    by_cases h₂i : ‖i.1‖ = 1
+    -- case pos
+    exact int'₂ h₂i
+    -- case neg
+    apply Continuous.intervalIntegrable
+    apply continuous_iff_continuousAt.2
+    intro x
+    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
+      rfl
+    rw [this]
+    apply ContinuousAt.comp
+    apply Real.continuousAt_log
     simp
-    constructor
-    · have : (circleMap 0 1 x) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
-      exact h₂F (circleMap 0 1 x) this
-    · by_contra h'
-      obtain ⟨s, _, h₂s⟩  := Finset.prod_eq_zero_iff.1 h'
-      have : circleMap 0 1 x = a s := by
-        rw [← sub_zero (circleMap 0 1 x)]
-        nth_rw 2 [← h₂s]
-        simp
-      let A := ha s
-      rw [← this] at A
-      simp at A
 
-  have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
-  simp_rw [s₁ (circleMap 0 1 _) this h₀] at t₁
-  rw [intervalIntegral.integral_sub] at t₁
-  rw [intervalIntegral.integral_finset_sum] at t₁
+    by_contra ha'
+    conv at h₂i =>
+      arg 1
+      rw [← ha']
+      rw [Complex.norm_eq_abs]
+      rw [abs_circleMap_zero 1 x]
+      simp
+    tauto
+    apply ContinuousAt.comp
+    apply Complex.continuous_abs.continuousAt
+    fun_prop
+    -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
+    apply Continuous.intervalIntegrable
+    apply continuous_iff_continuousAt.2
+    intro x
+    have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
+      rfl
+    rw [this]
+    apply ContinuousAt.comp
+    apply Real.continuousAt_log
+    simp [h₂F]
+    -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
+    apply ContinuousAt.comp
+    apply Complex.continuous_abs.continuousAt
+    apply ContinuousAt.comp
+    apply DifferentiableAt.continuousAt (𝕜 := ℂ )
+    apply HolomorphicAt.differentiableAt
+    simp [h'₁F]
+    -- ContinuousAt (fun x => circleMap 0 1 x) x
+    apply Continuous.continuousAt
+    apply continuous_circleMap
 
-  simp_rw [int₀ (ha _)] at t₁
-  simp at t₁
-  rw [t₁]
+    have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s)))
+      = ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
+      funext x
+      simp
+    rw [this]
+    apply IntervalIntegrable.sum
+    intro i _
+    apply IntervalIntegrable.const_mul
+    --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
+    --simp at this
+    by_cases h₂i : ‖i.1‖ = 1
+    -- case pos
+    exact int'₂ h₂i
+    -- case neg
+    --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
+    apply Continuous.intervalIntegrable
+    apply continuous_iff_continuousAt.2
+    intro x
+    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
+      rfl
+    rw [this]
+    apply ContinuousAt.comp
+    apply Real.continuousAt_log
+    simp
+
+    by_contra ha'
+    conv at h₂i =>
+      arg 1
+      rw [← ha']
+      rw [Complex.norm_eq_abs]
+      rw [abs_circleMap_zero 1 x]
+      simp
+    tauto
+    apply ContinuousAt.comp
+    apply Complex.continuous_abs.continuousAt
+    fun_prop
+
+  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
+    let logAbsF := fun w ↦ Real.log ‖F w‖
+    have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
+      intro z hz
+      apply logabs_of_holomorphicAt_is_harmonic
+      apply h'₁F z hz
+      exact h₂F z hz
+
+    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
+
+  simp_rw [← Complex.norm_eq_abs] at decompose_int_G
+  rw [t₁] at decompose_int_G
+
+  conv at decompose_int_G =>
+    right
+    right
+    arg 2
+    intro x
+    right
+    rw [int₃ x.2]
+  simp at decompose_int_G
+
+  rw [int_logAbs_f_eq_int_G]
+  rw [decompose_int_G]
+  rw [h₃F]
   simp
-  have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
-    ring_nf
-    simp [mul_inv_cancel₀ Real.pi_ne_zero]
+  have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
+    calc π⁻¹ * 2⁻¹ * (2 * π * l)
+    _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
+    _ = π⁻¹ * π * l := by ring
+    _ = (π⁻¹ * π) * l := by ring
+    _ = 1 * l := by
+      rw [inv_mul_cancel₀]
+      exact pi_ne_zero
+    _ = l := by simp
   rw [this]
+  rw [log_mul]
+  rw [log_prod]
   simp
-  rfl
-  -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
-  intro i _
-  apply Continuous.intervalIntegrable
-  apply continuous_iff_continuousAt.2
-  intro x
-  have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
-    rfl
-  rw [this]
-  apply ContinuousAt.comp
-  apply Real.continuousAt_log
+
+  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
   simp
-  by_contra ha'
-  let A := ha i
-  rw [← ha'] at A
+  simp
+  intro x ⟨h₁x, _⟩
+  simp
+
+  dsimp [AnalyticOn.order] at h₁x
+  simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
+  exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x
+
+  --
+  intro x hx
+  simp at hx
+  simp
+  intro h₁x
+  nth_rw 1 [← h₁x] at h₂f
+  tauto
+
+  --
+  rw [Finset.prod_ne_zero_iff]
+  intro x hx
+  simp at hx
+  simp
+  intro h₁x
+  nth_rw 1 [← h₁x] at h₂f
+  tauto
+
+  --
+  simp
+  apply h₂F
+  simp
+
+
+lemma const_mul_circleMap_zero
+  {R θ : ℝ} :
+  circleMap 0 R θ = R * circleMap 0 1 θ := by
+  rw [circleMap_zero, circleMap_zero]
+  simp
+
+
+theorem jensen
+  {R : ℝ}
+  (hR : 0 < R)
+  (f : ℂ → ℂ)
+  (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 R))
+  (h₂f : f 0 ≠ 0) :
+  log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
+
+
+  let ℓ : ℂ ≃L[ℂ] ℂ :=
+  {
+    toFun := fun x ↦ R * x
+    map_add' := fun x y => DistribSMul.smul_add R x y
+    map_smul' := fun m x => mul_smul_comm m (↑R) x
+    invFun := fun x ↦ R⁻¹ * x
+    left_inv := by
+      intro x
+      simp
+      rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one]
+      simp
+      exact ne_of_gt hR
+    right_inv := by
+      intro x
+      simp
+      rw [← mul_assoc, mul_inv_cancel₀, one_mul]
+      simp
+      exact ne_of_gt hR
+    continuous_toFun := continuous_const_smul R
+    continuous_invFun := continuous_const_smul R⁻¹
+  }
+
+
+  let F := f ∘ ℓ
+
+  have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
+    apply AnalyticOn.comp (t := Metric.closedBall 0 R)
+    exact h₁f
+    intro x _
+    apply ℓ.toContinuousLinearMap.analyticAt x
+
+    intro x hx
+    have : ℓ x = R * x := by rfl
+    rw [this]
+    simp
+    simp at hx
+    rw [abs_of_pos hR]
+    calc R * Complex.abs x
+    _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
+    _ = R := by simp
+
+  have h₂F : F 0 ≠ 0 := by
+    dsimp [F]
+    have : ℓ 0 = R * 0 := by rfl
+    rw [this]
+    simpa
+
+  let A := jensen_case_R_eq_one F h₁F h₂F
+
+  dsimp [F] at A
+  have {x : ℂ} : ℓ x = R * x := by rfl
+  repeat
+    simp_rw [this] at A
   simp at A
-  apply ContinuousAt.comp
-  apply Complex.continuous_abs.continuousAt
-  fun_prop
-  -- IntervalIntegrable (fun x => logAbsf (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
-  apply Continuous.intervalIntegrable
-  apply continuous_iff_continuousAt.2
+  simp
+  rw [A]
+  simp_rw [← const_mul_circleMap_zero]
+  simp
+
+  let e : (Metric.closedBall (0 : ℂ) 1) → (Metric.closedBall (0 : ℂ) R) := by
+    intro ⟨x, hx⟩
+    have hy : R • x ∈ Metric.closedBall (0 : ℂ) R := by
+      simp
+      simp at hx
+      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+      rw [← this]
+      norm_num
+      calc R * Complex.abs x
+      _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
+      _ = R := by simp
+    exact ⟨R • x, hy⟩
+
+  let e' : (Metric.closedBall (0 : ℂ) R) → (Metric.closedBall (0 : ℂ) 1) := by
+    intro ⟨x, hx⟩
+    have hy : R⁻¹ • x ∈ Metric.closedBall (0 : ℂ) 1 := by
+      simp
+      simp at hx
+      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+      rw [← this]
+      norm_num
+      calc R⁻¹ * Complex.abs x
+      _ ≤ R⁻¹ * R := by
+        apply mul_le_mul_of_nonneg_left hx
+        apply inv_nonneg.mpr
+        exact abs_eq_self.mp (id (Eq.symm this))
+      _ = 1 := by
+        apply inv_mul_cancel₀
+        exact Ne.symm (ne_of_lt hR)
+    exact ⟨R⁻¹ • x, hy⟩
+
+  apply finsum_eq_of_bijective e
+
+
+  apply Function.bijective_iff_has_inverse.mpr
+  use e'
+  constructor
+  · apply Function.leftInverse_iff_comp.mpr
+    funext x
+    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
+    conv =>
+      left
+      arg 1
+      rw [← smul_assoc, smul_eq_mul]
+      rw [inv_mul_cancel₀ (Ne.symm (ne_of_lt hR))]
+      rw [one_smul]
+  · apply Function.rightInverse_iff_comp.mpr
+    funext x
+    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
+    conv =>
+      left
+      arg 1
+      rw [← smul_assoc, smul_eq_mul]
+      rw [mul_inv_cancel₀ (Ne.symm (ne_of_lt hR))]
+      rw [one_smul]
+
   intro x
-  have : (fun x => logAbsf (circleMap 0 1 x)) = Real.log ∘ Complex.abs ∘ f ∘ (fun x ↦ circleMap 0 1 x) :=
-    rfl
-  rw [this]
-  apply ContinuousAt.comp
   simp
-  exact h₀
-  apply ContinuousAt.comp
-  apply Complex.continuous_abs.continuousAt
-  apply ContinuousAt.comp
-  apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1)
-  apply HolomorphicAt.contDiffAt
-  apply h₁f
+  by_cases hx : x = (0 : ℂ)
+  rw [hx]
   simp
-  let A := continuous_circleMap 0 1
-  apply A.continuousAt
-  -- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
-  apply Continuous.intervalIntegrable
-  apply continuous_finset_sum
-  intro i _
-  apply continuous_iff_continuousAt.2
-  intro x
-  have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=
-    rfl
-  rw [this]
-  apply ContinuousAt.comp
-  apply Real.continuousAt_log
+
+  rw [log_mul, log_mul, log_inv, log_inv]
+  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+  rw [← this]
   simp
-  by_contra ha'
-  let A := ha i
-  rw [← ha'] at A
-  simp at A
-  apply ContinuousAt.comp
-  apply Complex.continuous_abs.continuousAt
-  fun_prop
+  left
+  congr 1
+
+  dsimp [AnalyticOn.order]
+  rw [← AnalyticAt.order_comp_CLE ℓ]
+
+  --
+  simpa
+  --
+  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+  rw [← this]
+  apply inv_ne_zero
+  exact Ne.symm (ne_of_lt hR)
+  --
+  exact Ne.symm (ne_of_lt hR)
+  --
+  simp
+  constructor
+  · assumption
+  · exact Ne.symm (ne_of_lt hR)

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -1,287 +0,0 @@
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOn_zeroSet
-import Nevanlinna.harmonicAt_examples
-import Nevanlinna.harmonicAt_meanValue
-import Nevanlinna.specialFunctions_CircleIntegral_affine
-
-open Real
-
-
-noncomputable def Zeroset
-  {f : ℂ → ℂ}
-  {s : Set ℂ}
-  (hf : ∀ z ∈ s, HolomorphicAt f z) :
-  Set ℂ := by
-  exact f⁻¹' {0} ∩ s
-
-
-noncomputable def ZeroFinset
-  {f : ℂ → ℂ}
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  (h₂f : f 0 ≠ 0) :
-  Finset ℂ := by
-
-  let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
-  have hZ : Set.Finite Z := by
-    dsimp [Z]
-    rw [Set.inter_comm]
-    apply finiteZeros
-    -- Ball is preconnected
-    apply IsConnected.isPreconnected
-    apply Convex.isConnected
-    exact convex_closedBall 0 1
-    exact Set.nonempty_of_nonempty_subtype
-    --
-    exact isCompact_closedBall 0 1
-    --
-    intro x hx
-    have A := (h₁f x hx)
-    let B := HolomorphicAt_iff.1 A
-    obtain ⟨s, h₁s, h₂s, h₃s⟩ := B
-    apply DifferentiableOn.analyticAt (s := s)
-    intro z hz
-    apply DifferentiableAt.differentiableWithinAt
-    apply h₃s
-    exact hz
-    exact IsOpen.mem_nhds h₁s h₂s
-    --
-    use 0
-    constructor
-    · simp
-    · exact h₂f
-  exact hZ.toFinset
-
-
-lemma ZeroFinset_mem_iff
-  {f : ℂ → ℂ}
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  {h₂f : f 0 ≠ 0}
-  (z : ℂ) :
-  z ∈ ↑(ZeroFinset h₁f h₂f) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
-  dsimp [ZeroFinset]; simp
-  tauto
-
-
-noncomputable def order
-  {f : ℂ → ℂ}
-  {h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z}
-  {h₂f : f 0 ≠ 0} :
-  ZeroFinset h₁f h₂f → ℕ := by
-  intro i
-  let A := ((ZeroFinset_mem_iff h₁f i).1 i.2).1
-  let B := (h₁f i.1 A).analyticAt
-  exact B.order.toNat
-
-
-theorem jensen_case_R_eq_one
-  (f : ℂ → ℂ)
-  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
-  (h₂f : f 0 ≠ 0) :
-  log ‖f 0‖ = -∑ s : (ZeroFinset h₁f h₂f), order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
-
-  have F : ℂ → ℂ := by sorry
-  have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
-  have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
-  have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry
-
-  let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f h₂f, (order s) * log ‖z - s‖
-
-  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
-    intro z h₁z h₂z
-
-    conv =>
-      left
-      arg 1
-      rw [h₃F]
-      rw [norm_mul]
-      rw [norm_prod]
-      right
-      arg 2
-      intro b
-      rw [norm_pow]
-    simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
-    rw [Real.log_mul]
-    rw [Real.log_prod]
-    conv =>
-      left
-      right
-      arg 2
-      intro s
-      rw [Real.log_pow]
-    dsimp [G]
-
-    -- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0
-    simp
-    intro s hs
-    rw [ZeroFinset_mem_iff h₁f s] at hs
-    rw [← hs.2] at h₂z
-    tauto
-
-    -- Complex.abs (F z) ≠ 0
-    simp
-    exact h₂F z h₁z
-
-    -- ∏ I : { x // x ∈ S }, Complex.abs (z - a I) ≠ 0
-    by_contra C
-    obtain ⟨s, h₁s, h₂s⟩ := Finset.prod_eq_zero_iff.1 C
-    simp at h₂s
-    rw [← ((ZeroFinset_mem_iff h₁f s).1 (Finset.coe_mem s)).2, h₂s.1] at h₂z
-    tauto
-
-  have : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
-
-    rw [intervalIntegral.integral_congr_ae]
-    rw [MeasureTheory.ae_iff]
-    apply Set.Countable.measure_zero
-    simp
-
-    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
-      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
-      intro a ha
-      simp at ha
-      simp
-      by_contra C
-      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := by
-        sorry
-      exact ha.2 (decompose_f (circleMap 0 1 a) this C)
-
-    apply Set.Countable.mono t₀
-    apply Set.Countable.preimage_circleMap
-    apply Set.Finite.countable
-    apply finiteZeros
-
-    -- IsPreconnected (Metric.closedBall (0 : ℂ) 1)
-    apply IsConnected.isPreconnected
-    apply Convex.isConnected
-    exact convex_closedBall 0 1
-    exact Set.nonempty_of_nonempty_subtype
-    --
-    exact isCompact_closedBall 0 1
-    --
-    exact h'₁f
-    use 0
-    exact ⟨Metric.mem_closedBall_self (zero_le_one' ℝ), h₂f⟩
-    exact Ne.symm (zero_ne_one' ℝ)
-
-  have h₁Gi : ∀ i ∈ (ZeroFinset h₁f h₂f).attach, IntervalIntegrable (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) := by
-    -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
-    sorry
-
-  have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) + ∑ x ∈ (ZeroFinset h₁f h₂f).attach, ↑(order x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
-    dsimp [G]
-    rw [intervalIntegral.integral_add]
-    rw [intervalIntegral.integral_finset_sum]
-    simp_rw [intervalIntegral.integral_const_mul]
-
-    --  ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => ↑(order i) *
-    --  log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
-    intro i hi
-    apply IntervalIntegrable.const_mul
-    have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
-    simp at this
-    by_cases h₂i : ‖i.1‖ = 1
-    -- case pos
-    exact int'₂ h₂i
-    -- case neg
-    have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
-
-
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
-      rfl
-    rw [this]
-    apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp
-
-    by_contra ha'
-    conv at h₂i =>
-      arg 1
-      rw [← ha']
-      rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero 1 x]
-      simp
-    tauto
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    fun_prop
-    -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
-      rfl
-    rw [this]
-    apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp [h₂F]
-    --
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    apply ContinuousAt.comp
-    apply DifferentiableAt.continuousAt (𝕜 := ℂ )
-    apply HolomorphicAt.differentiableAt
-    simp [h₁F]
-    --
-    apply Continuous.continuousAt
-    apply continuous_circleMap
-    --
-    have : (fun x => ∑ s ∈ (ZeroFinset h₁f h₂f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s)))
-      = ∑ s ∈ (ZeroFinset h₁f h₂f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
-      funext x
-      simp
-    rw [this]
-    apply IntervalIntegrable.sum
-    intro i h₂i
-    apply IntervalIntegrable.const_mul
-    have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
-    simp at this
-    by_cases h₂i : ‖i.1‖ = 1
-    -- case pos
-    exact int'₂ h₂i
-    -- case neg
-    have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
-      rfl
-    rw [this]
-    apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp
-
-    by_contra ha'
-    conv at h₂i =>
-      arg 1
-      rw [← ha']
-      rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero 1 x]
-      simp
-    tauto
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    fun_prop
-
-  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
-    let logAbsF := fun w ↦ Real.log ‖F w‖
-    have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
-      intro z hz
-      apply logabs_of_holomorphicAt_is_harmonic
-      apply h₁F z hz
-      exact h₂F z hz
-
-    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
-  simp_rw [← Complex.norm_eq_abs] at this
-  rw [t₁] at this
-
-  --let Z₁ := (ZeroFinset h₁f h₂f) ∩ (Metric.ball 0 1)
-
-  let Z₂ := { x : ZeroFinset h₁f h₂f | ‖x.1‖ = 1 }
-
-
-  sorry

Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -8,10 +8,6 @@ import Nevanlinna.periodic_integrability
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
--- Integrability of periodic functions
-
-
-
 
 
 -- Lemmas for the circleMap
@@ -46,6 +42,20 @@ lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x))
 
 -- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.
 
+lemma int'₀
+  {a : ℂ}
+  (ha : a ∈ Metric.ball 0 1) :
+  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
+  apply Continuous.intervalIntegrable
+  apply Continuous.log
+  fun_prop
+  simp
+  intro x
+  by_contra h₁a
+  rw [← h₁a] at ha
+  simp at ha
+
+
 lemma int₀
   {a : ℂ}
   (ha : a ∈ Metric.ball 0 1) :
@@ -210,7 +220,6 @@ lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary
   rw [zero_add]
   exact int'₁
 
-
 lemma int₁ :
   ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
 
@@ -360,3 +369,16 @@ lemma int₂
     simp
   simp_rw [this]
   exact int₁
+
+
+lemma int₃
+  {a : ℂ}
+  (ha : a ∈ Metric.closedBall 0 1) :
+  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
+  by_cases h₁a : a ∈ Metric.ball 0 1
+  · exact int₀ h₁a
+  · apply int₂
+    simp at ha
+    simp at h₁a
+    simp
+    linarith