diff --git a/Nevanlinna/comparingDerivatives.lean b/Nevanlinna/comparingDerivatives.lean deleted file mode 100644 index 7e7de02..0000000 --- a/Nevanlinna/comparingDerivatives.lean +++ /dev/null @@ -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 - diff --git a/Nevanlinna/harmonic.lean b/Nevanlinna/harmonic.lean deleted file mode 100644 index 6a29e6c..0000000 --- a/Nevanlinna/harmonic.lean +++ /dev/null @@ -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 \ No newline at end of file diff --git a/Nevanlinna/logabs.lean b/Nevanlinna/logabs.lean deleted file mode 100644 index dc92c6d..0000000 --- a/Nevanlinna/logabs.lean +++ /dev/null @@ -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 diff --git a/Nevanlinna/realHarmonic.lean b/Nevanlinna/realHarmonic.lean deleted file mode 100644 index 92db0ab..0000000 --- a/Nevanlinna/realHarmonic.lean +++ /dev/null @@ -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)