Nevanlinna/analyticAt.lean

@@ -1,226 +0,0 @@
-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,25 +1,21 @@
 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₀ : U}
+  {z₀ : ℂ}
   (hf : AnalyticOn ℂ f U)
+  (hz₀ : z₀ ∈ U)
   (n : ℕ) :
-  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
+  (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₀ z₀.2) n).1 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
@@ -48,7 +44,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₀.1}ᶜ
+    use {z₀}ᶜ
     constructor
     · intro y hy
       simp at hy
@@ -91,20 +87,59 @@ 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₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
+  exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
 
 
-theorem AnalyticOn.support_of_order₁
+theorem AnalyticAt.order_mul
-  {f : ℂ → ℂ}
+  {f₁ f₂ : ℂ → ℂ}
-  {U : Set ℂ}
+  {z₀ : ℂ}
-  (hf : AnalyticOn ℂ f U) :
+  (hf₁ : AnalyticAt ℂ f₁ z₀)
-  Function.support hf.order = U.restrict f⁻¹' {0} := by
+  (hf₂ : AnalyticAt ℂ f₂ z₀) :
-  ext u
+  (AnalyticAt.mul hf₁ hf₂).order = hf₁.order + hf₂.order := by
-  simp [AnalyticOn.order]
+  by_cases h₂f₁ : hf₁.order = ⊤
-  rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
+  · 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
@@ -112,8 +147,8 @@ theorem AnalyticOn.eliminateZeros
   {U : Set ℂ}
   {A : Finset U}
   (hf : AnalyticOn ℂ f U)
-  (n : U → ℕ) :
+  (n : ℂ → ℕ) :
-  (∀ 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
+  (∀ 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)
 
@@ -132,7 +167,7 @@ theorem AnalyticOn.eliminateZeros
 
     rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)]
 
-    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a)
+    let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1)
 
     have : f = fun z ↦ φ z * g₀ z := by
       funext z
@@ -173,7 +208,8 @@ theorem AnalyticOn.eliminateZeros
     rw [h₂φ]
     simp
 
-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
+
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
 
   use g₁
   constructor
@@ -223,14 +259,14 @@ theorem discreteZeros
   (hU : IsPreconnected U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  DiscreteTopology ((U.restrict f)⁻¹' {0}) := by
+  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.1.2
+  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
@@ -275,9 +311,9 @@ theorem discreteZeros
     _ < min ε₁ ε₂ := by assumption
     _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
 
+
   have F := h₂ε₂ y.1 h₂y
-  have : f y = 0 := by exact y.2
+  rw [y.2.2] at F
-  rw [this] at F
   simp at F
 
   have : g y.1 ≠ 0 := by
@@ -295,19 +331,19 @@ theorem finiteZeros
   (h₂U : IsCompact U)
   (h₁f : AnalyticOn ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  Set.Finite (U.restrict f⁻¹' {0}) := by
+  Set.Finite ↑(U ∩ f⁻¹' {0}) := by
 
-  have closedness : IsClosed (U.restrict f⁻¹' {0}) := by
+  have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by
-    apply IsClosed.preimage
+    apply IsCompact.of_isClosed_subset h₂U
-    apply continuousOn_iff_continuous_restrict.1
+    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
-    exact h₁f.continuousOn
+    exact IsCompact.isClosed h₂U
     exact isClosed_singleton
+    exact Set.inter_subset_left
 
-  have : CompactSpace U := by
+  apply hinter.finite
-    exact isCompact_iff_compactSpace.mp h₂U
+  apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0}))
-
-  apply (IsClosed.isCompact closedness).finite
   exact discreteZeros h₁U h₁f h₂f
+  rfl
 
 
 theorem AnalyticOnCompact.eliminateZeros
@@ -317,20 +353,32 @@ 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.order a).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 a a.2).order.toNat) • g z := by
 
-  let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
+  let ι : U → ℂ := Subtype.val
 
-  let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat
+  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, AnalyticOn.order]
+    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
@@ -338,6 +386,11 @@ 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
@@ -347,115 +400,15 @@ 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 C
+            exact this
           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

@@ -0,0 +1,449 @@
+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

@@ -0,0 +1,9 @@
+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,23 +125,6 @@ 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,449 +1,172 @@
-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 : AnalyticOn ℂ f (Metric.closedBall 0 1))
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  (h₂f : f 0 ≠ 0) :
+  (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
+  (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
 
-  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
+  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by sorry
-    (convex_closedBall (0 : ℂ) 1).isPreconnected
+  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 : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
+  let α := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f
-    isCompact_closedBall 0 1
+  obtain ⟨g, A, h'₁g, h₂g, h₃g⟩ := α
+  have h₁g : ∀ z ∈ Metric.closedBall 0 1, HolomorphicAt F z := by sorry
 
-  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
 
-  have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
+  let logAbsF := fun w ↦ Real.log ‖F w‖
-    intro z h₁z
-    apply AnalyticAt.holomorphicAt
-    exact h₁F z h₁z
 
-  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₀ : ∀ 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
 
-  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
+  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
     intro z h₁z h₂z
-
+    dsimp [logAbsf]
-    conv =>
+    rw [h₃F]
-      left
+    simp_rw [Complex.abs.map_mul]
-      arg 1
+    rw [Complex.abs_prod]
-      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]
-    conv =>
+    rfl
-      left
+    intro s hs
-      left
+    simp
-      arg 2
+    by_contra ha'
-      intro s
+    rw [ha'] at h₂z
-      rw [Real.log_pow]
+    exact h₂z (t₂ s)
-    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
-  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
+    intro z h₁z h₂z
-
+    rw [s₀ z h₁z]
-    rw [intervalIntegral.integral_congr_ae]
-    rw [MeasureTheory.ae_iff]
-    apply Set.Countable.measure_zero
     simp
+    assumption
 
-    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
+  have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp
-      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
+  rw [s₁ 0 this h₂f] at t₁
-      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)
 
-    apply Set.Countable.mono t₀
+  have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
-    apply Set.Countable.preimage_circleMap
+    rw [h₃F]
-    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
 
-    by_contra ha'
+  have {θ} : (circleMap 0 1 θ) ∈ Metric.closedBall (0 : ℂ) 1 := by simp
-    conv at h₂i =>
+  simp_rw [s₁ (circleMap 0 1 _) this h₀] at t₁
-      arg 1
+  rw [intervalIntegral.integral_sub] at t₁
-      rw [← ha']
+  rw [intervalIntegral.integral_finset_sum] at t₁
-      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
 
-    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)))
+  simp_rw [int₀ (ha _)] at t₁
-      = ∑ 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
+  simp at t₁
-      funext x
+  rw [t₁]
-      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 {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
+  have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by
-    calc π⁻¹ * 2⁻¹ * (2 * π * l)
+    ring_nf
-    _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
+    simp [mul_inv_cancel₀ Real.pi_ne_zero]
-    _ = π⁻¹ * π * 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
-  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
+  -- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
-  simp
+  intro i _
-  simp
+  apply Continuous.intervalIntegrable
-  intro x ⟨h₁x, _⟩
+  apply continuous_iff_continuousAt.2
-  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
-  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 => 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
   simp
-  by_cases hx : x = (0 : ℂ)
+  by_contra ha'
-  rw [hx]
+  let A := ha i
+  rw [← ha'] 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
+  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₀
-  rw [log_mul, log_mul, log_inv, log_inv]
+  apply ContinuousAt.comp
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+  apply Complex.continuous_abs.continuousAt
-  rw [← this]
+  apply ContinuousAt.comp
+  apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1)
+  apply HolomorphicAt.contDiffAt
+  apply h₁f
   simp
-  left
+  let A := continuous_circleMap 0 1
-  congr 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)
-  dsimp [AnalyticOn.order]
+  apply Continuous.intervalIntegrable
-  rw [← AnalyticAt.order_comp_CLE ℓ]
+  apply continuous_finset_sum
-
+  intro i _
-  --
+  apply continuous_iff_continuousAt.2
-  simpa
+  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) :=
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
+    rfl
-  rw [← this]
+  rw [this]
-  apply inv_ne_zero
+  apply ContinuousAt.comp
-  exact Ne.symm (ne_of_lt hR)
+  apply Real.continuousAt_log
-  --
-  exact Ne.symm (ne_of_lt hR)
-  --
   simp
-  constructor
+  by_contra ha'
-  · assumption
+  let A := ha i
-  · exact Ne.symm (ne_of_lt hR)
+  rw [← ha'] at A
+  simp at A
+  apply ContinuousAt.comp
+  apply Complex.continuous_abs.continuousAt
+  fun_prop

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -0,0 +1,287 @@
+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,6 +8,10 @@ import Nevanlinna.periodic_integrability
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
+-- Integrability of periodic functions
+
+
+
 
 
 -- Lemmas for the circleMap
@@ -42,20 +46,6 @@ 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) :
@@ -220,6 +210,7 @@ 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
 
@@ -369,16 +360,3 @@ 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