working…

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,3 +1,4 @@
+import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
@@ -5,31 +6,38 @@ import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : Differentiable ℂ 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 : Differentiable ℂ F)
+  (h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z)
-  (h₂F : ∀ z, F z ≠ 0)
+  (h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0)
-  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s))
+  (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) := 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
+
+  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
+
+
+
   let logAbsF := fun w ↦ Real.log ‖F w‖
 
-  have t₀ : ∀ z ∈ Metric.ball 0 2, HarmonicAt logAbsF z := by
+  have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
-    intro z _
+    intro z hz
     apply logabs_of_holomorphicAt_is_harmonic
-    apply h₁F.holomorphicAt
+    apply h₁F z hz
-    exact h₂F z
+    exact h₂F z hz
 
   have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, logAbsF (circleMap 0 1 x)) = 2 * Real.pi * logAbsF 0 := by
-    have hR : (0 : ℝ) < (1 : ℝ) := by apply Real.zero_lt_one
+    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
-    have hρ : (1 : ℝ) < (2 : ℝ) := by linarith
-    apply harmonic_meanValue 2 1 hR hρ t₀
-
 
   have t₂ : ∀ s, f (a s) = 0 := by
     intro s
@@ -41,8 +49,8 @@ theorem jensen_case_R_eq_one
     simp
 
   let logAbsf := fun w ↦ Real.log ‖f w‖
-  have s₀ : ∀ z, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
+  have s₀ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsf z = logAbsF z + ∑ s, Real.log ‖z - a s‖ := by
-    intro z hz
+    intro z h₁z h₂z
     dsimp [logAbsf]
     rw [h₃F]
     simp_rw [Complex.abs.map_mul]
@@ -53,31 +61,34 @@ theorem jensen_case_R_eq_one
     intro s hs
     simp
     by_contra ha'
-    rw [ha'] at hz
+    rw [ha'] at h₂z
-    exact hz (t₂ s)
+    exact h₂z (t₂ s)
     -- Complex.abs (F z) ≠ 0
     simp
-    exact h₂F z
+    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 hz
+    rw [h''] at h₂z
     let A := t₂ s
-    exact hz A
+    exact h₂z A
 
-  have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
+  have s₁ : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
-    intro z hz
+    intro z h₁z h₂z
-    rw [s₀ z hz]
+    rw [s₀ z h₁z]
     simp
+    assumption
 
-  rw [s₁ 0 h₂f] at t₁
+  have : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by simp
+  rw [s₁ 0 this h₂f] at t₁
 
   have h₀ {x : ℝ} : f (circleMap 0 1 x) ≠ 0 := by
     rw [h₃F]
     simp
     constructor
-    · exact h₂F (circleMap 0 1 x)
+    · 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
@@ -88,7 +99,8 @@ theorem jensen_case_R_eq_one
       rw [← this] at A
       simp at A
 
-  simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁
+  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₁
 
@@ -133,7 +145,10 @@ theorem jensen_case_R_eq_one
   apply ContinuousAt.comp
   apply Complex.continuous_abs.continuousAt
   apply ContinuousAt.comp
-  apply h₁f.continuous.continuousAt
+  apply ContDiffAt.continuousAt (f := f) (𝕜 := ℝ) (n := 1)
+  apply HolomorphicAt.contDiffAt
+  apply h₁f
+  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)

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -1,41 +1,163 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
+import Mathlib.Analysis.Analytic.IsolatedZeros
+import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
-import Mathlib.Analysis.Analytic.IsolatedZeros
+
+open Real
 
 
-lemma xx
+def ZeroFinset
   {f : ℂ → ℂ}
-  {S : Set ℂ}
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) :
-  (h₁S : IsPreconnected S)
+  Finset ℂ := by
-  (h₂S : IsCompact S)
-  (hf : ∀ s ∈ S, AnalyticAt ℂ f s) :
-  ∃ o : ℂ → ℕ, ∃ F : ℂ → ℂ, ∀ z ∈ S, (AnalyticAt ℂ F z) ∧ (F z ≠ 0) ∧ (f z = F z * ∏ᶠ s ∈ S, (z - s) ^ (o s)) := by
 
-  let o : ℂ → ℕ := by
+  let Z := f⁻¹' {0} ∩ Metric.closedBall (0 : ℂ) 1
-    intro z
+  have hZ : Set.Finite Z := by sorry
-    if hz : z ∈ S then
+  exact hZ.toFinset
-      let A := hf z hz
-      let B := A.order
 
-      exact (A.order : ⊤)
-    else
-      exact 0
 
+def order
+  {f : ℂ → ℂ}
+  {hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z} :
+  ZeroFinset hf → ℕ := by sorry
+
+
+lemma ZeroFinset_mem_iff
+  {f : ℂ → ℂ}
+  (hf : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
+  (z : ℂ) :
+  z ∈ ↑(ZeroFinset hf) ↔ z ∈ Metric.closedBall 0 1 ∧ f z = 0 := by
   sorry
 
 
-theorem jensen_case_R_eq_one'
+theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : Differentiable ℂ f)
+  (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z)
-  (h₂f : f 0 ≠ 0)
+  (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z)
-  (S : Finset ℕ)
+  (h₂f : f 0 ≠ 0) :
-  (a : S → ℂ)
+  log ‖f 0‖ = -∑ s : ZeroFinset h₁f, order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by
-  (ha : ∀ s, a s ∈ Metric.ball 0 1)
+
-  (F : ℂ → ℂ)
+  have F : ℂ → ℂ := by sorry
-  (h₁F : Differentiable ℂ F)
+  have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry
-  (h₂F : ∀ z, F z ≠ 0)
+  have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry
-  (h₃F : f = fun z ↦ (F z) * ∏ s : S, (z - a s))
+  have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f, (z - s) ^ (order s) := by sorry
-  :
+
-  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
+  let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset 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).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).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 * π)
+
+    -- This won't work, because the function **is not** continuous. Need to fix.
+    intro i hi
+    apply IntervalIntegrable.const_mul
+    exact h₁Gi i hi
+
+    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'
+    let A := ha i
+    rw [← ha'] at A
+    simp at A
+    apply ContinuousAt.comp
+    apply Complex.continuous_abs.continuousAt
+    fun_prop
+
+    sorry
+
+
   sorry