nevanlinna/Nevanlinna/harmonic.lean

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