working

Nevanlinna/analyticAt.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Complex.Basic
+import Mathlib.Analysis.Analytic.Linear
 
 
 theorem AnalyticAt.order_mul
@@ -85,3 +86,97 @@ theorem AnalyticAt.supp_order_toNat
   contrapose
   intro h₁f
   simp [hf.order_eq_zero_iff.2 h₁f]
+
+
+theorem ContinuousLinearEquiv.analyticAt
+  (ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀
+
+
+theorem eventually_nhds_comp_composition
+  {f₁ f₂ ℓ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : ∀ᶠ (z : ℂ) in nhds (ℓ z₀), f₁ z = f₂ z)
+  (hℓ : Continuous ℓ) :
+  ∀ᶠ (z : ℂ) in nhds z₀, (f₁ ∘ ℓ) z = (f₂ ∘ ℓ) z := by
+  obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hf
+  apply eventually_nhds_iff.2
+  use ℓ⁻¹' t
+  constructor
+  · intro y hy
+    exact h₁t (ℓ y) hy
+  · constructor
+    · apply IsOpen.preimage
+      exact ContinuousLinearEquiv.continuous ℓ
+      exact h₂t
+    · exact h₃t
+
+
+theorem AnalyticAt.order_congr
+  {f₁ f₂ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf₁ : AnalyticAt ℂ f₁ z₀)
+  (hf₂ : AnalyticAt ℂ f₂ z₀)
+  (hf : ∀ᶠ (z : ℂ) in nhds z₀, f₁ z = f₂ z) :
+  hf₁.order = hf₂.order := by
+
+  sorry
+
+
+theorem AnalyticAt.order_comp_CLE
+  (ℓ : ℂ ≃L[ℂ] ℂ)
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f (ℓ z₀)) :
+  hf.order = (hf.comp (ℓ.analyticAt z₀)).order := by
+
+  by_cases h₁f : hf.order = ⊤
+  · rw [h₁f]
+    rw [AnalyticAt.order_eq_top_iff] at h₁f
+    let A := eventually_nhds_comp_composition h₁f ℓ.continuous
+    simp at A
+    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
+
+    have : this.order = ⊤ := by
+      rw [AnalyticAt.order_eq_top_iff]
+      simp
+    rw [this]
+  · let n := hf.order.toNat
+    have hn : hf.order = n := Eq.symm (ENat.coe_toNat h₁f)
+    rw [hn]
+    rw [AnalyticAt.order_eq_nat_iff] at hn
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
+    have A := eventually_nhds_comp_composition h₃g ℓ.continuous
+    simp only [Function.comp_apply] at A
+    have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by apply analyticAt_const
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
+    simp
+    rw [AnalyticAt.order_mul]
+
+
+
+
+    --rw [hn, AnalyticAt.order_eq_nat_iff]
+    rw [AnalyticAt.order_eq_nat_iff] at hn
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
+    use g ∘ ℓ
+    constructor
+    · exact h₁g.comp (ℓ.analyticAt z₀)
+    · constructor
+      · exact h₂g
+      · rw [eventually_nhds_iff]
+        rw [eventually_nhds_iff] at h₃g
+        obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₃g
+        use ℓ⁻¹' t
+        constructor
+        · intro y hy
+          simp
+          rw [h₁t (ℓ y) hy]
+
+
+          sorry
+        · constructor
+          · apply IsOpen.preimage
+            exact ContinuousLinearEquiv.continuous ℓ
+            exact h₂t
+          · exact h₃t

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -11,7 +11,7 @@ open Real
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1))
+  (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
 
@@ -284,3 +284,103 @@ theorem jensen_case_R_eq_one
   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 F := fun z ↦ f (R • z)
+
+
+
+  have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
+    apply AnalyticOn.comp (t := Metric.closedBall 0 R)
+    exact h₁f
+
+
+
+    sorry
+  have h₂F : F 0 ≠ 0 := by sorry
+
+  let A := jensen_case_R_eq_one F h₁F h₂F
+  dsimp [F] at A
+  simp
+  rw [mul_zero] at A
+  rw [A]
+  simp
+
+  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
+
+
+  sorry