Working…

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_JensenFormula2.lean

@@ -7,72 +7,12 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 open Real
 
-/-
+lemma h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
-noncomputable def Zeroset
+  (convex_closedBall (0 : ℂ) 1).isPreconnected
-  {f : ℂ → ℂ}
-  {s : Set ℂ}
-  (hf : ∀ z ∈ s, HolomorphicAt f z) :
-  Set ℂ := by
-  exact f⁻¹' {0} ∩ s
 
+lemma h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
+  isCompact_closedBall 0 1
 
-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 : ℂ → ℂ)
@@ -81,19 +21,15 @@ theorem jensen_case_R_eq_one
   (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) :=
-    (convex_closedBall (0 : ℂ) 1).isPreconnected
-
-  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
 
   have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
-    sorry
+    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‖
 
@@ -149,7 +85,7 @@ theorem jensen_case_R_eq_one
     exact h₂F z h₁z
 
 
-  have : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := 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
 
     rw [intervalIntegral.integral_congr_ae]
     rw [MeasureTheory.ae_iff]
@@ -184,7 +120,7 @@ theorem jensen_case_R_eq_one
     -- This is hard. Need to invoke specialFunctions_CircleIntegral_affine.
     sorry
 
-  have : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
+  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]
@@ -290,9 +226,65 @@ theorem jensen_case_R_eq_one
       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
 
+  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
 
-  sorry
+  rw [int_logAbs_f_eq_int_G]
+  rw [decompose_int_G]
+  rw [h₃F]
+  simp
+  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
+
+  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset)]
+  simp
+  simp
+  intro x ⟨h₁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

Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -360,3 +360,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