Update harmonic.lean

This commit is contained in:
Stefan Kebekus 2024-04-26 16:02:56 +02:00
parent 187781f971
commit 1918cc0139
1 changed files with 216 additions and 15 deletions

View File

@ -1,5 +1,7 @@
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.LineDeriv.Basic import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
-- Harmonic functions on the plane -- Harmonic functions on the plane
@ -7,19 +9,187 @@ import Mathlib.Analysis.Calculus.LineDeriv.Basic
noncomputable def laplace' : () → () := by noncomputable def laplace' : () → () := by
intro f intro f
let f₁ := fun x ↦ lineDeriv f x ⟨1, 0⟩ let f₁ := fun x ↦ lineDeriv f x 1
let g₁ := fun x ↦ lineDeriv f x ⟨1, 0⟩ let f₁₁ := fun x ↦ lineDeriv f₁ x 1
let f₁₁ := fun x ↦ lineDeriv f₁ x ⟨1, 0⟩ let f₂ := fun x ↦ lineDeriv f x Complex.I
let f₂ := fun x ↦ lineDeriv f x ⟨0, 1⟩ let f₂₂ := fun x ↦ lineDeriv f₂ x Complex.I
let f₂₂ := fun x ↦ lineDeriv f₂ x ⟨0, 1⟩
exact f₁₁ + f₂₂ exact f₁₁ + f₂₂
example : ∀ z₀ : , laplace' (fun z ↦ z.re) z₀ = 0 := by example : laplace' (fun z ↦ z.re) = fun z ↦ 0 := by
intro z₀
unfold laplace' lineDeriv
unfold laplace' lineDeriv
simp simp
conv =>
lhs
intro x
arg 1
intro t
rw [deriv_add] <;> tactic => try fun_prop
simp
rfl
example : laplace' (fun z ↦ (z*z).re) = fun z ↦ 0 := by
unfold laplace' lineDeriv
simp
conv =>
lhs
intro x
simp
arg 1
arg 1
intro t
rw [deriv_sub] <;> tactic => try fun_prop
simp
rw [deriv_mul] <;> tactic => try fun_prop
simp
rw [deriv_add] <;> tactic => try fun_prop
simp
conv =>
lhs
intro x
arg 1
rw [deriv_add] <;> tactic => try fun_prop
rw [deriv_add] <;> tactic => try fun_prop
simp
rw [one_add_one_eq_two]
conv =>
lhs
intro x
arg 2
conv =>
arg 1
intro t
rw [deriv_sub] <;> tactic => try fun_prop
rw [deriv_mul] <;> tactic => try fun_prop
simp
rw [deriv_mul] <;> tactic => try fun_prop
simp
rw [deriv_add] <;> tactic => try fun_prop
rw [deriv_add] <;> tactic => try fun_prop
simp
conv =>
lhs
intro x
rw [deriv_add] <;> tactic => try fun_prop
rw [deriv_add] <;> tactic => try fun_prop
simp
group
example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
unfold laplace' lineDeriv
simp
conv =>
lhs
arg 1
intro x
arg 1
intro t
arg 1
intro t₁
rw [Complex.exp_add]
rw [Complex.exp_add]
conv =>
lhs
arg 1
intro x
arg 1
intro t
simp
conv =>
rhs
arg 1
intro x₁
rw [Complex.exp_re]
simp
rw [Real.deriv_exp]
simp
conv =>
lhs
arg 1
intro x
simp
rhs
arg 1
intro x
rw [Complex.exp_re]
conv =>
lhs
lhs
intro x
rhs
lhs
intro x₁
simp
simp
conv =>
lhs
rhs
intro x
lhs
intro t
arg 1
intro t₁
rw [Complex.exp_add]
rw [Complex.exp_add]
simp
rw [Complex.exp_re]
rw [Complex.exp_im]
simp
conv =>
lhs
rhs
intro x
lhs
intro t
simp
-- oops
conv =>
lhs
rw [Complex.exp_add]
rw [deriv_mul] <;> tactic => try fun_prop
sorry
rw [deriv_add] <;> tactic => try fun_prop
sorry sorry
noncomputable def laplace : () → () := by noncomputable def laplace : () → () := by
@ -39,13 +209,33 @@ noncomputable def laplace : () → () := by
example : ∀ z₀ : , laplace (fun z ↦ (z*z).re) z₀ = 0 := by example : ∀ z₀ : , laplace (fun z ↦ (z*z).re) z₀ = 0 := by
intro z₀ intro z₀
unfold laplace unfold laplace
dsimp [lineDeriv] dsimp [lineDeriv]
simp simp
conv =>
sorry lhs
lhs
arg 1
intro t
rw [deriv_sub] <;> tactic => try fun_prop
rw [deriv_mul] <;> tactic => try fun_prop
rw [deriv_const_add]
simp
ring_nf
conv =>
lhs
rhs
arg 1
intro t
rw [deriv_sub] <;> tactic => try fun_prop
rw [deriv_const]
rw [deriv_mul] <;> tactic => try fun_prop
rw [deriv_const_add]
simp
ring_nf
rw [deriv_const_add, deriv_sub] <;> try fun_prop
simp
example : ∀ z₀ : , laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by example : ∀ z₀ : , laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
intro z₀ intro z₀
@ -57,8 +247,19 @@ example : ∀ z₀ : , laplace (fun z ↦ (Complex.exp z).re) z₀ = 0 := by
sorry sorry
example : deriv (fun (t : ) ↦ 2 + t) = fun (t : ) ↦ 1 := by example : deriv (fun (t : ) ↦ 2 + t) = fun (t : ) ↦ 1 := by
-- Does not work: simp [deriv.add] -- in my experience with the library, more results are stated about
sorry -- `HasDerivAt` than about equality of `deriv`
rw [deriv_eq]
intro x
-- I guessed the name `HasDerivAt.add`, which didn't work, but the
-- autocomplete dropdown showed `add_const` and `const_add` too
apply HasDerivAt.const_add
-- I assumed this was in the library, and `apply?` found it
exact hasDerivAt_id' x
example : laplace (fun z ↦ (Complex.exp z).re) = 0 := by example : laplace (fun z ↦ (Complex.exp z).re) = 0 := by
have : (fun z => (Complex.exp z).re) = (fun z => Real.exp z.re * Real.cos z.im) := by have : (fun z => (Complex.exp z).re) = (fun z => Real.exp z.re * Real.cos z.im) := by