How to do differentiation on concrete multivariable function

Stream: new members

[ZhiKai Pong]

Hi, I'm trying to learn how differentiation works in mathlib. I still don't really understand how fderiv works so I'm trying to construct some examples myself. The following is clearly wrong, and I would like to know whether stating something like this is possible and how to proceed.

$\frac{\partial}{\partial x}cos(x)sin(y) = -sin(x)sin(y)$

2 questions:

1. How to define a multivariable function? do I need to specify I'm in $\R^2$? (and how do I do that)
2. does deriv theorems carry over to fderiv? what's the correct syntax?

any tips and explanations appreciated!

import Mathlib

example : deriv (fun x : ℝ => Real.cos x) = (fun x => -Real.sin x) := by
  simp

example : fderiv ℝ (fun x : ℝ => Real.cos x) = (fun x => -Real.sin x) := by
  sorry --statement is wrong, type mismatch

example : fderiv ℝ (fun x y : ℝ => (Real.cos x)*(Real.sin y)) = (fun x y => (-Real.sin x)*(Real.sin y)) := by
  sorry --Don't know how to define cos(x)sin(y)

[ZhiKai Pong]

Oh if it's a function to $\R$ does that mean I don't have to actually use fderiv? is this the correct syntax?

import Mathlib

noncomputable

def some_f : ℝ → ℝ → ℝ := fun x y => (Real.cos x)*(Real.sin y)

example : deriv (fun x' => some_f x' y) x = (-Real.sin x)*(Real.sin y) := by

  sorry

[ZhiKai Pong]

simp [some_f] closes the goal. Is this stating what I'm wanting it to say? simp seems too powerful here, and I would like to understand what's going on under the hood.

I think I'll still want to know how to write this with fderiv, since my current goal is to work towards something related to vector calculus in $\R^3$.

[Ruben Van de Velde]

You can look what simp? [some_f] brings up - that probably gives an indication both about what API we have and if it uses the steps you'd expect mathematically

[ZhiKai Pong]

import Mathlib

variable (f : ℝ → ℝ)  (x : ℝ)

example : deriv f x = fderiv ℝ f x 1 := by rfl

example : deriv (fun x => Real.cos x) = (fun x => -Real.sin x) := by
  simp

example : fderiv ℝ (fun x => Real.cos x) 1 = (fun x => -Real.sin x) := by
  simp --doesn't work

maybe this illustrates the problem more clearly, how should I state the same thing with fderiv? I guess I don't really understand the function of the 1 in fderiv ℝ f x 1

[Aaron Liu]

The fderiv ℝ (fun x => Real.cos x) x 1 means you are taking the derivative of the function Real.cos at the point x in the direction of 1

[Aaron Liu]

This is useful if you are taking the jacobian in a higher dimension, because you can plug in a direction.

[ZhiKai Pong]

thanks, does that scale? if I put a 2 does the result also multiply by a factor of 2?

[ZhiKai Pong]

I found that there is fderiv_cos but I don't really understand how to use it. the goal state says ⇑(fderiv ℝ (fun x ↦ Real.cos x) 1) = fun x ↦ -Real.sin x and I don't understand how the coercion works

[Aaron Liu]

You want

example (x : ℝ) : fderiv ℝ (fun x => Real.cos x) x 1 = -Real.sin x := by
  simp

[ZhiKai Pong]

thanks! why is the fun necessary on the left but not on the right?

[Aaron Liu]

It is in fact not necessary on the left :)

example (x : ℝ) : fderiv ℝ Real.cos x 1 = -Real.sin x := by
  simp

[ZhiKai Pong]

oh I get it now, the x just substitutes in the fun, thanks a lot!

[ZhiKai Pong]

I've now moved on to try to prove the derivatives in $R^3$ commute along the standard basis. Using code I scraped together (tried my best to understand #new members > partial derivative of a vector field @ 💬 ) I came up with the following. I hope this is the correct statement, and I'm left with IsSymmSndFDerivAt ℝ f x and 2 pairs of goals involving DifferentiableAt . I wonder are those provable from properties of EuclideanSpace or would I need more properties. Would like some pointers as to how to proceed.

import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.InnerProductSpace.PiL2

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

macro "∂[" i:term "]" : term => `(fun f x => fderiv ℝ f x (EuclideanSpace.single $i (1:ℝ)))

open EuclideanSpace in
lemma deriv_commute (f : ℝ³ → ℝ³) (x : ℝ³) (v u: Fin 3) : ∂[u] (∂[v] f) x = ∂[v] (∂[u] f) x := by
  simp
  rw [fderiv_clm_apply, fderiv_clm_apply]
  simp
  rw [IsSymmSndFDerivAt.eq]
  sorry

[ZhiKai Pong]

import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.InnerProductSpace.PiL2

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

macro "∂[" i:term "]" : term => `(fun f x => fderiv ℝ f x (EuclideanSpace.single $i (1:ℝ)))

open EuclideanSpace in
lemma deriv_commute (f : ℝ³ → ℝ³) (x : ℝ³) (v u: Fin 3) (hf : ContDiff ℝ ⊤ f) : ∂[u] (∂[v] f) x = ∂[v] (∂[u] f) x := by
  simp
  rw [fderiv_clm_apply, fderiv_clm_apply]
  simp
  rw [IsSymmSndFDerivAt.eq]
  apply ContDiffAt.isSymmSndFDerivAt_of_omega
  apply hf.contDiffAt
  repeat
  show DifferentiableAt ℝ (fderiv ℝ f) x
  sorry
  apply differentiableAt_const

I got this far, I think I need (hf : ContDiff ℝ ⊤ f) to specify the function is $C^\infty$. Any suggestions on how to finish the final sorry?

[ZhiKai Pong]

import Mathlib.Analysis.Calculus.FDeriv.Symmetric

import Mathlib.Analysis.InnerProductSpace.PiL2

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (x : ℝ³) (hf : ContDiff ℝ ⊤ f): DifferentiableAt ℝ (fderiv ℝ f) x := by

  rw [contDiff_infty_iff_fderiv] at hf --doesn't work

I think this is what I need, but I'm not understanding why this rewrite doesn't work

[Aaron Liu]

Actually, ContDiff ℝ ⊤ f means f is analytic

[ZhiKai Pong]

Aaron Liu said:

analytic

Sorry I don't quite follow, I'm aware I can do this

import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.InnerProductSpace.PiL2

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (x : ℝ³) (hf : ContDiff ℝ ⊤ f): DifferentiableAt ℝ (fderiv ℝ f) x := by
  apply AnalyticAt.differentiableAt
  apply ContDiffAt.analyticAt
  apply ContDiff.contDiffAt

and get the goal state as

f : ℝ³ → ℝ³
x : ℝ³
hf : ContDiff ℝ ⊤ f
⊢ ContDiff ℝ ⊤ (fderiv ℝ f)

which is actually how I found contDiff_infty_iff_fderiv, but I'm not sure how to apply that. Am I missing something or are you suggesting something else?

[Aaron Liu]

Read carefully: docs#ContDiff takes a WithTop ENat, which has two tops. The higher top ("omega") is for analytic functions, and the lower top ("infinity") is for smooth (infinitely differentiable) functions.

[Aaron Liu]

If you open scoped ContDiff it'll print these differently.

[ZhiKai Pong]

I'm not from a maths background so please correct me if I'm wrong: analyticity is a stronger condition than infinitely differentiable so having (hf : ContDiff ℝ ⊤ f) should be strong enough. I want to show DifferentiableAt ℝ (fderiv ℝ f) x which just means the second derivative exists right? and contDiff_infty_iff_fderiv is applicable when f is analytic which is satisfied by hf? what am I missing with my reasoning?

[Aaron Liu]

import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.InnerProductSpace.PiL2

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (x : ℝ³) (hf : ContDiff ℝ ⊤ f) : DifferentiableAt ℝ (fderiv ℝ f) x := by
  have hf' : ContDiff ℝ (.some ⊤) f := hf.of_le le_top
  rw [contDiff_infty_iff_fderiv] at hf'
  apply hf'.right.contDiffAt.differentiableAt
  simp

[Yakov Pechersky]

More idiomatic would be have hf' : ContDiff ℝ (⊤ : ℕ∞) f := hf.of_le le_top, which matches the syntax of the contDiff_infty_iff_fderiv statement

[ZhiKai Pong]

Sorry if this looks a bit messy. Basically I'm trying to prove partial derivatives distribute over add but wrapped in some custom notation, and I would like to ask how do I apply pd_add keeping everything in EuclideanSpace. If pd_add is better defined in another form please let me know.

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
macro "∂[" i:term "]" : term => `(fun f x => fderiv ℝ f x (EuclideanSpace.single $i (1:ℝ)))

lemma pd_add  [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : EuclideanSpace ℝ (Fin n) → M) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
    ∂[u] (f1 + f2) = ∂[u] f1 + ∂[u] f2 := by
  sorry -- I can prove this

#check pd_add

noncomputable def grad (f : ℝ³ → ℝ) :
  ℝ³ → ℝ³ := fun x i =>
    ∂[i] f x

lemma grad_add (f1 f2 : ℝ³ → ℝ): grad (f1 + f2) = grad f1 + grad f2 := by
  unfold grad
  ext x i
  simp
  sorry -- how to use pd_add?

(edit: added differentiability assumptions)

[Sébastien Gouëzel]

You can do

lemma grad_add (f1 f2 : ℝ³ → ℝ): grad (f1 + f2) = grad f1 + grad f2 := by
  unfold grad
  ext x i
  rw [pd_add]
  rfl

But note that pd_add is not true, you need differentiability assumptions.

[ZhiKai Pong]

If I'm already in the state after simp is there a way to go back to the fun f => form?

[ZhiKai Pong]

context: divergence and curl are defined through some convoluted notation and after simp it's in a form that I can't apply pd_add directly e.g.

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
macro "∂[" i:term "]" : term => `(fun f x => fderiv ℝ f x (EuclideanSpace.single $i (1:ℝ)))

lemma pd_add  [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : EuclideanSpace ℝ (Fin n) → M) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
    ∂[u] (f1 + f2) = ∂[u] f1 + ∂[u] f2 := by
  sorry -- I can prove this

noncomputable def div (f : ℝ³ → ℝ³) :
  ℝ³ → ℝ := fun x =>
  -- get i-th component of `f`
  let fi i x := inner (f x) (EuclideanSpace.basisFun (Fin 3) ℝ i)
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i x := ∂[i] (fi i) x
  ∑ i, df i x

lemma div_add (f1 f2 : ℝ³ → ℝ³) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) : div (f1 + f2) = div f1 + div f2 := by
  unfold div
  simp
  ext x
  unfold Finset.sum
  simp
  sorry -- rw [pd_add] doesn't work

[Sébastien Gouëzel]

You can do a change to switch to whatever form you prefer. Or modify the statement of pd_add to have it in applied form, to make sure it applies after the simp.

[ZhiKai Pong]

Sorry what does applied form mean?

[Kevin Buzzard]

It means "don't say two functions are equal, say that for all v they have equal values at v"

[ZhiKai Pong]

Kevin Buzzard said:

It means "don't say two functions are equal, say that for all v they have equal values at v"

thanks you so much, this works now:

lemma pd_add  [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : EuclideanSpace ℝ (Fin n) → M) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2):
    ∀ v, ∂[u] (f1 + f2) v = ∂[u] f1 v + ∂[u] f2 v := by
  sorry -- I can prove this

#check pd_add

noncomputable def grad (f : ℝ³ → ℝ) :
  ℝ³ → ℝ³ := fun x i =>
    ∂[i] f x

lemma grad_add (f1 f2 : ℝ³ → ℝ) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) : grad (f1 + f2) = grad f1 + grad f2 := by
  unfold grad
  ext x i
  simp
  apply pd_add --works
  <;> assumption

[ZhiKai Pong]

Sorry its getting messier - I now have another layer of definition cderiv and I hope that I can avoid unfolding to the fderiv level. becasue of the way div is defined, the differentiation occurs at each coordinate. I tried to define pd_coord_add by pattern matching with the goal but the apply still doesn't work. I probably have to change the pd_coord_add definition somehow but I still don't fully grasp how the fun notation works

import Mathlib

noncomputable def cderiv [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (μ : Fin d) (f : EuclideanSpace ℝ (Fin d) → M) : EuclideanSpace ℝ (Fin d) → M :=
  (fun x => fderiv ℝ f x (EuclideanSpace.single μ (1:ℝ)))

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
macro "∂[" i:term "]" : term => `(fun f => cderiv $i f)

lemma pd_add  [NormedAddCommGroup M] [NormedSpace ℝ M] (f1 f2 : EuclideanSpace ℝ (Fin d) → M) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2):
    ∀ v, ∂[u] (f1 + f2) v = ∂[u] f1 v + ∂[u] f2 v := by
  sorry -- v ∈ EuclideanSpace ℝ (Fin d)

lemma pd_coord_add (f1 f2 : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
    ∀ v, (∂[u] (fun v => f1 v i + f2 v i) v) = (∂[u] (fun v => f1 v i) v) + (∂[u] (fun v => f2 v i) v) := by
  sorry -- I think I need this for explicit coordinates

#check pd_coord_add


noncomputable def div (f : ℝ³ → ℝ³) :
  ℝ³ → ℝ := fun x =>
  -- get i-th component of `f`
  let fi i x := inner (f x) (EuclideanSpace.basisFun (Fin 3) ℝ i)
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i x := ∂[i] (fi i) x
  ∑ i, df i x

lemma div_add (f1 f2 : ℝ³ → ℝ³) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) : div (f1 + f2) = div f1 + div f2 := by
  unfold div
  simp
  ext x
  unfold Finset.sum
  simp
  apply pd_coord_add --tried to define pd_coord_add by pattern matching but doesn't work

[ZhiKai Pong]

essentially I don't really know how to proceed when the fun is nested within something else

[ZhiKai Pong]

Summarizing my current understanding:

import Mathlib

noncomputable def cderiv [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (μ : Fin d) (f : EuclideanSpace ℝ (Fin d) → M) : EuclideanSpace ℝ (Fin d) → M :=
  (fun x => fderiv ℝ f x (EuclideanSpace.single μ (1:ℝ)))

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
macro "∂[" i:term "]" : term => `(fun f => cderiv $i f)

lemma pd_add  [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f1 f2 : EuclideanSpace ℝ (Fin n) → M) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
  ∂[u] (f1 + f2) = ∂[u] f1 + ∂[u] f2 := by
  sorry -- I can prove this

lemma pd_add_applied  [NormedAddCommGroup M] [NormedSpace ℝ M]
    (f1 f2 : EuclideanSpace ℝ (Fin n) → M) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
  ∂[u] (f1 + f2) v = ∂[u] f1 v + ∂[u] f2 v:= by
  sorry -- I can prove this

lemma pd_fun_add (f1 f2 : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
    (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
  (∂[u] (fun x => (f1 + f2) x) v) = (∂[u] f1 v) + (∂[u] f2 v) := by
  sorry -- how do I state the fun x => version?

#check pd_add

noncomputable def grad (f : ℝ³ → ℝ) :
  ℝ³ → ℝ³ := fun x i =>
    ∂[i] f x

example (f1 f2 : ℝ³ → ℝ) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
    grad (f1 + f2) = grad f1 + grad f2 := by
  unfold grad
  ext x i
  rw [pd_add] -- rw works for fun =>
  rfl
  apply hf1
  apply hf2

example (f1 f2 : ℝ³ → ℝ) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
    grad (f1 + f2) = grad f1 + grad f2 := by
  unfold grad
  ext x i
  fin_cases i <;>
  . simp                 -- rw doesn't work after simp
    apply pd_add_applied -- apply can handle Fin indexing but pattern still has to be exact match
    apply hf1
    apply hf2

/- -------------------------------------------- -/

noncomputable def tmp (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
    -- get i-th component of `f`
    let fi i x := inner (f x) (EuclideanSpace.basisFun (Fin 3) ℝ i)
    -- derivative of i-th component in j-th coordinate
    -- ∂fᵢ/∂xⱼ
    let df i := ∂[i] (fi i) x
    fun i =>
      match i with
      | 0 => df 0 + df 1
      | 1 => df 1 + df 2
      | 2 => df 2 + df 0

example (f1 f2 : ℝ³ → ℝ³) (hf1 : ContDiff ℝ ⊤ f1) (hf2 : ContDiff ℝ ⊤ f2) :
    tmp (f1 + f2) = tmp f1 + tmp f2 := by
  unfold tmp
  ext x i
  fin_cases i
  simp                --necessary
  -- rw [pd_fun_add]  --doesn't work
  apply pd_fun_add    --apply has to be exact match, is there a partial apply or some alternative way of rewriting?

[ZhiKai Pong]

Am I correct that the applied form cannot be used for rewriting? because of the way tmp is defined, I have to simp to simply the definitions, then I run into the issue where I can't rw the goal (of the form:

cderiv 0 (fun x => f1 x 0 + f2 x 0) x + ... = cderiv 0 (fun x => f1 x 0) x + cderiv 0 (fun x => f2 x 0) x + ...

I want to rw this using a helper lemma, but I'm not sure how to state that.

[ZhiKai Pong]

I think I figured it out, I couldn't get rid of the (fun f => ...) because of the way the macro is defined.
I'll have to change to macro to

macro "∂[" i:term "]" : term => `(cderiv $i)

then it should work. apply and rw can't "see through" the fun notation

[ZhiKai Pong]

back to differentiability arguments: I now have the following

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    DifferentiableAt ℝ (fun x => (fderiv ℝ f x) (EuclideanSpace.single v 1)) x := by
  have hf' : ContDiff ℝ (⊤ : ℕ∞) f := hf.of_le le_top
  rw [contDiff_infty_iff_fderiv] at hf'
  apply ContDiffAt.differentiableAt
  apply ContDiff.contDiffAt
  sorry --apply hf'.right doesn't work

[ZhiKai Pong]

I feel like I'm getting more and more confused by fun x => notation... Any hints as to how to proceed from here?

[Aaron Liu]

Maybe docs#contDiff_pi

[ZhiKai Pong]

Neither docs#contDiff_pi nor docs#contDiff_single works :(

[ZhiKai Pong]

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    DifferentiableAt ℝ (fun x => (fderiv ℝ f x) (EuclideanSpace.single v 1)) x := by
  have hf' : ContDiff ℝ (⊤ : ℕ∞) f := hf.of_le le_top
  rw [contDiff_infty_iff_fderiv] at hf'
  apply ContDiffAt.differentiableAt
  apply ContDiff.contDiffAt
  apply contDiff_euclidean.mpr
  sorry --apply contDiff_single somehow?

I think apply contDiff_euclidean.mpr is the right call, but still unable to use contDiff_single

[ZhiKai Pong]

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ fun x =>
      (fderiv ℝ (fun x => f x (u : Fin 3)) x) (EuclideanSpace.single (v : Fin 3) (1 : ℝ)) := by
  have hf' : ContDiff ℝ (⊤ : ℕ∞) f := hf.of_le le_top
  rw [contDiff_infty_iff_fderiv] at hf'
  sorry --some modified form of fderiv_pi?

After playing around some more with the definitions, I ended up with this expression which I think just says ∂fᵤ/∂xᵥ is differentiable if f is infinitely differentiable. At this point I think I've tried enough things to say I'm at a point where I have to further understand lean syntax to make appropriate modifications to existing mathlib theorems to proceed, or I'm missing something obvious with the maths. would appreciate some guidance as to whether this is just a syntax thing or is this something deeper.

[Tomas Skrivan]

I think you want to use docs#DifferentiableAt.clm_apply to move the evaluation of the linear map outside of DifferentiableAt. Unfortunately, I don't have the time to look into the details right now.

[ZhiKai Pong]

Tomas Skrivan said:

I think you want to use docs#DifferentiableAt.clm_apply to move the evaluation of the linear map outside of DifferentiableAt. Unfortunately, I don't have the time to look into the details right now.

thank you so much, I think I'll have to read up on the difference between comp and apply to really understand how this works.

[ZhiKai Pong]

The final goal
Differentiable ℝ (fderiv ℝ fun x ↦ f x w)

looks a lot like docs#fderiv_pi, but the primed version which doesn't exist yet. Not sure whether there's an easy way to switch between them, I'll try to understand the difference between the primed and non-primed version of similar theorems

[ZhiKai Pong]

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (h : Differentiable ℝ (fderiv ℝ f)) :
    Differentiable ℝ (fderiv ℝ fun x => f x i) := by
  sorry

After removing all the clutter what I need is essentially the above. I think what it's saying and the way to do it on paper is:

the fderiv of each component is just projection composed with fderiv, since both are differentiable so the fderiv of each component follows from fderiv of f.

but I'm not sure how to state this in lean.

[Tomas Skrivan]

All there examples are solvable by fun_prop after adding these two theorems

theorem ContDiff.differentiable_fderiv (f : X → Y) (hf : ContDiff 𝕜 2 f) :
    Differentiable 𝕜 (fun x => fderiv 𝕜 f x) := ...

and

theorem EuclideanSpace.contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) := ...

Now you can solve your examples with fun_prop (disch:=decide). The (disch:=decide) is necessary for fun_prop to show that 2 ≤ ⊤. Also you can drop your assumption from ContDiff ℝ ⊤ f to ContDiff ℝ 2 f.

[Tomas Skrivan]

Full code

code

import Mathlib

variable
  {𝕜} [RCLike 𝕜]
  {X} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  {Y} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
  {Z} [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]

theorem lin_isometry_apply_differentiable (g : X → Y) (hg : Differentiable 𝕜 g) (f : Y ≃ₗᵢ[𝕜] Z) :
  Differentiable 𝕜 (fun x => f (g x)) := by fun_prop

@[fun_prop]
theorem ContDiff.differentiable_fderiv (f : X → Y) (hf : ContDiff 𝕜 2 f) :
    Differentiable 𝕜 (fun x => fderiv 𝕜 f x) := by
  have h : ∀ x, fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 X Y (iteratedFDeriv 𝕜 1 f x) := by
    sorry
  simp[h]
  apply lin_isometry_apply_differentiable
  apply ContDiff.differentiable_iteratedFDeriv
    (n:=2) (hm:=by decide) (hf:=hf)

@[fun_prop]
theorem EuclideanSpace.contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) := sorry

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fun x => (fderiv ℝ f x) (EuclideanSpace.single v 1)) := by
  fun_prop (disch:=decide)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ 2 f) :
    Differentiable ℝ (fderiv ℝ fun x => f x i) := by
  fun_prop

example {u v : Fin 3} (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ fun x =>
      (fderiv ℝ (fun x => f x u) x) (EuclideanSpace.single v (1 : ℝ)) := by
  fun_prop (disch:=decide)

What is left to show is that

fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 X Y (iteratedFDeriv 𝕜 1 f x)

I don't have experience working with multilinear maps so I would appreciate if someone helps out.

And

theorem EuclideanSpace.contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) := sorry

which is effectively contDiff_apply but under L2 norm rather than L∞ norm.

[Tomas Skrivan]

Yeah sorry, it looks like there is some API missing and doing what you are trying to do is messier then it should be.

[Tomas Skrivan]

I reduced ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) to showing that WithLp.linearEquiv 2 𝕜 (ι → 𝕜) is a bounded/continuous map which I'm unable to find as a statement in mathlib

import Mathlib

variable
  {𝕜} [RCLike 𝕜]

theorem euclideanSpace_contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff 𝕜 ⊤ (fun f : EuclideanSpace 𝕜 ι => f i) := by
  have h : (fun f : EuclideanSpace 𝕜 ι => f i)
           =
           (fun f : ι → 𝕜 => f i) ∘ (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm := by rfl
  rw[h]
  apply ContDiff.comp
  exact contDiff_apply 𝕜 𝕜 i
  apply IsBoundedLinearMap.contDiff
  constructor
  · apply LinearMap.isLinear
  · sorry

[Aaron Liu]

import Mathlib

theorem PiLp.contDiff_proj_apply {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    {ι : Type*} [Fintype ι] {f : ι → Type*} [∀ i, NormedAddCommGroup (f i)]
    [∀ i, NormedSpace 𝕜 (f i)] {n : WithTop ENat} (p : ENNReal) [Fact (1 ≤ p)] (i : ι) :
    ContDiff 𝕜 n fun p : PiLp p f => p i :=
  (PiLp.proj p (𝕜 := 𝕜) f i).contDiff

[ZhiKai Pong]

Tomas Skrivan said:

I reduced ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) to showing that WithLp.linearEquiv 2 𝕜 (ι → 𝕜) is a bounded/continuous map which I'm unable to find as a statement in mathlib

The fun_prop doesn't work for the second example after replacing euclideanSpace_contDiff_apply in the longer code above, only difference I can tell is the ContDiff ℝ n is changed to ContDiff 𝕜 ⊤ and fun_prop can't synthesize that?

works after I change the assumption back to hf : ContDiff ℝ ⊤ f

[ZhiKai Pong]

many thanks to both, I'll try to chew through the above

[ZhiKai Pong]

full code

code

import Mathlib

variable
  {𝕜} [RCLike 𝕜]
  {X} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  {Y} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
  {Z} [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]

theorem lin_isometry_apply_differentiable (g : X → Y) (hg : Differentiable 𝕜 g) (f : Y ≃ₗᵢ[𝕜] Z) :
  Differentiable 𝕜 (fun x => f (g x)) := by fun_prop

@[fun_prop]
theorem ContDiff.differentiable_fderiv (f : X → Y) (hf : ContDiff 𝕜 2 f) :
    Differentiable 𝕜 (fun x => fderiv 𝕜 f x) := by
  have h : ∀ x, fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 X Y (iteratedFDeriv 𝕜 1 f x) := by
    sorry
  simp[h]
  apply lin_isometry_apply_differentiable
  apply ContDiff.differentiable_iteratedFDeriv
    (n:=2) (hm:=by decide) (hf:=hf)

@[fun_prop]
theorem euclideanSpace_contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff 𝕜 ⊤ (fun f : EuclideanSpace 𝕜 ι => f i) := by
  have h : (fun f : EuclideanSpace 𝕜 ι => f i)
           =
           (fun f : ι → 𝕜 => f i) ∘ (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm := by rfl
  rw[h]
  apply ContDiff.comp
  exact contDiff_apply 𝕜 𝕜 i
  apply IsBoundedLinearMap.contDiff
  constructor
  · apply LinearMap.isLinear
  · sorry

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fun x => (fderiv ℝ f x) (EuclideanSpace.single v 1)) := by
  fun_prop (disch:=decide)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fderiv ℝ fun x => f x i) := by
  fun_prop (disch:=decide)

example {u v : Fin 3} (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ fun x =>
      (fderiv ℝ (fun x => f x u) x) (EuclideanSpace.single v (1 : ℝ)) := by
  fun_prop (disch:=decide)

[Tomas Skrivan]

With the addition of Aaron's proof:

code

import Mathlib

variable
  {𝕜} [RCLike 𝕜]
  {X} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  {Y} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
  {Z} [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]

theorem lin_isometry_apply_differentiable (g : X → Y) (hg : Differentiable 𝕜 g) (f : Y ≃ₗᵢ[𝕜] Z) :
  Differentiable 𝕜 (fun x => f (g x)) := by fun_prop

@[fun_prop]
theorem ContDiff.differentiable_fderiv (f : X → Y) (hf : ContDiff 𝕜 2 f) :
    Differentiable 𝕜 (fun x => fderiv 𝕜 f x) := by
  have h : ∀ x, fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 X Y (iteratedFDeriv 𝕜 1 f x) := by
        intro x; ext dx; simp; rfl
  simp[h]
  apply lin_isometry_apply_differentiable
  apply ContDiff.differentiable_iteratedFDeriv
    (n:=2) (hm:=by decide) (hf:=hf)

@[fun_prop]
theorem euclideanSpace_contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff 𝕜 ⊤ (fun f : EuclideanSpace 𝕜 ι => f i) :=
  (PiLp.proj 2 (𝕜 := 𝕜) (fun _ => 𝕜) i).contDiff

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fun x => (fderiv ℝ f x) (EuclideanSpace.single v 1)) := by
  fun_prop (disch:=decide)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fderiv ℝ fun x => f x i) := by
  fun_prop (disch:=decide)

example {u v : Fin 3} (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ fun x =>
      (fderiv ℝ (fun x => f x u) x) (EuclideanSpace.single v (1 : ℝ)) := by
  fun_prop (disch:=decide)

So the only missing piece is to show that fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 X Y (iteratedFDeriv 𝕜 1 f x)

edit: removed all sorries

[ZhiKai Pong]

I was working on this before you posted - wondering whether this leads anywhere or am I completely off the tracks:

attempt

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

section --copied setup from Mathlib.Analysis.Calculus.FDeriv.Prod
open ContinuousLinearMap

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
variable {f f₀ f₁ g : E → F}
variable {f' f₀' f₁' g' : E →L[𝕜] F}
variable (e : E →L[𝕜] F)
variable {x : E}
variable {s t : Set E}
variable {L L₁ L₂ : Filter E}

variable {ι : Type*} [Fintype ι] {F' : ι → Type*} [∀ i, NormedAddCommGroup (F' i)]
  [∀ i, NormedSpace 𝕜 (F' i)] {φ : ∀ i, E → F' i} {φ' : ∀ i, E →L[𝕜] F' i} {Φ : E → ∀ i, F' i}
  {Φ' : E →L[𝕜] ∀ i, F' i}

theorem fderiv_pi' (h : DifferentiableAt 𝕜 Φ x):
    fderiv 𝕜 Φ x = pi fun i => (fderiv 𝕜 fun x => Φ x i) x:= by
  apply HasFDerivAt.fderiv
  apply hasFDerivAt_pi''
  intro i
  rw [differentiableAt_pi] at h
  exact (h i).hasFDerivAt

end

lemma aux (f : ℝ³ → ℝ³) (h : DifferentiableAt ℝ f x):
    (fderiv ℝ fun x => f x i) x = (ContinuousLinearMap.proj i).comp (fderiv ℝ f x) := by
  rw [fderiv_pi', ContinuousLinearMap.proj_pi]
  apply h

example (f : ℝ³ → ℝ³) (h : Differentiable ℝ f) :
    DifferentiableAt ℝ (fderiv ℝ fun x => f x i) x := by
  have eq : (fun x => fderiv ℝ (fun x ↦ f x i) x)
      = (fun x => (ContinuousLinearMap.proj i).comp (fderiv ℝ f x)) := by
    ext x
    rw [aux]
    apply h
  rw [eq] --failed: the x is "seaprable" on the LHS but not on the RHS
  apply DifferentiableAt.clm_comp --does this lead anywhere?

[Tomas Skrivan]

It is essentially how the fun_prop proof works

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ 2 f) :
    DifferentiableAt ℝ (fderiv ℝ fun x => f x i) x := by
  have eq : (fderiv ℝ (fun x ↦ f x i))
      = (fun x => (ContinuousLinearMap.proj i).comp (fderiv ℝ f x)) := by
    ext x
    rw [aux]
    apply hf.differentiable
    decide
  rw[eq] --the x is "seaprable" on the LHS but not on the RHS
  apply DifferentiableAt.clm_comp --does this lead anywhere?
  · fun_prop
  · apply ContDiff.differentiable_fderiv
    apply hf

I had to change few things

• you need stronger assumption on f such as ContDiff ℝ 2 f
• rw does not play well with binders (i.e. fun x => ... ) so the statement of eq has to be fderiv ℝ (fun x ↦ f x i)) = ... (i.e. without fun x => ...)
• include the theorem ContDiff.differentiable_fderiv I gave above

You can call fun_prop right after rw[eq], with set_option trace.Meta.Tactic.fun_prop true you can actually see what fun_prop is doing:

    [Meta.Tactic.fun_prop] [✅️] applying: DifferentiableAt.clm_comp
...
        [Meta.Tactic.fun_prop] [✅️] applying: differentiableAt_const
...
        [Meta.Tactic.fun_prop] [✅️] applying: Differentiable.differentiableAt
...
            [Meta.Tactic.fun_prop] [✅️] applying: ContDiff.differentiable_fderiv
...
                [Meta.Tactic.fun_prop] [✅️] applying: hf : ContDiff ℝ 2 f

[ZhiKai Pong]

Amazing thanks!

[ZhiKai Pong]

I found this which imo simplifies a lot:

theorem ContDiff.differentiable_fderiv' (f : X → Y) (hf : ContDiff 𝕜 2 f) :
    Differentiable 𝕜 (fun x => fderiv 𝕜 f x) := by
  have hf' : ContDiff 𝕜 (1+1) f := hf
  rw [contDiff_succ_iff_fderiv] at hf'
  apply hf'.right.right.differentiable
  decide

(is there a better way to write the have statement? writing 2 = 1+1 is kind of stupid)

[Kevin Buzzard]

(Just think yourself lucky that we're not using Russell and Whitehead's foundations, or else it would take 300 pages to justify 2 = 1 + 1)

[Aaron Liu]

rw [show 2 = 1 + 1 by norm_num] at hf?

[Ruben Van de Velde]

You can use docs#one_add_one_eq_two

[Aaron Liu]

That's from nng

[ZhiKai Pong]

Aaron Liu said:

rw [show 2 = 1 + 1 by norm_num] at hf?

I actually have to write
rw [show (2 : WithTop ℕ∞) = 1 + 1 by norm_num] at hf

[ZhiKai Pong]

but that's just a minor inconvenience, I'm happy with what I've got, thanks all

[Tomas Skrivan]

I made PR #24056 that sets up ContDiff with fun_prop. You should be able to compose derivatives as much you want now:

import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.InnerProductSpace.PiL2

example (f : ℝ → ℝ) (h : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fun a => fderiv ℝ (deriv^[3] (deriv (fun x : ℝ => f (x^3 + x)))) a (a*a)) := by
  fun_prop (disch:=decide)

I should also add

theorem EuclideanSpace.contDiff_apply {ι} [Fintype ι] (i : ι) :
    ContDiff ℝ n (fun f : EuclideanSpace 𝕜 ι => f i) :=

not sure where it should go and how to name it.

[Tomas Skrivan]

Ok, I think the PR #24056 is ready. I had to reformulate few theorems such that they work better with fun_prop and I would appreciate to look over it such that I follow correct naming convention. Most of the time I just added ' but in few cases _one, _succ or _fun might be more appropriate.

On that PR you should be able now to do

import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.WithLp
import Mathlib.Analysis.InnerProductSpace.PiL2

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ (fun x => (fderiv ℝ f x) (EuclideanSpace.single v 1)) := by
  fun_prop (disch:=decide)

example (f : ℝ³ → ℝ³) (hf : ContDiff ℝ 2 f) :
    Differentiable ℝ (fderiv ℝ fun x => f x i) := by
  fun_prop

example {u v : Fin 3} (f : ℝ³ → ℝ³) (hf : ContDiff ℝ ⊤ f) :
    Differentiable ℝ fun x =>
      (fderiv ℝ (fun x => f x u) x) (EuclideanSpace.single v (1 : ℝ)) := by
  fun_prop (disch:=decide)

@ZhiKai Pong Let me know if there are other proof of differentiability/smoothess you struggle with. I think everything what you do should be solvable by fun_prop(potentially with (disch:=aesop) or similar tactic) but it might be the case that it is not set up correctly.

[Alok Singh]

Dumb q @Tomas Skrivan : have you tried grind as the discharger? (afk or id try)

[Tomas Skrivan]

I still do not know what kind of goals is grind supposed to solve. The subgoals of fun_prop are usually inequalities or non-equality on reals or set membership. Is grind good for that?

[Tomas Skrivan]

I would expect that grind, as many other tactics, would need some kind of set up, like tagging appropriate theorems with an attribute. So far I haven't seen anything like that in Mathlib.

[Kevin Buzzard]

The tactic isn't even finished yet, so it's premature for mathlib to start adapting to it