Rename file

Nevanlinna/holomorphic_JensenFormula.lean

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

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -1,449 +0,0 @@
-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 : 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
-    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 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 [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 =>
-      left
-      left
-      arg 2
-      intro s
-      rw [Real.log_pow]
-    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
-
-
-  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]
-    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 :=
-        circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
-      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
-    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
-
-    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]
-    -- 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)))
-      = ∑ 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
-      funext x
-      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
-    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
-
-
-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
-  simp
-  by_cases hx : x = (0 : ℂ)
-  rw [hx]
-  simp
-
-  rw [log_mul, log_mul, log_inv, log_inv]
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-  rw [← this]
-  simp
-  left
-  congr 1
-
-  dsimp [AnalyticOn.order]
-  rw [← AnalyticAt.order_comp_CLE ℓ]
-
-  --
-  simpa
-  --
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-  rw [← this]
-  apply inv_ne_zero
-  exact Ne.symm (ne_of_lt hR)
-  --
-  exact Ne.symm (ne_of_lt hR)
-  --
-  simp
-  constructor
-  · assumption
-  · exact Ne.symm (ne_of_lt hR)