Nevanlinna/holomorphic_examples.lean

@@ -1,6 +1,6 @@
 import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
-import Nevanlinna.holomorphic_primitive2
+import Nevanlinna.holomorphic_primitive
 import Nevanlinna.mathlibAddOn
 
 
@@ -108,175 +108,131 @@ function.
 
 theorem harmonic_is_realOfHolomorphic
   {f : ℂ → ℝ}
-  {z : ℂ}
-  {R : ℝ}
-  (hR : 0 < R)
-  (hf : ∀ x ∈ Metric.ball z R, HarmonicAt f x) :
-  ∃ F : ℂ → ℂ, (∀ x ∈ Metric.ball z R, HolomorphicAt F x) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := by
+  (hf : ∀ z, HarmonicAt f z) :
+  ∃ F : ℂ → ℂ, (∀ z, HolomorphicAt F z) ∧ (Complex.reCLM ∘ F = f) := by
 
   let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
   let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
 
   let g : ℂ → ℂ := f_1 - Complex.I • f_I
 
-  have contDiffOn_if_contDiffAt
-    {f' : ℂ → ℝ}
-    {z' : ℂ}
-    {R' : ℝ}
-    {n' : ℕ}
-    (hf' : ∀ x ∈ Metric.ball z' R', ContDiffAt ℝ n' f' x) :
-    ContDiffOn ℝ n' f' (Metric.ball z' R') := by
-    intro z hz
-    apply ContDiffAt.contDiffWithinAt
-    exact hf' z hz
+  have reg₂f : ContDiff ℝ 2 f := by
+    apply contDiff_iff_contDiffAt.mpr
+    intro z
+    exact (hf z).1
 
-  have reg₂f : ContDiffOn ℝ 2 f (Metric.ball z R) := by
-    apply contDiffOn_if_contDiffAt
-    intro x hx
-    exact (hf x hx).1
-
-  have contDiffOn_if_contDiffAt'
-    {f' : ℂ → ℂ}
-    {z' : ℂ}
-    {R' : ℝ}
-    {n' : ℕ}
-    (hf' : ∀ x ∈ Metric.ball z' R', ContDiffAt ℝ n' f' x) :
-    ContDiffOn ℝ n' f' (Metric.ball z' R') := by
-    intro z hz
-    apply ContDiffAt.contDiffWithinAt
-    exact hf' z hz
-
-  have reg₁f_1 : ContDiffOn ℝ 1 f_1 (Metric.ball z R) := by
-    apply contDiffOn_if_contDiffAt'
-    intro z hz
+  have reg₁f_1 : ContDiff ℝ 1 f_1 := by
+    apply contDiff_iff_contDiffAt.mpr
+    intro z
     dsimp [f_1]
     apply ContDiffAt.continuousLinearMap_comp
-    exact partialDeriv_contDiffAt ℝ (hf z hz).1 1
+    exact partialDeriv_contDiffAt ℝ (hf z).1 1
 
-  have reg₁f_I : ContDiffOn ℝ 1 f_I (Metric.ball z R) := by
-    apply contDiffOn_if_contDiffAt'
-    intro z hz
+  have reg₁f_I : ContDiff ℝ 1 f_I := by
+    apply contDiff_iff_contDiffAt.mpr
+    intro z
     dsimp [f_I]
     apply ContDiffAt.continuousLinearMap_comp
-    exact partialDeriv_contDiffAt ℝ (hf z hz).1 Complex.I
+    exact partialDeriv_contDiffAt ℝ (hf z).1 Complex.I
 
-  have reg₁g : ContDiffOn ℝ 1 g (Metric.ball z R) := by
+  have reg₁g : ContDiff ℝ 1 g := by
     dsimp [g]
-    apply ContDiffOn.sub
+    apply ContDiff.sub
     exact reg₁f_1
-    have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
-    rw [this]
-    apply ContDiffOn.const_smul
+    apply ContDiff.const_smul'
     exact reg₁f_I
 
-  have reg₁ : DifferentiableOn ℂ g (Metric.ball z R) := by
-    intro x hx
-    apply DifferentiableAt.differentiableWithinAt
+  have reg₁ : Differentiable ℂ g := by
+    intro z
     apply CauchyRiemann₇.2
     constructor
-    · apply DifferentiableWithinAt.differentiableAt (reg₁g.differentiableOn le_rfl x hx)
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
+    · apply Differentiable.differentiableAt
+      apply ContDiff.differentiable
+      exact reg₁g
+      rfl
     · dsimp [g]
-      rw [partialDeriv_sub₂_differentiableAt, partialDeriv_sub₂_differentiableAt]
+      rw [partialDeriv_sub₂, partialDeriv_sub₂]
+      simp
       dsimp [f_1, f_I]
       rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
-      rw [partialDeriv_compContLinAt, partialDeriv_compContLinAt]
-      simp
-      rw [partialDeriv_compContLinAt, partialDeriv_compContLinAt]
+      rw [partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin]
       rw [mul_sub]
       simp
       rw [← mul_assoc]
       simp
       rw [add_comm, sub_eq_add_neg]
       congr 1
-      · rw [partialDeriv_commOn _ reg₂f Complex.I 1]
-        exact hx
-        exact Metric.isOpen_ball
-      · let A := Filter.EventuallyEq.eq_of_nhds (hf x hx).2
+      · rw [partialDeriv_comm reg₂f Complex.I 1]
+      · let A := Filter.EventuallyEq.eq_of_nhds (hf z).2
         simp at A
         unfold Complex.laplace at A
         conv =>
           right
           right
-          rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) x)]
+          rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) z)]
           rw [← A]
         simp
 
-      --DifferentiableAt ℝ (partialDeriv ℝ _ f)
+      --Differentiable ℝ (partialDeriv ℝ _ f)
       repeat
-        apply ContDiffAt.differentiableAt
-        apply partialDeriv_contDiffAt ℝ (hf x hx).1
+        apply ContDiff.differentiable
+        apply contDiff_iff_contDiffAt.mpr
+        exact fun w ↦ partialDeriv_contDiffAt ℝ (hf w).1 _
         apply le_rfl
-
-      -- DifferentiableAt ℝ f_1 x
-      apply (reg₁f_1.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
-      -- DifferentiableAt ℝ (Complex.I • f_I)
-      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
-      rw [this]
-      apply DifferentiableAt.const_smul
-      apply (reg₁f_I.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
       -- Differentiable ℝ f_1
-      apply (reg₁f_1.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
+      exact reg₁f_1.differentiable le_rfl
       -- Differentiable ℝ (Complex.I • f_I)
-      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
-      rw [this]
-      apply DifferentiableAt.const_smul
-      apply (reg₁f_I.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
+      apply Differentiable.const_smul'
+      exact reg₁f_I.differentiable le_rfl
+      -- Differentiable ℝ f_1
+      exact reg₁f_1.differentiable le_rfl
+      -- Differentiable ℝ (Complex.I • f_I)
+      apply Differentiable.const_smul'
+      exact reg₁f_I.differentiable le_rfl
 
-  let F := fun z' ↦ (primitive z g) z' + f z
+  let F := fun z ↦ (primitive 0 g) z + f 0
 
-  have regF : DifferentiableOn ℂ F (Metric.ball z R) := by
-    apply DifferentiableOn.add
-    apply primitive_differentiableOn reg₁
+  have regF : Differentiable ℂ F := by
+    apply Differentiable.add
+    apply primitive_differentiable reg₁
     simp
 
-  have pF'' : ∀ x ∈ Metric.ball z R, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by
-    intro x hx
-    have : DifferentiableAt ℂ F x := by
-      apply (regF x hx).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    rw [DifferentiableAt.fderiv_restrictScalars ℝ this]
+  have pF'' : ∀ x, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by
+    intro x
+    rw [DifferentiableAt.fderiv_restrictScalars ℝ (regF x)]
     dsimp [F]
     rw [fderiv_add_const]
-    rw [primitive_fderiv' reg₁ x hx]
+    rw [primitive_fderiv']
     exact rfl
+    exact reg₁
 
   use F
 
   constructor
-  · -- ∀ x ∈ Metric.ball z R, HolomorphicAt F x
-    intro x hx
+  · -- ∀ (z : ℂ), HolomorphicAt F z
+    intro z
     apply HolomorphicAt_iff.2
-    use Metric.ball z R
+    use Set.univ
     constructor
-    · exact Metric.isOpen_ball
+    · exact isOpen_const
     · constructor
-      · assumption
-      · intro w hw
-        apply (regF w hw).differentiableAt
-        apply IsOpen.mem_nhds Metric.isOpen_ball hw
-  · -- Set.EqOn (⇑Complex.reCLM ∘ F) f (Metric.ball z R)
-    have : DifferentiableOn ℝ (Complex.reCLM ∘ F) (Metric.ball z R) := by
-      apply DifferentiableOn.comp
-      apply Differentiable.differentiableOn
-      apply ContinuousLinearMap.differentiable Complex.reCLM
-      apply regF.restrictScalars ℝ
-      exact Set.mapsTo'.mpr fun ⦃a⦄ _ => hR
-    have hz : z ∈ Metric.ball z R := by exact Metric.mem_ball_self hR
-    apply Convex.eqOn_of_fderivWithin_eq _ this _ _ _ hz _
-    exact convex_ball z R
-    apply reg₂f.differentiableOn one_le_two
-    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
+      · simp
+      · intro w _
+        exact regF w
+  · -- (F z).re = f z
+    have A := reg₂f.differentiable one_le_two
+    have B : Differentiable ℝ (Complex.reCLM ∘ F) := by
+      apply Differentiable.comp
+      exact ContinuousLinearMap.differentiable Complex.reCLM
+      exact Differentiable.restrictScalars ℝ regF
+    have C : (F 0).re = f 0 := by
+      dsimp [F]
+      rw [primitive_zeroAtBasepoint]
+      simp
 
-    intro x hx
-    rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
+    apply eq_of_fderiv_eq B A _ 0 C
+
+    intro x
     rw [fderiv.comp]
     simp
     apply ContinuousLinearMap.ext
@@ -291,24 +247,7 @@ theorem harmonic_is_realOfHolomorphic
     rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
     rw [smul_eq_mul, smul_eq_mul]
     ring
-
-    assumption
-    exact ContinuousLinearMap.differentiableAt Complex.reCLM
-    apply (regF.restrictScalars ℝ  x hx).differentiableAt
-    apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
-    assumption
-    apply (reg₂f.differentiableOn one_le_two).differentiableAt
-    apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
-    assumption
-    -- DifferentiableAt ℝ (⇑Complex.reCLM ∘ F) x
-    apply DifferentiableAt.comp
-    apply Differentiable.differentiableAt
-    exact ContinuousLinearMap.differentiable Complex.reCLM
-    apply (regF.restrictScalars ℝ  x hx).differentiableAt
-    apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    --
-    dsimp [F]
-    rw [primitive_zeroAtBasepoint]
-    simp
+    -- DifferentiableAt ℝ (⇑Complex.reCLM) (F x)
+    fun_prop
+    -- DifferentiableAt ℝ F x
+    exact regF.restrictScalars ℝ x

Nevanlinna/holomorphic_primitive2.lean

@@ -49,6 +49,9 @@ theorem primitive_fderivAtBasepointZero
     rw [this]
 
   obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by
+    have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by
+      apply Metric.ball_mem_nhds (f 0)
+      linarith
     apply eventually_nhds_iff.mp
     apply continuousAt_def.1
     apply Continuous.continuousAt
@@ -121,37 +124,7 @@ theorem primitive_fderivAtBasepointZero
     apply h₁s
     exact h₂ε.1 hy
 
-
-  have intervalComputation_uIcc {x' y' : ℝ} (h : x' ∈ Set.uIcc 0 y') : |x'| ≤ |y'| := by
-    let A := h.1
-    let B := h.2
-    rcases le_total 0 y' with hy | hy
-    · simp [hy] at A
-      simp [hy] at B
-      rwa [abs_of_nonneg A, abs_of_nonneg hy]
-    · simp [hy] at A
-      simp [hy] at B
-      rw [abs_of_nonpos hy]
-      rw [abs_of_nonpos]
-      linarith [h.1]
-      exact B
-
-
-  rw [Filter.eventually_iff_exists_mem]
-  use Metric.ball 0 (ε / (4 : ℝ))
-
-  constructor
-  · apply Metric.ball_mem_nhds 0
-    linarith
-  · intro y hy
-
-    have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
-      abel
-    rw [this]
-    rw [← smul_sub]
-
-
-    have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by
+  have t₀ {r : ℝ} (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
     apply ContinuousOn.intervalIntegrable
     apply ContinuousOn.comp
     exact hf
@@ -165,62 +138,60 @@ theorem primitive_fderivAtBasepointZero
     constructor
     · simp
       calc |x|
-        _ ≤ |y.re| := by apply intervalComputation_uIcc hx
-        _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
-        _ < ε / 4 := by simp at hy; assumption
-        _ < ε := by linarith
+      _ < ε := by
+        sorry
     · simpa
-    have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by
+
+  have t₁ {r : ℝ}  (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
     apply ContinuousOn.intervalIntegrable
     apply ContinuousOn.comp
     apply hf
     fun_prop
-      intro x _
+    intro x hx
     simpa
-    rw [← intervalIntegral.integral_sub t₀ t₁]
 
-    have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by
-      apply ContinuousOn.intervalIntegrable
-      apply ContinuousOn.comp
-      exact hf
-      have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by
+
+  have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp hf
+    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
       funext x
       apply Complex.ext
       rw [Complex.add_re]
       simp
       simp
     rw [this]
-      apply ContinuousOn.add
-      apply Continuous.continuousOn
+    apply Continuous.add
     continuity
     fun_prop
-      intro x hx
-      apply h₂ε.2
-      constructor
-      · simp
-        calc |y.re|
-        _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
-        _ < ε / 4 := by simp at hy; assumption
-        _ < ε := by linarith
-      · simp
-        calc |x|
-        _ ≤ |y.im| := by apply intervalComputation_uIcc hx
-        _ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y
-        _ < ε / 4 := by simp at hy; assumption
-        _ < ε := by linarith
-    have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by
-      apply ContinuousOn.intervalIntegrable
-      apply ContinuousOn.comp
+
+  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
+    apply Continuous.intervalIntegrable
+    apply Continuous.comp
     exact hf
     fun_prop
-      intro x _
-      apply h₂ε.2
-      simp
-      constructor
-      · simpa
-      · simpa
+
+  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
+    abel
+  conv =>
+    left
+    intro x
+    left
+    arg 1
+    rw [this]
+    rw [← smul_sub]
+
+    rw [← intervalIntegral.integral_sub t₀ t₁]
     rw [← intervalIntegral.integral_sub t₂ t₃]
 
+  rw [Filter.eventually_iff_exists_mem]
+
+
+  use Metric.ball 0 (ε / (4 : ℝ))
+  constructor
+  · apply Metric.ball_mem_nhds 0
+    linarith
+  · intro y hy
     have h₁y : |y.re| < ε / 4 := by
       calc |y.re|
       _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
@@ -781,11 +752,12 @@ theorem primitive_hasDerivAt
   apply hasDerivAt_const
 
 
-theorem primitive_differentiableOn
+
+theorem primitive_differentiable
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   {f : ℂ  → E}
-  {z₀ : ℂ}
-  {R : ℝ}
+  (z₀ : ℂ)
+  (R : ℝ)
   (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
   :
   DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by

Nevanlinna/partialDeriv.lean

@@ -102,6 +102,20 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f
   simp
 
 
+theorem partialDeriv_sub₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ - f₂) = (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
+  unfold partialDeriv
+  intro v
+  have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
+  rw [this]
+  conv =>
+    left
+    intro w
+    left
+    rw [fderiv_sub (h₁ w) (h₂ w)]
+  funext w
+  simp
+
+
 theorem partialDeriv_add₂_differentiableAt
   {f₁ f₂ : E → F}
   {v : E}
@@ -139,57 +153,6 @@ theorem partialDeriv_add₂_contDiffAt
     exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
 
 
-theorem partialDeriv_sub₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ - f₂) = (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
-  unfold partialDeriv
-  intro v
-  have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
-  rw [this]
-  conv =>
-    left
-    intro w
-    left
-    rw [fderiv_sub (h₁ w) (h₂ w)]
-  funext w
-  simp
-
-
-theorem partialDeriv_sub₂_differentiableAt
-  {f₁ f₂ : E → F}
-  {v : E}
-  {x : E}
-  (h₁ : DifferentiableAt 𝕜 f₁ x)
-  (h₂ : DifferentiableAt 𝕜 f₂ x) :
-  partialDeriv 𝕜 v (f₁ - f₂) x = (partialDeriv 𝕜 v f₁) x - (partialDeriv 𝕜 v f₂) x := by
-
-  unfold partialDeriv
-  have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
-  rw [this]
-  rw [fderiv_sub h₁ h₂]
-  rfl
-
-
-theorem partialDeriv_sub₂_contDiffAt
-  {f₁ f₂ : E → F}
-  {v : E}
-  {x : E}
-  (h₁ : ContDiffAt 𝕜 1 f₁ x)
-  (h₂ : ContDiffAt 𝕜 1 f₂ x) :
-  partialDeriv 𝕜 v (f₁ - f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
-
-  obtain ⟨f₁', u₁, hu₁, _, hf₁'⟩ := contDiffAt_one_iff.1 h₁
-  obtain ⟨f₂', u₂, hu₂, _, hf₂'⟩ := contDiffAt_one_iff.1 h₂
-
-  apply Filter.eventuallyEq_iff_exists_mem.2
-  use u₁ ∩ u₂
-  constructor
-  · exact Filter.inter_mem hu₁ hu₂
-  · intro x hx
-    simp
-    apply partialDeriv_sub₂_differentiableAt 𝕜
-    exact (hf₁' x (Set.mem_of_mem_inter_left hx)).differentiableAt
-    exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
-
-
 theorem partialDeriv_compContLin
   {f : E → F}
   {l : F →L[𝕜] G}