Update holomorphic_JensenFormula2.lean

Nevanlinna/analyticAt.lean

@@ -123,7 +123,7 @@ theorem eventually_nhds_comp_composition
     exact h₁t (ℓ y) hy
   · constructor
     · apply IsOpen.preimage
-      exact ContinuousLinearEquiv.continuous ℓ
+      exact hℓ
       exact h₂t
     · exact h₃t
 
@@ -132,11 +132,25 @@ 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
+  (hf : f₁ =ᶠ[nhds z₀] f₂) :
+  hf₁.order = (hf₁.congr hf).order := by
 
-  sorry
+  by_cases h₁f₁ : hf₁.order = ⊤
+  rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
+  rw [AnalyticAt.order_eq_top_iff] at h₁f₁
+  exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
+  --
+  let n := hf₁.order.toNat
+  have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
+  rw [hn, eq_comm, 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
+  · assumption
+  · constructor
+    · assumption
+    · exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
 
 
 theorem AnalyticAt.order_comp_CLE
@@ -151,9 +165,10 @@ theorem AnalyticAt.order_comp_CLE
     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]
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
 
+    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by
+      apply analyticAt_const
     have : this.order = ⊤ := by
       rw [AnalyticAt.order_eq_top_iff]
       simp
@@ -176,7 +191,7 @@ theorem AnalyticAt.order_comp_CLE
       exact t₀
       apply AnalyticAt.comp h₁g
       exact ContinuousLinearEquiv.analyticAt ℓ z₀
-    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
     simp
 
     rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]

Nevanlinna/diffOpGrothendieck.lean

@@ -1,9 +0,0 @@
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
-
-/-
-
-Here we would like to define differential operators, following EGA 4-1, §20.
-This is work to be done in the future.
-
--/

Nevanlinna/holomorphic_JensenFormula2.lean

@@ -301,25 +301,62 @@ theorem jensen
   (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)
+
+  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
 
-
-    sorry
-  have h₂F : F 0 ≠ 0 := by sorry
+  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 [mul_zero] at A
   rw [A]
-  simp
 
   simp_rw [← const_mul_circleMap_zero]
   simp