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

@@ -7,28 +7,93 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 open Real
 
-lemma h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
+/-
-  (convex_closedBall (0 : ℂ) 1).isPreconnected
+noncomputable def Zeroset
+  {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 : ℂ → ℂ)
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
   (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) :=
+    (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
-    intro z h₁z
+    sorry
-    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‖
 
@@ -84,7 +149,7 @@ theorem jensen_case_R_eq_one
     exact h₂F 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
+  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]
@@ -115,7 +180,11 @@ theorem jensen_case_R_eq_one
     exact Ne.symm (zero_ne_one' ℝ)
 
 
-  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
+  have h₁Gi : ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, 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 ∈ (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]
@@ -126,7 +195,7 @@ theorem jensen_case_R_eq_one
     --  ∀ 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 _
+    intro i hi
     apply IntervalIntegrable.const_mul
     --simp at this
     by_cases h₂i : ‖i.1‖ = 1
@@ -181,7 +250,7 @@ theorem jensen_case_R_eq_one
       simp
     rw [this]
     apply IntervalIntegrable.sum
-    intro i _
+    intro i h₂i
     apply IntervalIntegrable.const_mul
     --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
     --simp at this
@@ -221,65 +290,9 @@ 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
 
-  rw [int_logAbs_f_eq_int_G]
+  sorry
-  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, _⟩
-  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

@@ -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