## Stream: new members

### Topic: proving a function is differentiable

#### Nicholas Wilson (Nov 08 2023 at 10:59):

I have a local function that I'm computing derivatives on. How do I prove it is actually differentiable?

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.Calculus.Deriv.Pow
open Complex
open Real

theorem whatever ( x y: ℝ ) : True := by
let f := fun (w:ℝ)  ↦ (normSq (sin (x+w*I )))
let df := deriv f y
have hfd : Differentiable ℝ f := by sorry -- how to prove this?
trivial


#### Ruben Van de Velde (Nov 08 2023 at 12:36):

I only seem to have succeeded in reducing it to a less obvious goal:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.Calculus.Deriv.Pow

open Complex
open Real

theorem whatever ( x y: ℝ ) : True := by
let f := fun (w:ℝ)  ↦ (normSq (sin (x+w*I )))
let df := deriv f y
have hfd : Differentiable ℝ f := by
simp only [normSq_eq_abs, ← Complex.norm_eq_abs]
-- apply? suggests
-- refine Differentiable.norm_sq ?𝕜 ?hf
-- but get stuck on finding an instance before ?𝕜 is filled in, so specify it
refine Differentiable.norm_sq ℂ ?hf
suffices Differentiable ℂ fun w => Complex.sin (x + w * I) by
-- Is this true?
sorry
refine Differentiable.csin ?hf.hc -- apply?
refine Differentiable.const_add ?hf.hc.hf (x : ℂ) -- apply?
refine Differentiable.mul_const ?hf.hc.hf.ha I -- apply?
exact differentiable_id' -- apply?
trivial


#### Eric Wieser (Nov 08 2023 at 12:44):

I recommend you jump straight to showing HasDerivAt, as I did here

#### Eric Wieser (Nov 08 2023 at 13:00):

That looks as follows:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Exponential
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.Calculus.Deriv.Pow
open Complex
open Real

theorem whatever ( x y: ℝ ) : True := by
let f := fun (w:ℝ)  ↦ (normSq (sin (x+w*I )))
have hfd : ∀ x, HasDerivAt f _ x := by
intro x
simp only [normSq_eq_abs, ← Complex.norm_eq_abs]
-- we are missing HasDerivAt.norm_sq: #8268 !
apply HasFDerivAt.hasDerivAt; apply HasFDerivAt.norm_sq; apply HasDerivAt.hasFDerivAt
simp_rw [←Function.comp_def Complex.sin]
apply HasDerivAt.comp
· apply Complex.hasDerivAt_sin
apply HasDerivAt.mul_const
apply HasDerivAt.ofReal_comp
apply hasDerivAt_id
-- the () here are a workaround for a Lean bug
simp [(ContinuousLinearMap.comp_apply), (ContinuousLinearMap.smulRight_apply)] at hfd
have : Differentiable ℝ f := fun x => (hfd x).differentiableAt
have hd_eq := deriv_eq hfd
sorry


#### Eric Wieser (Nov 08 2023 at 13:20):

(#8267 makes the simp more poweful, but doesn't fix the bug)

Last updated: Dec 20 2023 at 11:08 UTC