Update complexHarmonic.lean
This commit is contained in:
parent
71ad6aa67e
commit
aeda1e981d
|
@ -49,7 +49,7 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
|
||||||
· have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
|
· have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
|
||||||
rw [this]
|
rw [this]
|
||||||
exact harmonic_comp_CLM_is_harmonic
|
exact harmonic_comp_CLM_is_harmonic
|
||||||
· have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
|
· have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
|
||||||
funext z
|
funext z
|
||||||
unfold Function.comp
|
unfold Function.comp
|
||||||
simp
|
simp
|
||||||
|
@ -129,6 +129,12 @@ theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ
|
||||||
exact holomorphic_is_harmonic h
|
exact holomorphic_is_harmonic h
|
||||||
|
|
||||||
|
|
||||||
|
theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
|
||||||
|
Harmonic (Complex.conjCLE ∘ f) := by
|
||||||
|
apply harmonic_iff_comp_CLE_is_harmonic.1
|
||||||
|
exact holomorphic_is_harmonic h
|
||||||
|
|
||||||
|
|
||||||
theorem log_normSq_of_holomorphic_is_harmonic
|
theorem log_normSq_of_holomorphic_is_harmonic
|
||||||
{f : ℂ → ℂ}
|
{f : ℂ → ℂ}
|
||||||
(h₁ : Differentiable ℂ f)
|
(h₁ : Differentiable ℂ f)
|
||||||
|
|
Loading…
Reference in New Issue