Nevanlinna/analyticAt.lean

@@ -123,7 +123,7 @@ theorem eventually_nhds_comp_composition
     exact h₁t (ℓ y) hy
   · constructor
     · apply IsOpen.preimage
-      exact hℓ
+      exact ContinuousLinearEquiv.continuous ℓ
       exact h₂t
     · exact h₃t
 
@@ -132,25 +132,11 @@ theorem AnalyticAt.order_congr
   {f₁ f₂ : ℂ → ℂ}
   {z₀ : ℂ}
   (hf₁ : AnalyticAt ℂ f₁ z₀)
-  (hf : f₁ =ᶠ[nhds z₀] f₂) :
-  hf₁.order = (hf₁.congr hf).order := by
+  (hf₂ : AnalyticAt ℂ f₂ z₀)
+  (hf : ∀ᶠ (z : ℂ) in nhds z₀, f₁ z = f₂ z) :
+  hf₁.order = hf₂.order := by
 
-  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))
+  sorry
 
 
 theorem AnalyticAt.order_comp_CLE
@@ -165,10 +151,9 @@ 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
-    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
+    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
 
-    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by
-      apply analyticAt_const
     have : this.order = ⊤ := by
       rw [AnalyticAt.order_eq_top_iff]
       simp
@@ -191,7 +176,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₀)) A]
+    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
     simp
 
     rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]

Nevanlinna/diffOpGrothendieck.lean

@@ -0,0 +1,9 @@
+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,62 +301,25 @@ 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 ℓ : ℂ ≃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 := fun z ↦ f (R • z)
 
 
-  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
+
+    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
-  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