import Nevanlinna.laplace variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace G₁] def Harmonic (f : ℂ → F) : Prop := (ContDiff ℝ 2 f) ∧ (∀ z, Δ f z = 0) def HarmonicAt (f : ℂ → F) (x : ℂ) : Prop := (ContDiffAt ℝ 2 f x) ∧ (Δ f =ᶠ[nhds x] 0) def HarmonicOn (f : ℂ → F) (s : Set ℂ) : Prop := (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) theorem HarmonicAt_iff {f : ℂ → F} {x : ℂ} : HarmonicAt f x ↔ ∃ s : Set ℂ, IsOpen s ∧ x ∈ s ∧ (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by constructor · intro hf obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl simp at h₃s₁ obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2) obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂ let s := s₁ ∩ s₂ use s constructor · exact IsOpen.inter h₁s₁ h₂s₂ · constructor · exact Set.mem_inter h₂s₁ h₃s₂ · constructor · exact h₃s₁.mono (Set.inter_subset_left s₁ s₂) · intro z hz exact h₂t₂ (h₁s₂ hz.2) · intro hyp obtain ⟨s, h₁s, h₂s, h₁f, h₂f⟩ := hyp constructor · apply h₁f.contDiffAt apply (IsOpen.mem_nhds_iff h₁s).2 h₂s · apply Filter.eventuallyEq_iff_exists_mem.2 use s constructor · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s · exact h₂f theorem HarmonicAt_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x := by constructor · intro h₁ constructor · exact ContDiffAt.congr_of_eventuallyEq h₁.1 (Filter.EventuallyEq.symm h) · exact Filter.EventuallyEq.trans (laplace_eventuallyEq' (Filter.EventuallyEq.symm h)) h₁.2 · intro h₁ constructor · exact ContDiffAt.congr_of_eventuallyEq h₁.1 h · exact Filter.EventuallyEq.trans (laplace_eventuallyEq' h) h₁.2 theorem HarmonicOn_of_locally_HarmonicOn {f : ℂ → F} {s : Set ℂ} (h : ∀ x ∈ s, ∃ (u : Set ℂ), IsOpen u ∧ x ∈ u ∧ HarmonicOn f (s ∩ u)) : HarmonicOn f s := by constructor · apply contDiffOn_of_locally_contDiffOn intro x xHyp obtain ⟨u, uHyp⟩ := h x xHyp use u exact ⟨ uHyp.1, ⟨uHyp.2.1, uHyp.2.2.1⟩⟩ · intro x xHyp obtain ⟨u, uHyp⟩ := h x xHyp exact (uHyp.2.2.2) x ⟨xHyp, uHyp.2.1⟩ theorem HarmonicOn_congr {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (hf₁₂ : ∀ x ∈ s, f₁ x = f₂ x) : HarmonicOn f₁ s ↔ HarmonicOn f₂ s := by constructor · intro h₁ constructor · apply ContDiffOn.congr h₁.1 intro x hx rw [eq_comm] exact hf₁₂ x hx · intro z hz have : f₁ =ᶠ[nhds z] f₂ := by unfold Filter.EventuallyEq unfold Filter.Eventually simp refine mem_nhds_iff.mpr ?_ use s constructor · exact hf₁₂ · constructor · exact hs · exact hz rw [← laplace_eventuallyEq this] exact h₁.2 z hz · intro h₁ constructor · apply ContDiffOn.congr h₁.1 intro x hx exact hf₁₂ x hx · intro z hz have : f₁ =ᶠ[nhds z] f₂ := by unfold Filter.EventuallyEq unfold Filter.Eventually simp refine mem_nhds_iff.mpr ?_ use s constructor · exact hf₁₂ · constructor · exact hs · exact hz rw [laplace_eventuallyEq this] exact h₁.2 z hz theorem harmonic_add_harmonic_is_harmonic {f₁ f₂ : ℂ → F} (h₁ : Harmonic f₁) (h₂ : Harmonic f₂) : Harmonic (f₁ + f₂) := by constructor · exact ContDiff.add h₁.1 h₂.1 · rw [laplace_add h₁.1 h₂.1] simp intro z rw [h₁.2 z, h₂.2 z] simp theorem harmonicOn_add_harmonicOn_is_harmonicOn {f₁ f₂ : ℂ → F} {s : Set ℂ} (hs : IsOpen s) (h₁ : HarmonicOn f₁ s) (h₂ : HarmonicOn f₂ s) : HarmonicOn (f₁ + f₂) s := by constructor · exact ContDiffOn.add h₁.1 h₂.1 · intro z hz rw [laplace_add_ContDiffOn hs h₁.1 h₂.1 z hz] rw [h₁.2 z hz, h₂.2 z hz] simp theorem harmonicAt_add_harmonicAt_is_harmonicAt {f₁ f₂ : ℂ → F} {x : ℂ} (h₁ : HarmonicAt f₁ x) (h₂ : HarmonicAt f₂ x) : HarmonicAt (f₁ + f₂) x := by constructor · exact ContDiffAt.add h₁.1 h₂.1 · apply Filter.EventuallyEq.trans (laplace_add_ContDiffAt' h₁.1 h₂.1) apply Filter.EventuallyEq.trans (Filter.EventuallyEq.add h₁.2 h₂.2) simp rfl theorem harmonic_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (h : Harmonic f) : Harmonic (c • f) := by constructor · exact ContDiff.const_smul c h.1 · rw [laplace_smul] dsimp intro z rw [h.2 z] simp theorem harmonic_iff_smul_const_is_harmonic {f : ℂ → F} {c : ℝ} (hc : c ≠ 0) : Harmonic f ↔ Harmonic (c • f) := by constructor · exact harmonic_smul_const_is_harmonic · nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)] exact fun a => harmonic_smul_const_is_harmonic a theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) : Harmonic (l ∘ f) := by constructor · -- Continuous differentiability apply ContDiff.comp exact ContinuousLinearMap.contDiff l exact h.1 · rw [laplace_compCLM] simp intro z rw [h.2 z] simp exact ContDiff.restrict_scalars ℝ h.1 theorem harmonicOn_comp_CLM_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ →L[ℝ] G} (hs : IsOpen s) (h : HarmonicOn f s) : HarmonicOn (l ∘ f) s := by constructor · -- Continuous differentiability apply ContDiffOn.continuousLinearMap_comp exact h.1 · -- Vanishing of Laplace intro z zHyp rw [laplace_compCLMAt] simp rw [h.2 z] simp assumption apply ContDiffOn.contDiffAt h.1 exact IsOpen.mem_nhds hs zHyp theorem harmonicAt_comp_CLM_is_harmonicAt {f : ℂ → F₁} {z : ℂ} {l : F₁ →L[ℝ] G} (h : HarmonicAt f z) : HarmonicAt (l ∘ f) z := by constructor · -- ContDiffAt ℝ 2 (⇑l ∘ f) z apply ContDiffAt.continuousLinearMap_comp exact h.1 · -- Δ (⇑l ∘ f) =ᶠ[nhds z] 0 obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁r obtain ⟨t, h₁t, h₂t⟩ := Filter.eventuallyEq_iff_exists_mem.1 h.2 obtain ⟨u, h₁u, h₂u, h₃u⟩ := mem_nhds_iff.1 h₁t apply Filter.eventuallyEq_iff_exists_mem.2 use s ∩ u constructor · apply IsOpen.mem_nhds exact IsOpen.inter h₂s h₂u constructor · exact h₃s · exact h₃u · intro x xHyp rw [laplace_compCLMAt] simp rw [h₂t] simp exact h₁u xHyp.2 apply (h₂r.mono h₁s).contDiffAt (IsOpen.mem_nhds h₂s xHyp.1) theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} : Harmonic f ↔ Harmonic (l ∘ f) := by constructor · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl rw [this] exact harmonic_comp_CLM_is_harmonic · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by funext z unfold Function.comp simp nth_rewrite 2 [this] exact harmonic_comp_CLM_is_harmonic theorem harmonicAt_iff_comp_CLE_is_harmonicAt {f : ℂ → F₁} {z : ℂ} {l : F₁ ≃L[ℝ] G₁} : HarmonicAt f z ↔ HarmonicAt (l ∘ f) z := by constructor · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl rw [this] exact harmonicAt_comp_CLM_is_harmonicAt · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by funext z unfold Function.comp simp nth_rewrite 2 [this] exact harmonicAt_comp_CLM_is_harmonicAt theorem harmonicOn_iff_comp_CLE_is_harmonicOn {f : ℂ → F₁} {s : Set ℂ} {l : F₁ ≃L[ℝ] G₁} (hs : IsOpen s) : HarmonicOn f s ↔ HarmonicOn (l ∘ f) s := by constructor · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl rw [this] exact harmonicOn_comp_CLM_is_harmonicOn hs · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by funext z unfold Function.comp simp nth_rewrite 2 [this] exact harmonicOn_comp_CLM_is_harmonicOn hs