proving a function is differentiable

Stream: new members

[Nicholas Wilson]

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]

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

import Mathlib.Analysis.InnerProductSpace.Calculus -- added

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]

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

[Eric Wieser]

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
import Mathlib.Analysis.InnerProductSpace.Calculus -- added
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.const_add
      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]

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