Clean up
This commit is contained in:
Stefan Kebekus
parent
b26256d84e
commit
b5cf426b7f
|
|
@ -1,17 +0,0 @@
|
|||
import Mathlib.Data.Fin.Tuple.Basic
|
||||
import Mathlib.Analysis.Complex.Basic
|
||||
import Mathlib.Analysis.Complex.TaylorSeries
|
||||
import Mathlib.Analysis.Calculus.LineDeriv.Basic
|
||||
import Mathlib.Analysis.Calculus.ContDiff.Defs
|
||||
import Mathlib.Analysis.Calculus.FDeriv.Basic
|
||||
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
|
||||
|
||||
|
||||
lemma l₁ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
|
||||
∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = iteratedFDeriv ℝ 2 f z ![a, b] := by
|
||||
sorry
|
||||
|
||||
lemma l₂ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
|
||||
∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w ↦ (fderiv ℝ f w) a) z) b := by
|
||||
sorry
|
||||
|
||||
|
|
@ -1,445 +0,0 @@
|
|||
import Mathlib.Analysis.Complex.Basic
|
||||
import Mathlib.Analysis.Calculus.LineDeriv.Basic
|
||||
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
|
||||
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
|
||||
import Mathlib.Analysis.Calculus.ContDiff.Basic
|
||||
import Mathlib.Analysis.Calculus.Deriv.Linear
|
||||
import Mathlib.Analysis.Complex.Conformal
|
||||
import Mathlib.Analysis.Calculus.Conformal.NormedSpace
|
||||
import Mathlib.Analysis.Complex.RealDeriv
|
||||
|
||||
/RealDeriv.lean
|
||||
-- Harmonic functions on the plane
|
||||
|
||||
variable {f : ℂ → ℂ} {e' : ℂ} {z : ℝ} {h : HasDerivAt f e' z}
|
||||
|
||||
example : 1 = 0 := by
|
||||
|
||||
let XX := HasDerivAt.real_of_complex h
|
||||
sorry
|
||||
|
||||
|
||||
noncomputable def lax (f : ℂ → ℝ) (z : ℂ) : ℝ :=
|
||||
iteratedFDeriv ℝ 1 f z ![Complex.I]
|
||||
|
||||
example : lax (fun z ↦ z.re) = fun z ↦ 1 := by
|
||||
unfold lax
|
||||
simp
|
||||
funext x
|
||||
|
||||
let XX := HasDerivAt.real_of_complex
|
||||
|
||||
sorry
|
||||
|
||||
|
||||
noncomputable def laplace (f : ℂ → ℝ) (z : ℂ) : ℝ :=
|
||||
iteratedFDeriv ℝ 2 f z ![1, 1] + iteratedFDeriv ℝ 2 f z ![Complex.I, Complex.I]
|
||||
|
||||
|
||||
example : laplace (fun z ↦ z.re) = fun z ↦ 0 := by
|
||||
|
||||
unfold laplace
|
||||
rw [iteratedFDeriv_succ_eq_comp_left]
|
||||
rw [iteratedFDeriv_succ_eq_comp_left]
|
||||
rw [iteratedFDeriv_zero_eq_comp]
|
||||
simp
|
||||
|
||||
have : Fin.tail ![Complex.I, Complex.I] = ![Complex.I] := by
|
||||
rfl
|
||||
rw [this]
|
||||
|
||||
rw [deriv_comp]
|
||||
|
||||
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
|
||||
|
||||
open Complex ContinuousLinearMap
|
||||
|
||||
open scoped ComplexConjugate
|
||||
|
||||
variable {z : ℂ} {f : ℂ → ℂ}
|
||||
|
||||
#check deriv_comp_const_add
|
||||
|
||||
theorem DifferentiableAt_conformalAt (h : DifferentiableAt ℂ f z) :
|
||||
ConformalAt f z := by
|
||||
|
||||
let XX := (h.hasFDerivAt.restrictScalars ℝ).fderiv
|
||||
|
||||
let f₁ := fun x ↦ lineDeriv ℝ f x 1
|
||||
let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
|
||||
|
||||
have t₁ : deriv (fun (t : ℂ) => f (z + t)) 0 = deriv f z := by
|
||||
rw [deriv_comp_const_add]
|
||||
simp
|
||||
simp
|
||||
exact h
|
||||
have t'₁ : deriv (fun (t : ℝ) => f (z + ↑t)) 0 = deriv f z := by
|
||||
sorry
|
||||
|
||||
have : f₁ z = deriv f z := by
|
||||
dsimp [f₁]
|
||||
unfold lineDeriv
|
||||
simp
|
||||
exact t'₁
|
||||
|
||||
have : f₂ z = deriv f z := by
|
||||
dsimp [f₂]
|
||||
unfold lineDeriv
|
||||
simp
|
||||
|
||||
exact t'₁
|
||||
|
||||
|
||||
/-
|
||||
simp at f₂
|
||||
|
||||
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
|
||||
apply isConformalMap_complex_linear
|
||||
simpa only [Ne, ext_ring_iff]
|
||||
-/
|
||||
|
||||
example : laplace' (fun z ↦ (Complex.exp z).re) = fun z ↦ 0 := by
|
||||
|
||||
let f := fun z ↦ (Complex.exp z).re
|
||||
let f₁ := fun x ↦ lineDeriv ℝ f x 1
|
||||
let fz := fun x ↦ deriv f
|
||||
|
||||
|
||||
|
||||
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
|
||||
rw [deriv_sub] <;> tactic => try fun_prop
|
||||
rw [deriv_mul] <;> tactic => try fun_prop
|
||||
rw [deriv_mul] <;> tactic => try fun_prop
|
||||
simp
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
-- oops
|
||||
|
||||
|
||||
|
||||
|
||||
conv =>
|
||||
lhs
|
||||
|
||||
rw [Complex.exp_add]
|
||||
|
||||
rw [deriv_mul] <;> tactic => try fun_prop
|
||||
|
||||
|
||||
|
||||
sorry
|
||||
|
||||
rw [deriv_add] <;> tactic => try fun_prop
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
sorry
|
||||
|
||||
noncomputable def laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
|
||||
intro f
|
||||
|
||||
let F : ℝ × ℝ → ℝ := fun x ↦ f (x.1 + x.2 * Complex.I)
|
||||
|
||||
let e₁ : ℝ × ℝ := ⟨1, 0⟩
|
||||
let e₂ : ℝ × ℝ := ⟨0, 1⟩
|
||||
|
||||
let F₁ := fun x ↦ lineDeriv ℝ F x e₁
|
||||
let F₁₁ := fun x ↦ lineDeriv ℝ F₁ x e₁
|
||||
let F₂ := fun x ↦ lineDeriv ℝ F x e₂
|
||||
let F₂₂ := fun x ↦ lineDeriv ℝ F₂ x e₂
|
||||
|
||||
exact fun x ↦ F₁₁ ⟨x.1, x.2⟩ + F₂₂ ⟨x.1, x.2⟩
|
||||
|
||||
|
||||
example : ∀ z₀ : ℂ, laplace (fun z ↦ (z*z).re) z₀ = 0 := by
|
||||
intro z₀
|
||||
unfold laplace
|
||||
dsimp [lineDeriv]
|
||||
simp
|
||||
conv =>
|
||||
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
|
||||
intro z₀
|
||||
|
||||
unfold laplace
|
||||
dsimp [lineDeriv]
|
||||
simp
|
||||
|
||||
sorry
|
||||
|
||||
example : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
|
||||
-- in my experience with the library, more results are stated about
|
||||
-- `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
|
||||
have : (fun z => (Complex.exp z).re) = (fun z => Real.exp z.re * Real.cos z.im) := by
|
||||
funext z
|
||||
rw [Complex.exp_re]
|
||||
rw [this]
|
||||
|
||||
unfold laplace
|
||||
simp
|
||||
|
||||
have F₁ : (fun (x : ℝ × ℝ) => lineDeriv ℝ (fun (t : ℝ × ℝ) => Real.exp t.1 * Real.cos t.2) x ⟨1, 0⟩) = ((fun (x : ℝ × ℝ) => (Real.exp x.1 * Real.cos x.2))) := by
|
||||
funext x
|
||||
dsimp [lineDeriv]
|
||||
simp
|
||||
left
|
||||
have t₁ : (fun x_1 => Real.exp (x.1 + x_1)) = (fun x_1 => Real.exp x.1 * Real.exp x_1) := by
|
||||
funext t
|
||||
exact Real.exp_add x.1 t
|
||||
rw [t₁]
|
||||
simp
|
||||
|
||||
have F₂ : (fun (x : ℝ × ℝ) => lineDeriv ℝ (fun (t : ℝ × ℝ) => Real.exp t.1 * Real.sin t.2) x ⟨0, 1⟩) = ((fun (x : ℝ × ℝ) => (Real.exp x.1 * Real.cos x.2))) := by
|
||||
funext x
|
||||
|
||||
dsimp [lineDeriv]
|
||||
simp
|
||||
|
||||
have t₁ : (fun t => Real.sin (x.2 + t)) = (Real.sin ∘ (fun t => x.2 + t)) := by
|
||||
rfl
|
||||
rw [t₁]
|
||||
rw [deriv.comp]
|
||||
simp
|
||||
|
||||
have : deriv (fun (t : ℝ) ↦ 2 + t) = fun (t : ℝ) ↦ 1 := by
|
||||
simp [deriv.add]
|
||||
sorry
|
||||
|
||||
|
||||
|
||||
rw [this]
|
||||
simp
|
||||
· exact Real.differentiableAt_sin
|
||||
· -- DifferentiableAt ℝ (fun t => x.2 + t) 0
|
||||
sorry
|
||||
|
||||
|
||||
rw [this]
|
||||
|
||||
sorry
|
||||
|
||||
have : deriv (fun x_1 => Real.exp (x_1 + x_1)) 0 = 2 := by
|
||||
simp
|
||||
group
|
||||
|
||||
|
||||
rw [this]
|
||||
simp
|
||||
|
||||
have : deriv (fun t => Real.cos (x.2 + t * y.2)) = (fun t => -y.2 * Real.sin (x.2 + t * y.2)) := by
|
||||
funext t₀
|
||||
have t₁ : (fun t => Real.cos (x.2 + t * y.2)) = (Real.cos ∘ (fun t => x.2 + t * y.2)) := by
|
||||
rfl
|
||||
rw [t₁]
|
||||
rw [deriv.comp]
|
||||
simp
|
||||
· group
|
||||
· exact Real.differentiableAt_cos
|
||||
· simp
|
||||
|
||||
simp
|
||||
simp
|
||||
|
||||
sorry
|
||||
|
||||
let XX := fderiv ℝ (fun (x : ℝ × ℝ) => Real.exp x.1 * Real.cos x.2)
|
||||
simp at XX
|
||||
|
||||
have : fderiv ℝ fun x => Real.exp x.1 * Real.cos x.2 = 0 := by
|
||||
|
||||
sorry
|
||||
|
||||
funext z
|
||||
simp
|
||||
funext
|
||||
|
||||
let ZZ := Complex.exp_re z
|
||||
sorry
|
||||
|
|
@ -1,56 +0,0 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
open ComplexConjugate
|
||||
|
||||
/- logAbs of a product is sum of logAbs of factors -/
|
||||
|
||||
lemma logAbs_mul : ∀ z₁ z₂ : ℂ, z₁ ≠ 0 → z₂ ≠ 0 → Real.log (Complex.abs (z₁ * z₂)) = Real.log (Complex.abs z₁) + Real.log (Complex.abs z₂) := by
|
||||
intro z₁ z₂ z₁Hyp z₂Hyp
|
||||
rw [Complex.instNormedFieldComplex.proof_2 z₁ z₂]
|
||||
exact Real.log_mul ((AbsoluteValue.ne_zero_iff Complex.abs).mpr z₁Hyp) ((AbsoluteValue.ne_zero_iff Complex.abs).mpr z₂Hyp)
|
||||
|
||||
lemma absAndProd : ∀ z : ℂ, Complex.abs z = Real.sqrt ( (z * conj z).re ) := by
|
||||
intro z
|
||||
simp
|
||||
rfl
|
||||
|
||||
#check Complex.log_mul_eq_add_log_iff
|
||||
#check Complex.arg_eq_pi_iff
|
||||
|
||||
lemma logAbsXX : ∀ z : ℂ, z ≠ 0 → Real.log (Complex.abs z) = (1 / 2) * Complex.log z + (1 / 2) * Complex.log (conj z) := by
|
||||
intro z z₁Hyp
|
||||
|
||||
by_cases argHyp : Complex.arg z = Real.pi
|
||||
|
||||
-- Show pos: Complex.arg z = Real.pi
|
||||
have : conj z = z := by
|
||||
apply Complex.conj_eq_iff_im.2
|
||||
rw [Complex.arg_eq_pi_iff] at argHyp
|
||||
exact argHyp.right
|
||||
rw [this]
|
||||
sorry
|
||||
|
||||
-- Show pos: Complex.arg z ≠ Real.pi
|
||||
have t₁ : Complex.abs z = Real.sqrt (Complex.normSq z) := by
|
||||
exact rfl
|
||||
rw [t₁]
|
||||
|
||||
have t₂ : 0 ≤ Complex.normSq z := by
|
||||
exact Complex.normSq_nonneg z
|
||||
rw [ Real.log_sqrt t₂ ]
|
||||
|
||||
|
||||
have t₃ : Real.log (Complex.normSq z) = Complex.log (Complex.normSq z) := by
|
||||
apply Complex.ofReal_log
|
||||
exact t₂
|
||||
simp
|
||||
rw [t₃]
|
||||
rw [Complex.normSq_eq_conj_mul_self]
|
||||
|
||||
have t₄ : conj z ≠ 0 := by
|
||||
exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr z₁Hyp
|
||||
|
||||
let XX := Complex.log_mul_eq_add_log_iff this z₁Hyp
|
||||
|
||||
|
||||
|
||||
sorry
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
import Mathlib.Analysis.Calculus.LineDeriv.Basic
|
||||
import Mathlib.Analysis.Calculus.ContDiff.Defs
|
||||
|
||||
noncomputable def Real.laplace : (ℝ × ℝ → ℝ) → (ℝ × ℝ → ℝ) := by
|
||||
intro f
|
||||
|
||||
let f₁ := fun x ↦ lineDeriv ℝ f x ⟨1,0⟩
|
||||
let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x ⟨1,0⟩
|
||||
let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
|
||||
let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x ⟨0,1⟩
|
||||
|
||||
exact f₁₁ + f₂₂
|
||||
|
||||
|
||||
def Harmonic (f : ℝ × ℝ → ℝ) : Prop :=
|
||||
(ContDiff ℝ 2 f) ∧ (∀ x, Real.laplace f x = 0)
|
||||
Loading…
Reference in New Issue