nevanlinna/Nevanlinna/harmonicAt.lean

331 lines
9.5 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Nevanlinna.laplace
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace F₁]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace G]
variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace 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
· 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_isOpen
(f : → F) :
IsOpen { x : | HarmonicAt f x } := by
rw [← subset_interior_iff_isOpen]
intro x hx
simp at hx
obtain ⟨s, h₁s, h₂s, h₃s⟩ := HarmonicAt_iff.1 hx
use s
constructor
· simp
constructor
· exact h₁s
· intro x hx
simp
rw [HarmonicAt_iff]
use s
· exact h₂s
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 harmonicAt_smul_const_is_harmonicAt
{f : → F}
{x : }
{c : }
(h : HarmonicAt f x) :
HarmonicAt (c • f) x := by
constructor
· exact ContDiffAt.const_smul c h.1
· rw [laplace_smul]
have A := Filter.EventuallyEq.const_smul h.2 c
simp at A
assumption
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 harmonicAt_iff_smul_const_is_harmonicAt
{f : → F}
{x : }
{c : }
(hc : c ≠ 0) :
HarmonicAt f x ↔ HarmonicAt (c • f) x := by
constructor
· exact harmonicAt_smul_const_is_harmonicAt
· nth_rewrite 2 [((eq_inv_smul_iff₀ hc).mpr rfl : f = c⁻¹ • c • f)]
exact fun a => harmonicAt_smul_const_is_harmonicAt 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