simplify a match pattern nested within another function

Stream: new members

[ZhiKai Pong]

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
open InnerProductSpace
noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  -- get i-th component of `f`
   let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  fun i =>
    match i with
    | 0 => df 1 2 x - df 2 1 x
    | 1 => df 2 0 x - df 0 2 x
    | 2 => df 0 1 x - df 1 0 x

variable {ft : ℝ → ℝ³ → ℝ³}

example :  curl (fderiv ℝ (fun t => (ft t)) t 1) = fderiv ℝ (fun t => curl (ft t)) t 1 := by
  unfold curl
  ext x i
  simp
  fin_cases i
  simp -- how to simplify the match pattern nested within fderiv and fun?
  sorry

I have a match pattern nested within fderiv and fun=>. I want to extract the 0th component which is at the end of the expression, but I don't know how to substitute it into the expression. is there a way to do that or any suggestion on how to avoid this?

[ZhiKai Pong]

(I know I'll need differentiability conditions etc. to finish the proof)

[ZhiKai Pong]

sorry for bumping this, still stuck :(

if this is not a simple thing to resolve, I'd like to know what's needed (specific auxiliary lemmas etc.) or are there any clever ways around this

[ZhiKai Pong]

Essentially I have something of the form:

(fderiv ℝ (fun t x i => match i with ... ) t) 1 x 0

I think docs#fderiv_pi is closest to what I have but won't work in its current form, so I had a try at modifying it:

import Mathlib

variable
  {𝕜} [NontriviallyNormedField 𝕜]
  {W} [NormedAddCommGroup W] [NormedSpace 𝕜 W]
  {X} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
  {Y} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
  {ι : Type*} [Fintype ι] {Y' : ι → Type*} [∀ i, NormedAddCommGroup (Y' i)]
  [∀ i, NormedSpace 𝕜 (Y' i)] {Φ : X → ∀ i, Y' i} {φ : ∀ i, X → Y' i} {w : W} {x : X}

lemma fderiv_coord_apply (h : DifferentiableAt 𝕜 Φ x) :
    (fderiv 𝕜 (fun w x i => Φ x i) w) w x i = (fderiv 𝕜 (fun w x => Φ x i) w) w x := by
  sorry

lemma fderiv_pi_nested (h : ∀ i, DifferentiableAt 𝕜 (φ i) x) :
    (fderiv 𝕜 (fun w x i => φ i x) w) w x i = pi fun i => fderiv 𝕜 => (φ i) x :=
  sorry -- don't know how to state RHS

I'm not sure which form is the correct one for moving the x and the 0 inside the fderiv, or whether I'm on the wrong track. Any pointers appreciated

[Kyle Miller]

I tried looking at this a little last night, but I'm not too familiar with working with fderiv.

I got the sense that what you want to do is work with HasFDerivAt to do computations (see Mathematics in Lean, chapter 11). The general idea is that fderiv computes the correct derivative if the provided function is differentiable. Using HasFDerivAt keeps track of differentiability.

[Joseph Tooby-Smith]

I think for fderiv_pi_nested you want something like this no:

lemma fderiv_pi_nested (h : ∀ i, DifferentiableAt 𝕜 (φ i) x) :
    (fderiv 𝕜 (fun w x i => φ i x) w) w x i =
    (fderiv 𝕜 (fun w i => φ i x) w) w i :=
  sorry -- don't know how to state RHS

[ZhiKai Pong]

Joseph Tooby-Smith said:

I think for fderiv_pi_nested you want something like this no:

lemma fderiv_pi_nested (h : ∀ i, DifferentiableAt 𝕜 (φ i) x) :
    (fderiv 𝕜 (fun w x i => φ i x) w) w x i =
    (fderiv 𝕜 (fun w i => φ i x) w) w i :=
  sorry -- don't know how to state RHS

I've tried various forms of this but none of them seem to be able to see through the match pattern, or at least I don't know how to apply it. something like simp [fderiv_pi_nested] doesn't work nor does rw/apply

[Tomas Skrivan]

Ha of all things you are hitting the most obscure part of fderiv :)

In your original question, after the last simp you have on right hand side

  (fderiv ℝ
        (fun (t : ℝ) (x : ℝ³) (i : Fin 3) => ...))

It does not even matter that ... contains match statement there is a different problem lurking.

You are differentiating function of type ℝ → ℝ³ → ℝ³ i.e. domain is ℝ and codomain is ℝ³ → ℝ³. The problem is that ℝ³ → ℝ³ is not a normed space (i.e. you can't really equip it with a sensible norm) and unfortunately most of the theorems about fderiv, like fderiv_pi, are formulated for normed spaces. There is an ongoing push to generalize fderiv to topological vector spaces and that is the reason you are even allowed to write fderiv ℝ (fun (t : ℝ) (x : ℝ³) (i : Fin 3) => ...) and Lean does not complain that it can't synthesize NormedAddCommGroup (ℝ³ → ℝ³).

If you are not familiar with functional analysis, this probably did not make much sense. I would say that the take away is that you should double check that you are differentiating expressions that are values not functions. For examples, in fderiv ℝ (fun t => curl (ft t)) t 1 you are differentiating the expression curl (ft t) w.r.t. t but the type of curl (ft t) is ℝ³ → ℝ³. (Yes ℝ³ is a function as well, but the domain is finite type so it make sense to think about it as a value as well)

[Tomas Skrivan]

So you should reformulate the original problem as

example (x : ℝ³) : curl (fderiv ℝ (fun t => (ft t)) t 1) x = fderiv ℝ (fun t => curl (ft t) x) t 1 := ...

and the proof should be effectivelly

by
  unfold curl
  ext i
  simp [-fderiv_eq_smul_deriv]
  rw[fderiv_pi (ι:=Fin 3) (h:=by sorry)]
  fin_cases i  <;> /- simp and swap x and t derivativevs -/

For some reason, I'm having really hard time applying ContinuousLinearMap.pi_apply

[Tomas Skrivan]

Ughhh I think this is again the problem with the fact that Fin 3 → ℝ and EuclideanSpace ℝ (Fin 3) have different topology ... hmm in that case maybe using fderiv_pi is not the right move and some PiLp equivalent is necessary. Ahh this is so annoying an beginner unfriendly :(

[Tomas Skrivan]

Or can anyone tell me why the last simp call does not simplify (ContinuousLinearMap.pi f) 1 0 to f 0 1?

code

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
open InnerProductSpace
noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  -- get i-th component of `f`
  let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  fun i =>
    match i with
    | 0 => df 1 2 x - df 2 1 x
    | 1 => df 2 0 x - df 0 2 x
    | 2 => df 0 1 x - df 1 0 x

variable {ft : ℝ → ℝ³ → ℝ³}

example (x : ℝ³) : curl (fderiv ℝ (fun t => (ft t)) t 1) x = fderiv ℝ (fun t => curl (ft t) x) t 1 := by
  unfold curl
  ext i
  simp [-fderiv_eq_smul_deriv]
  rw[fderiv_pi (ι:=Fin 3) (h:=by sorry)]
  fin_cases i
  · simp[ContinuousLinearMap.pi_apply]
    sorry
  · sorry
  · sorry

[Tomas Skrivan]

Right, so I think the mathlib idiomatic way we should define curl as

noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  -- get i-th component of `f`
  let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  (WithLp.equiv 2 (Fin 3 → ℝ)).symm fun i =>
    match i with
    | 0 => df 1 2 x - df 2 1 x
    | 1 => df 2 0 x - df 0 2 x
    | 2 => df 0 1 x - df 1 0 x

Notice the (WithLp.equiv 2 (Fin 3 → ℝ)).symm. Then at some point we will be faced with

(fderiv ℝ
        (fun t =>
          (WithLp.equiv 2 (Fin 3 → ℝ)).symm fun i => ...

which can still be rewritten fderiv_pi but you are committing defeq abuse so some specialized version of fderiv_pi should exists. This is very similar situation we encountered in this thread and had to use PiLp.proj.

[ZhiKai Pong]

Tomas Skrivan said:

Or can anyone tell me why the last simp call does not simplify (ContinuousLinearMap.pi f) 1 0 to f 0 1?

code

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
open InnerProductSpace
noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  -- get i-th component of `f`
  let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  fun i =>
    match i with
    | 0 => df 1 2 x - df 2 1 x
    | 1 => df 2 0 x - df 0 2 x
    | 2 => df 0 1 x - df 1 0 x

variable {ft : ℝ → ℝ³ → ℝ³}

example (x : ℝ³) : curl (fderiv ℝ (fun t => (ft t)) t 1) x = fderiv ℝ (fun t => curl (ft t) x) t 1 := by
  unfold curl
  ext i
  simp [-fderiv_eq_smul_deriv]
  rw[fderiv_pi (ι:=Fin 3) (h:=by sorry)]
  fin_cases i
  · simp[ContinuousLinearMap.pi_apply]
    sorry
  · sorry
  · sorry

Joseph gave me some suggestions earlier, with some adaptations I can get the following:

code

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
open InnerProductSpace
noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  -- get i-th component of `f`
  let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  -- derivative of i-th component in j-th coordinate
  -- ∂fᵢ/∂xⱼ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  fun i =>
    match i with
    | 0 => df 1 2 x - df 2 1 x
    | 1 => df 2 0 x - df 0 2 x
    | 2 => df 0 1 x - df 1 0 x

variable {ft : ℝ → ℝ³ → ℝ³}

example (x : ℝ³) : curl (fderiv ℝ (fun t => (ft t)) t 1) x = fderiv ℝ (fun t => curl (ft t) x) t 1 := by
  ext i
  rw [fderiv_pi (ι:=Fin 3) (h:=by sorry)]
  symm
  change (fderiv ℝ (fun t => curl (ft t) x i) t) 1 = _
  unfold curl
  fin_cases i
  · simp [-fderiv_eq_smul_deriv]
    rw [fderiv_sub]
    sorry -- rw [IsSymmSndFDerivAt.eq] somehow
  · sorry
  · sorry

[ZhiKai Pong]

I guess that bypasses the match issue somehow (I'm still figuring out the difference). but then I think IsSymmSndFDerivAt.eq requires both t and x to be of the same type? does this mean what you said above is still a problem (t and x are in different domains )?

[Tomas Skrivan]

You want to use IsSymmSndFDerivAt.eq with

f := fun (tx : ℝ × ℝ³) => ft tx.1 tx.2
v := (1,0)
w := (0,EuclideanSpace.single i (1:ℝ))

[Tomas Skrivan]

But then you still need to turn it into the form you need which should be mathematically trivial but not practically. I think fderiv_uncurry will be useful at some point.

[ZhiKai Pong]

ok, more notations to learn... I'll try to go through these and see what I can come up with, thanks!

[Tomas Skrivan]

Yeah I'm sorry that it is so complicated. I don't have much time these days to browse Zulip so feel free to ping me next time.

[Aaron Liu]

btw there is a !₂[x, y, z] notation that you can use

[Aaron Liu]

Then you won't have to use a match maybe?

[Tomas Skrivan]

Correct, you can define curl as

import Mathlib

local notation "ℝ³" => EuclideanSpace ℝ (Fin 3)
open InnerProductSpace
noncomputable def curl (f : ℝ³ → ℝ³) :
    ℝ³ → ℝ³ := fun x =>
  let fi i x := ⟪f x, EuclideanSpace.single i (1:ℝ)⟫_ℝ
  let df i j x := fderiv ℝ (fi i) x (EuclideanSpace.single j (1:ℝ))
  !₂[df 1 2 x - df 2 1 x,
     df 2 0 x - df 0 2 x,
     df 0 1 x - df 1 0 x]

but I think that to make any progress in proofs you will have to use fin_cases i anyway.

[Tomas Skrivan]

The match is not really the problem. The main issues are

• you can't use fderiv_pi with (ι:=ℝ³)
• you should not be using fderiv_pi in the first place but some PiLp alternative
• how to actually apply IsSymmSndFDerivAt.eq in this scenarios i.e. how to get and apply curried version of IsSymmSndFDerivAt.eq