import Nevanlinna.complexHarmonic import Nevanlinna.holomorphicAt import Nevanlinna.holomorphic_primitive import Nevanlinna.mathlibAddOn theorem CauchyRiemann₆ {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {z : E} : (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by constructor · -- Direction "→" intro h constructor · exact DifferentiableAt.restrictScalars ℝ h · unfold partialDeriv conv => intro e left rw [DifferentiableAt.fderiv_restrictScalars ℝ h] simp rw [← mul_one Complex.I] rw [← smul_eq_mul] conv => intro e right right rw [DifferentiableAt.fderiv_restrictScalars ℝ h] simp · -- Direction "←" intro ⟨h₁, h₂⟩ apply (differentiableAt_iff_restrictScalars ℝ h₁).2 use { toFun := fderiv ℝ f z map_add' := fun x y => ContinuousLinearMap.map_add (fderiv ℝ f z) x y map_smul' := by simp intro m x have : m = m.re + m.im • Complex.I := by simp rw [this, add_smul, add_smul, ContinuousLinearMap.map_add] congr simp rw [smul_assoc, smul_assoc, ContinuousLinearMap.map_smul (fderiv ℝ f z) m.2] congr exact h₂ x } rfl theorem CauchyRiemann₇ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {z : ℂ} : (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by constructor · intro hf constructor · exact (CauchyRiemann₆.1 hf).1 · let A := (CauchyRiemann₆.1 hf).2 1 simp at A exact A · intro ⟨h₁, h₂⟩ apply CauchyRiemann₆.2 constructor · exact h₁ · intro e have : Complex.I • e = e • Complex.I := by rw [smul_eq_mul, smul_eq_mul] exact CommMonoid.mul_comm Complex.I e rw [this] have : e = e.re + e.im • Complex.I := by simp rw [this, add_smul, partialDeriv_add₁, partialDeriv_add₁] simp rw [← smul_eq_mul] have : partialDeriv ℝ ((e.re : ℝ) • Complex.I) f = partialDeriv ℝ ((e.re : ℂ) • Complex.I) f := by rfl rw [← this, partialDeriv_smul₁ ℝ] have : (e.re : ℂ) = (e.re : ℝ) • (1 : ℂ) := by simp rw [this, partialDeriv_smul₁ ℝ] have : partialDeriv ℝ ((e.im : ℂ) * Complex.I) f = partialDeriv ℝ ((e.im : ℝ) • Complex.I) f := by rfl rw [this, partialDeriv_smul₁ ℝ] simp rw [h₂] rw [smul_comm] congr rw [mul_assoc] simp nth_rw 2 [smul_comm] rw [← smul_assoc] simp have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp rw [this, partialDeriv_smul₁ ℝ] simp /- A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic function. -/ theorem harmonic_is_realOfHolomorphic {f : ℂ → ℝ} (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 reg₂f : ContDiff ℝ 2 f := by apply contDiff_iff_contDiffAt.mpr intro z exact (hf z).1 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).1 1 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).1 Complex.I have reg₁g : ContDiff ℝ 1 g := by dsimp [g] apply ContDiff.sub exact reg₁f_1 apply ContDiff.const_smul' exact reg₁f_I have reg₁ : Differentiable ℂ g := by intro z apply CauchyRiemann₇.2 constructor · apply Differentiable.differentiableAt apply ContDiff.differentiable exact reg₁g rfl · dsimp [g] rw [partialDeriv_sub₂, partialDeriv_sub₂] simp dsimp [f_1, f_I] rw [partialDeriv_smul'₂, partialDeriv_smul'₂] 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_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) z)] rw [← A] simp --Differentiable ℝ (partialDeriv ℝ _ f) repeat apply ContDiff.differentiable apply contDiff_iff_contDiffAt.mpr exact fun w ↦ partialDeriv_contDiffAt ℝ (hf w).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 have regF : Differentiable ℂ F := by apply Differentiable.add apply primitive_differentiable reg₁ simp 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'] exact rfl exact reg₁ use F constructor · -- ∀ (z : ℂ), HolomorphicAt F z intro z apply HolomorphicAt_iff.2 use Set.univ constructor · exact isOpen_const · 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 apply eq_of_fderiv_eq B A _ 0 C intro x rw [fderiv.comp] simp apply ContinuousLinearMap.ext intro w simp rw [pF''] dsimp [g, f_1, f_I, partialDeriv] simp have : w = w.re • 1 + w.im • Complex.I := by simp nth_rw 3 [this] rw [(fderiv ℝ f x).map_add] 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