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,93 +7,28 @@ 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 : ℂ → ℂ)
-  (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
-    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 +84,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]
@@ -180,11 +115,7 @@ theorem jensen_case_R_eq_one
     exact Ne.symm (zero_ne_one' ℝ)
 
 
-  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
+  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
-    -- 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]
@@ -195,7 +126,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 hi
+    intro i _
     apply IntervalIntegrable.const_mul
     --simp at this
     by_cases h₂i : ‖i.1‖ = 1
@@ -250,7 +181,7 @@ theorem jensen_case_R_eq_one
       simp
     rw [this]
     apply IntervalIntegrable.sum
-    intro i h₂i
+    intro i _
     apply IntervalIntegrable.const_mul
     --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
     --simp at this
@@ -290,9 +221,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, _⟩
+  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,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