Update holomorphic_examples.lean

Nevanlinna/holomorphic_examples.lean

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

Nevanlinna/holomorphic_primitive2.lean

@@ -49,9 +49,6 @@ 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
@@ -124,7 +121,37 @@ theorem primitive_fderivAtBasepointZero
     apply h₁s
     exact h₂ε.1 hy
 
-  have t₀ {r : ℝ} (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
+
+  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
       apply ContinuousOn.intervalIntegrable
       apply ContinuousOn.comp
       exact hf
@@ -138,60 +165,62 @@ theorem primitive_fderivAtBasepointZero
       constructor
       · simp
         calc |x|
-      _ < ε := by
-        sorry
+        _ ≤ |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
       · simpa
-
-  have t₁ {r : ℝ}  (hr : r ∈ Metric.ball 0 ε) : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
+    have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by
       apply ContinuousOn.intervalIntegrable
       apply ContinuousOn.comp
       apply hf
       fun_prop
-    intro x hx
+      intro x _
       simpa
+    rw [← intervalIntegral.integral_sub t₀ t₁]
 
-
-  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
+    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
         funext x
         apply Complex.ext
         rw [Complex.add_re]
         simp
         simp
       rw [this]
-    apply Continuous.add
+      apply ContinuousOn.add
+      apply Continuous.continuousOn
       continuity
       fun_prop
-
-  have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
-    apply Continuous.intervalIntegrable
-    apply Continuous.comp
+      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
       exact hf
       fun_prop
-
-  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₁]
+      intro x _
+      apply h₂ε.2
+      simp
+      constructor
+      · simpa
+      · simpa
     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
@@ -752,12 +781,11 @@ theorem primitive_hasDerivAt
   apply hasDerivAt_const
 
 
-
-theorem primitive_differentiable
+theorem primitive_differentiableOn
   {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,20 +102,6 @@ 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}
@@ -153,6 +139,57 @@ 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}