kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

All done.

This commit is contained in:
Stefan Kebekus 2024-06-03 13:35:53 +02:00
parent 40659c2f17
commit c2c730e510
2 changed files with 37 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Nevanlinna/complexHarmonic.lean
View File

@ -407,11 +407,7 @@ theorem log_normSq_of_holomorphicOn_is_harmonicOn
-- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s -- HarmonicOn (Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f) s
apply holomorphicOn_is_harmonicOn hs apply holomorphicOn_is_harmonicOn hs
apply? exact DifferentiableOn.clog h₁ h₃
exact h₁ z
theorem log_normSq_of_holomorphic_is_harmonic theorem log_normSq_of_holomorphic_is_harmonic
{f : ℂ → ℂ} {f : ℂ → ℂ}

42
Nevanlinna/laplace.lean
View File

@ -65,22 +65,52 @@ theorem laplace_add_ContDiffOn
simp simp
intro x hx intro x hx
have hf₁ : ∀ z ∈ s, DifferentiableAt ℝ f₁ z := by
intro z hz
convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn h₁ one_le_two
have hf₂ : ∀ z ∈ s, DifferentiableAt ℝ f₂ z := by
intro z hz
convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn h₂ one_le_two
have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by have : partialDeriv ℝ 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ 1 f₁) + (partialDeriv ℝ 1 f₂) := by
sorry apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· exact IsOpen.mem_nhds hs hx
· intro z hz
apply partialDeriv_add₂_differentiableAt
exact hf₁ z hz
exact hf₂ z hz
rw [partialDeriv_eventuallyEq ℝ this] rw [partialDeriv_eventuallyEq ℝ this]
have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
sorry let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
sorry let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂] rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]
have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
sorry apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· exact IsOpen.mem_nhds hs hx
· intro z hz
apply partialDeriv_add₂_differentiableAt
exact hf₁ z hz
exact hf₂ z hz
rw [partialDeriv_eventuallyEq ℝ this] rw [partialDeriv_eventuallyEq ℝ this]
have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
sorry let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
sorry let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄] rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
-- I am super confused at this point because the tactic 'ring' does not work. -- I am super confused at this point because the tactic 'ring' does not work.