Vector calculus

Stream: PhysLean

[ZhiKai Pong]

although there is gradient in mathlib, will it still be useful to state the usual 3D gradient? (I assume making it compatible with SpaceTime requires this anyway) so we can state things like

theorem curl_of_grad_eq_zero (x: SpaceTime)
    (A : SpaceTime → EuclideanSpace ℝ (Fin 3)) : ∇× (∇ A) x = 0 := by
  sorry

and things like the Laplacian operator

[ZhiKai Pong]

/-- The gradient of a function `SpaceTime → EuclideanSpace ℝ (Fin 3)`. -/
def spaceGrad (f : SpaceTime → EuclideanSpace ℝ (Fin 3)) :
    SpaceTime → EuclideanSpace ℝ (Fin 3) := fun x j =>
  match j with
  | 0 => deriv 0 (fun y => f y 0) x
  | 1 => deriv 1 (fun y => f y 1) x
  | 2 => deriv 2 (fun y => f y 2) x

@[inherit_doc spaceGrad]
scoped[SpaceTime] notation "∇" => spaceGrad

attempt following how spaceDiv and spaceCurl are defined

[ZhiKai Pong]

I realized f should be from SpaceTime to R (scalar function)... I'll correct this in the next PR

[ZhiKai Pong]

I'm working on some vector calculus identities, should we assume everything is ContDiff 𝕜 ⊤ f or keep all the assumptions as minimal as possible?

[ZhiKai Pong]

i.e. for example only assume ContDiff 𝕜 2 f for deriv_commute

[ZhiKai Pong]

Or maybe the identities should have minimal assumption, then we prove the physical functions satisfies those?

[Kevin Buzzard]

The philosophy in mathlib is to stick to minimal assumptions as far as is reasonably possible, and in mathlib this has its advantages. At the very least it seems pointless putting more hypothesis in a theorem than the proof uses!

[Joseph Tooby-Smith]

I would like it if for div and curl we could have ∇ × f and ∇ ⬝ f instead of ∇× f and ∇⬝ f (note the different spacings). I couldn't find any easy way to do this with notation or marcos.

[Joseph Tooby-Smith]

Actually never mind, something like:

macro (name := divNotation) "∇" "⬝" f:term:100  : term => `(div $f)

works. I was trying

macro (name := divNotation) "∇ ⬝" f:term:100  : term => `(div $f)

which doesn't work.

[ZhiKai Pong]

trying to define the Laplacian, which one of ∇² and Δ is more commonly used? I'm thinking of using ∇² for the scalar and Δ for the vector Laplacian, not sure if that's a good idea.

[Joseph Tooby-Smith]

I don't really have an opinion here, so don't mind too much. Both seem equally as common.

But I will say (somewhat related), at some point it would be really nice to have the (scalar) Laplacian written in e.g. spherical coordinates and an easy way to go between cartesian and spherical coordinates on space. I think this will be very useful in situations with spherical symmetry.

[Joseph Tooby-Smith]

I think your suggestion for using ∇² for the scalar and Δ for the vector is good - though if possible I think it would be nicer to use the same notation for both

[ZhiKai Pong]

Joseph Tooby-Smith said:

I don't really have an opinion here, so don't mind too much. Both seem equally as common.

But I will say (somewhat related), at some point it would be really nice to have the (scalar) Laplacian written in e.g. spherical coordinates and an easy way to go between cartesian and spherical coordinates on space. I think this will be very useful in situations with spherical symmetry.

is spherical coordinates in mathlib? I found docs#polarCoord but don't seem to find spherical coordinates.

[ZhiKai Pong]

ok I think it's safe to say it's just not a thing in mathlib :sweat_smile: #maths > polar coordinates @ 💬 is pretty much the only discussion on this

[ZhiKai Pong]

Joseph Tooby-Smith said:

I think your suggestion for using ∇² for the scalar and Δ for the vector is good - though if possible I think it would be nicer to use the same notation for both

I don't think having the same notation works, lean throws an error

hmm nevermind it might work, let me do some more testing

[Tomas Skrivan]

There are multiple ways to have the same notation for different things. I think there are three main approaches:

• overloaded notation
• use notation for a specialized typeclass and provide instances for every use case. The canonical example is + and the associated type class HAdd
• write custom elaborator, this is most flexible but requires meta programming

I think the typeclass approach should work in this case.

[Tomas Skrivan]

Personally, I would reserve ∇² for Hessian i.e. matrix of all second order derivatives.

[Tomas Skrivan]

For Laplacian I would go with Δ

[Joseph Tooby-Smith]

One place it would be nice to implement these results is in
PhysLean.QuantumMechanics .OneDimension.GeneralPotential.Basic, and more generally in quantum mechanics.

I also think it may be worth making Space, and Time non-reducible(?) to prevent casting from say ℝ to Time. One way of doing this is to make them structures, but I think there is probably a better way (I've discussed this with some people before but forgot what the conclusion was).

(Not expecting anyone to do any of this just getting it out there :) )

[ZhiKai Pong]

I think this is somewhat related, if I want to show Time.deriv and Space.deriv commute, is it sufficient to state that their respective underlying fderiv commute, or do we want a more "physical" approach? (I don't know what that would look like)

[ZhiKai Pong]

for example ∂ₜ (∇ × E) = ∇ × (∂ₜ E)

[Joseph Tooby-Smith]

I have no problem with you using the underlying fderiv :).

My comment about non-reduciablity is to stop you doing something like:

def oddDef (t : Time) : Space 1 := t

which would currently work because Lean tries to help by casting types - but in this case isn't helping.

[Tomas Skrivan]

Joseph Tooby-Smith said:

I also think it may be worth making Space, and Time non-reducible(?) to prevent casting from say ℝ to Time. One way of doing this is to make them structures, but I think there is probably a better way (I've discussed this with some people before but forgot what the conclusion was).

I understand that from a philosophical standpoint this is desirable but I would be very cautious about this. You might end up duplicating lots of API for not technical benefit but only philosophical one.

[Alex Meiburg]

Hot take: the real issue here (philsophically - and this can be reflected in the Lean!) is that Space and Time aren't reals, they're AddTorsor ℝ.

That is, Time is some generic Type* equipped with an AddTorsor ℝ Time instance; Space k is some other generic Type* equipped with an AddTime ℝ^k (Space k) instance.

docs#AddTorsor

[Alex Meiburg]

This correctly reflects the fact that, for instance, there's no notion of adding a Time to a Time: I can't add last Wednesday to tomorrow to get a meaningful number. Same goes for locations in space

You can take the differences between times, though, and get a Real out, with p₁ -ᵥ p₂

[Alex Meiburg]

And I contend that casting that Real acrossSpace 1 and Time is actually a much smaller sin. Since it's only ever measuring distances (and not absolute positions), this is just converting distance to durations (at, presumably, the speed of light), which is a "cast" that physicists happily do very often all the time anyway

[Alex Meiburg]

It's actually a failing that docs#deriv has the type signature

{𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : 𝕜 → F) (x : 𝕜) : F

when it could just as well have the type signature

{𝕜 : Type u} [NontriviallyNormedField 𝕜] {P : Type w} [AddTorsor 𝕜 P] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : P → F) (x : 𝕜) : F

which would correctly let us talk about derivatives on a torsor. Similarly, fderiv requires the domain be a module AddCommGroup E when it really should be AddTorsor P E.

Then it would use the instance addGroupIsAddTorsor by default anyway, and basically work the same for "simple" cases.

[Alex Meiburg]

I guess I would be willing to try to make this change in upstream mathlib (assuming that mathlib folks are okay with it - will open thread in a sec). I recognize that doing calculus is kind of a bare minimum for a useful definition, so I wouldn't expect PhysLean to accept torsors as the basis for spacetime until you can do derivatives with them in a reasonable way... but I feel confident this is the "right" way to state (flat) spacetime!

[Joseph Tooby-Smith]

Hi Alex, I agree with pretty much all of this. This is somewhat related to my post about the definition of a second and how ℝ is equipped with a norm in a way that Time really shouldn't be.

I think (correct me if you disagree) that we can take Time as manifold should be taken as isomorphic to ℝ. (I know in some systems you take time to be isomorphic to the circle as a manifold, or a closed interval etc.) But I think taking it isomorphic to ℝ is most useful for most purposes.
So maybe defining Time as the type ℝ without any additional structure (so def not abbrev), then putting on it an instance of AddTorsor ℝ Time and any other bona-fide instances instead of just inheriting things from ℝ .

This will also make it much easier to make Time non-reducible which solves my problem.

[Alex Meiburg]

Yeah, I think that taking it as an AddTorsor should be logically equivalent to taking it as a simply connected manifold with zero curvature...

At least, it is a fact that AddTorsor G P always means that P is isomorphic to a group G. It just has no "canonical" origin, and so no canonical isomorphism. This is a special case of how a group is a manifold for itself, I guess

[Alex Meiburg]

Other thread about mathlib

[Joseph Tooby-Smith]

This relies you on having the type P in the first place though, and I think it is better to have a specific type called Time, then having a variable P in all equations which can equivalently represent time (although the category theorist in me doesn't want to say this :().

In any case I think we are agreeing on the main points.
I will create an issue on PhysLean regarding this. To others: This shouldn't discourage anyone from working with Time and Space as they currently are - we can refactor later :).

[Alex Meiburg]

Ah yes, that's how I meant it too. :)

[Tomas Skrivan]

On a high level, I guess I disagree. I believe that simple things should be kept simple. A huge part of physics is classical, no relativity and no quantum physics, and adding all this complexity has very little benefit there.

I would also consider the cost this will incur on onboarding new people to the project. Someone wants to do a simple thing in classical mechanics and suddenly has to learn how manifolds are done in mathlib or what an AddTorsor is.

What I want to say is that unless you have a concrete project where this is really beneficial I would strongly recommend keeping simple things simple. I think I'm talking from experience, multiple times I tried to make something "future proof" only to realize that I didn't consider some really common case and had to refactor everything again. (To give you an example, for a very long time I tried making symbolic/automatic differentiation in SciLean to also work for variational calculus too but it was adding so much more complexity than I had to abandoned it. I think I wasted lots of time and effort on it which could have been used elsewhere more efficiently.)

[Joseph Tooby-Smith]

I agree that it is wise to worry if there is going to be a cost to onboarding new people by doing this - and by making any such change in PhysLean.

I think this is something we can actually test. We have enough usages of Time and Space in classical mechanics, quantum mechanics, vector calculus etc. in PhysLean that I think we can test if this change is going to make a massive difference to it's usage and the end user experience.

But the way I see this is that you will only notice this change in definition of Time if you were doing something with Time that you shouldn't be.
For example, add two times, take the zero time, multiply two times etc.

The definition actual definition of Time will still be

def  Time : Type := ℝ

we're just not going to inherit every instance on ℝ.
So unless you actually are doing something related to smoothness etc. you are not going to need to worry about the definition of a manifold etc.

[Kevin Buzzard]

I would also consider the cost this will incur on onboarding new people to the project. Someone wants to do a simple thing in classical mechanics and suddenly has to learn how manifolds are done in mathlib or what an AddTorsor is.

For many years in the 2010s I was vehemently arguing that we should just get on and prove the fundamental theorem of calculus the way it's proved in a 1st year undergraduate course, so that 1st year undergraduates could get on formalizing analysis. There was a huge pushback from the analysts here; their argument was that the correct way to formalize integration was via some exotic integral taking values in a topological vector space, and that there was no point setting up the theory of 1-variable calculus, it should all be deduced from a multivariable theory; the argument was that multivariable calculus is not done by induction on number of variables, and there was simply no point doing the one-variable case when we knew we wanted the multivariable case. The idea was to deduce the FTC from some form of Stokes' theorem applied to an interval in the reals, with boundary the two endpoints. I argued and I argued (because I had a pile of 1st year undergraduates desperate to formalize analysis as they were being taught it) but I didn't get my way, and ultimately I think that the community made the right decision by ignoring me and doing things the way Bourbaki did them.

[Tyler Josephson ⚛️]

Onboarding cost is very real. I’ve guided many scientists / engineers into Lean, and it remains a steep learning curve. But I find it interesting how it’s gotten easier over the years - better documentation helped, Mechanics of Proof helped, search engine tools like Moogle helped. When I started, it was Lean 3, and my UG ChemE student didn’t know what a ring was or anything about abstract algebra, and he had to learn it to make any headway. Now, students come in with exactly the same background, and they can make more headway because powerful tactics and other tools just help.

I’ve been curious about differential manifolds since watching a few lovely videos about thermodynamics and manifolds, but I don’t understand them, I haven’t had the time to learn that version of thermo. I intuit that the rigorous way to formalize classical thermo will be through manifolds, and that such derivations will be more elegant and more powerful than those in all the engineering textbooks. But, I’d struggle with even reading such proofs, in the end. I’d struggle to communicate such results with people in my field, and they would struggle to build on it.

[Tyler Josephson ⚛️]

I wonder if PhysLean should be like Mathlib in this regard - make it as rigorous as possible, relying on present or future tactics / tools to make it accessible. Or is PhysLean just different? Kevin is glad Mathlib didn’t align with the math level of undergrads, and that’s wise because the people driving the field of mathematics forward have much more math expertise. But in science and engineering, “undergrad math” is not just a reasonable level of math for most learners, but many/most of the people driving the field forward don’t have much more math than the typical core taught to scientists and engineers. I’d like it if a grad student with that kind of background could derive a new theory in their area of research and also be able to formalize it, needing no more than perhaps a one-semester introduction to proofs in Lean.

[Joseph Tooby-Smith]

I agree with you Tyler. Especially at this stage when the community needs growing, anything that turns people off contributing is necessarily a bad thing.

I really hope that we can have the best of both worlds here. That we can have the rigorous definitions sitting behind, or parallel to more conventional and easy to use approaches. Then someone who's work depends on the rigorous definitions can use that, whilst someone who wants to work with more down-to-earth definitions can.
I think this is really a case of making good API and documentation. Similar to what is currently happening around Space and Time.

To use the example of theormodyanmics (which I don't know too much about - so apologize if I say something stupid). Ideally I would like to have in PhysLean both the conventional approach and the manifold approach. If the manifold approach can sit behind the conventional approach in such a way that someone using the conventional approach doesn't need to know it exists, then this is good. But I don't think we should sacrifice the usability of the conventional approach for the manifold approach - but I do think we should have the manifold approach also.

[Joseph Tooby-Smith]

I guess by "doesn't need to know it exists" can mean a number of different things.

• It could mean that the conventional approach is built completely separately from the manifold approach. And there may exist separate modules connecting the two.
• It could mean that the basic definitions of the conventional approach come from the manifold approach, but enough API exists that this is hidden.

I think the exact choice of which we follow here will depend on the exact nature of the problem.

[Joseph Tooby-Smith]

Given we can't actually change the definition of Space and Time until
this is resolved, and that this doesn't seem to be possible anytime soon, I've made this PR improving the docs around Time and Space.

Basically it explains that we inherit instances on these types and this, for example automatically gives us a metric etc., but also a few things we don't necessarily want.

[ZhiKai Pong]

Just writing this down somewhere to document what I've learnt the past couple days (mainly through here).

ZhiKai Pong said:

if I want to show Time.deriv and Space.deriv commute, is it sufficient to state that their respective underlying fderiv commute

Few days ago I wrote the message above as I set out to prove ∂ₜ (∇ × E) = ∇ × (∂ₜ E). It turns out this is much more complicated than what I previously conceived so I thought it might be worth sharing. What I had in mind was pretty much just: after unfolding all definitions I should have a bunch of terms of the form
$\frac{\partial^2}{\partial_x\partial_t}=\frac{\partial^2}{\partial_t\partial_x}$
and then I just show they commute. I've already proved differentiations along space coordinates ($\frac{\partial^2}{\partial_x\partial_y}=\frac{\partial^2}{\partial_y\partial_x}$) commute so surely this can't be that bad.

Now I'm realizing that Space and Time lives in different domains, and I'm actually trying to do differentiation in ℝ × ℝ³. I think how I'll have to approach this is to turn Space and Time derivatives into SpaceTime derivatives where the domain is ℝ × ℝ³ via timeSlice, and in Lean terms this involves a whole lot of (un)currying.

Many thanks to @Joseph Tooby-Smith and @Tomas Skrivan for their help and patience!

[Tomas Skrivan]

I got intrigued by how annoying this is, here is my sketch of proving

theorem fderiv_swap (f : X → Y → Z) (x dx : X) (y dy : Y) (hf : IsSymmSndFDerivAt 𝕜 (↿f) (x,y)) :
    fderiv 𝕜 (fun x' => fderiv 𝕜 (fun y' => f x' y') y dy) x dx
    =
    fderiv 𝕜 (fun y' => fderiv 𝕜 (fun x' => f x' y') x dx) y dy := by ...

Full code missing just the final differentiability obligations. With PR #24056 they might be solvable simple by fun_prop if you add the assumption ContDiff 𝕜 2 (↿f).

code

import Mathlib

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

theorem fderiv_uncurry (f : X → Y → Z) (xy dxy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) :
    fderiv 𝕜 ↿f xy dxy
    =
    fderiv 𝕜 (f · xy.2) xy.1 dxy.1 + fderiv 𝕜 (f xy.1 ·) xy.2 dxy.2 := by

  have hx : (f · xy.2) = ↿f ∘ (fun x' => (x',xy.2)) := by rfl
  have hy : (f xy.1 ·) = ↿f ∘ (fun y' => (xy.1,y')) := by rfl
  rw[hx,hy]
  repeat rw[fderiv_comp (hg:=by fun_prop) (hf:=by fun_prop)]
  dsimp
  rw[←ContinuousLinearMap.map_add]
  congr
  repeat rw[DifferentiableAt.fderiv_prod (hf₁ := by fun_prop) (hf₂ := by fun_prop)]
  simp

theorem fderiv_uncurry' (f : X → Y → Z) (xy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) :
    fderiv 𝕜 ↿f xy
    =
    (fderiv 𝕜 (f · xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
    +
    (fderiv 𝕜 (f xy.1 ·) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := by
  apply ContinuousLinearMap.ext; intro dxy
  exact fderiv_uncurry f xy dxy hf

theorem fderiv_uncurry'' (f : X → Y → Z) (hf : Differentiable 𝕜 (↿f)) :
    fderiv 𝕜 ↿f
    =
    fun xy =>
      (fderiv 𝕜 (f · xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
      +
      (fderiv 𝕜 (f xy.1 ·) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := by
  funext xy; exact fderiv_uncurry' f xy (hf xy)

theorem fderiv_wrt_prod (f : X × Y → Z) (xy dxy : X × Y) (hf : DifferentiableAt 𝕜 f xy) :
    fderiv 𝕜 f xy dxy
    =
    (fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1 dxy.1)
    +
    (fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2 dxy.2) :=
  fderiv_uncurry (fun x y => f (x,y)) xy dxy hf

theorem fderiv_wrt_prod' (f : X × Y → Z) (xy : X × Y) (hf : DifferentiableAt 𝕜 f xy) :
    fderiv 𝕜 f xy
    =
    (fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
    +
    (fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) :=
  fderiv_uncurry' (fun x y => f (x,y)) xy hf

theorem fderiv_wrt_prod'' (f : X × Y → Z) (hf : Differentiable 𝕜 f) :
    fderiv 𝕜 f
    =
    fun xy =>
      (fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
      +
      (fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) :=
  fderiv_uncurry'' (fun x y => f (x,y)) hf

theorem fderiv_clm_apply' (f : X → Y →L[𝕜] Z) (y : Y) (x dx : X) (h : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 f x dx y
    =
    fderiv 𝕜 (f · y) x dx := by
  rw[fderiv_clm_apply] <;> first | simp | fun_prop

theorem fderiv_swap (f : X → Y → Z) (x dx : X) (y dy : Y) (hf : IsSymmSndFDerivAt 𝕜 (↿f) (x,y)) :
    fderiv 𝕜 (fun x' => fderiv 𝕜 (fun y' => f x' y') y dy) x dx
    =
    fderiv 𝕜 (fun y' => fderiv 𝕜 (fun x' => f x' y') x dx) y dy := by

  have h := IsSymmSndFDerivAt.eq hf (dx,0) (0,dy)
  rw[fderiv_wrt_prod''] at h
  rw[fderiv_wrt_prod''] at h
  simp[Function.HasUncurry.uncurry] at h
  rw[fderiv_clm_apply'] at h
  rw[fderiv_clm_apply'] at h
  simp at h
  exact h
  -- differentiability conditions
  · sorry
  · sorry
  · sorry
  · sorry

theorem fderiv_swap' (f : X → Y → Z) (x : X) (y : Y) (hf : IsSymmSndFDerivAt 𝕜 (↿f) (x,y)) :
    fderiv 𝕜 (fun x' => fderiv 𝕜 (fun y' => f x' y') y) x
    =
    (fderiv 𝕜 (fun y' => fderiv 𝕜 (fun x' => f x' y') x) y).flip := by
  ext dx dy; simp
  rw[fderiv_clm_apply']
  rw[fderiv_clm_apply']
  rw[fderiv_swap f x dx y dy hf]
  · sorry
  · sorry

There are six versions of fderiv_uncurry:/

[Tomas Skrivan]

At the bottom of that code you can find version of the theorem with dx and dy not applied.

theorem fderiv_swap' (f : X → Y → Z) (x : X) (y : Y) (hf : IsSymmSndFDerivAt 𝕜 (↿f) (x,y)) :
    fderiv 𝕜 (fun x' => fderiv 𝕜 (fun y' => f x' y') y) x
    =
    (fderiv 𝕜 (fun y' => fderiv 𝕜 (fun x' => f x' y') x) y).flip := ..

[ZhiKai Pong]

@Tomas Skrivan sorry for pinging, I have this as an intermediate step:

import Mathlib

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

lemma fderiv_coord (f : ℝ → ℝ³ → ℝ³) (t dt : ℝ) (x : ℝ³) :
    (fderiv ℝ (fun t' => f t' x i) t) dt = (fderiv ℝ f t) dt x i := by
  sorry

codomain of the left fderiv is (fun x ↦ ℝ) i and codomain of the right fderiv is ℝ³ → ℝ³ . this manages to typecheck somehow, but how do I proceed to proof this?

[ZhiKai Pong]

(I think I'm getting the gist of what your previous message is doing, but it's getting quite complicated in my implementation due to all the coordinate functions i.e. EuclideanSpace.single )

[Tomas Skrivan]

I'm afraid that with the current mathlib you can't really prove this exactly because the codomain on rhs is ℝ³ → ℝ³. You can state it only because fderiv was generalized to general topological vector spaces but 99% of the theorems has not been generalized and they are formulated using normed vector spaces and ℝ³ → ℝ³ is not a normed vector space.

So my question is what is the original problem that got you to this lemma? Maybe you can't reformulate the original problem differently.

I will check with @Yury G. Kudryashov what are his thoughts on this as he is the one generalizing fderiv to topological vector spaces.

[ZhiKai Pong]

Tomas Skrivan said:

So my question is what is the original problem that got you to this lemma? Maybe you can't reformulate the original problem differently.

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 2 1 x - df 1 2 x
    | 1 => df 0 2 x - df 2 0 x
    | 2 => df 1 0 x - df 0 1 x

lemma dt_dist (f : ℝ → ℝ³ → ℝ³) :
    (fderiv ℝ (fun t => (fderiv ℝ (fun x => f t x u) x) dx1) t -
    fderiv ℝ (fun t => (fderiv ℝ (fun x => f t x v) x) dx2) t) 1
    =
    (fderiv ℝ (fun t => (fderiv ℝ (fun x => f t x u) x) dx1) t) 1 -
    (fderiv ℝ (fun t => (fderiv ℝ (fun x => f t x v) x) dx2) t) 1 := by
  rfl

theorem fderiv_swap (f : ℝ → ℝ³ → ℝ³) (t dt : ℝ) (x : ℝ³)
    (dx : EuclideanSpace ℝ (Fin 3)) (hf : IsSymmSndFDerivAt ℝ (↿f) (t,x)) :
    fderiv ℝ (fun t' => fderiv ℝ (fun x' => f t' x' i) x dx) t dt
    =
    (fderiv ℝ (fun x' => fderiv ℝ (fun t' => f t' x' i) t dt) x dx) := by
  sorry

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)]
  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]
    rw [dt_dist]
    rw [fderiv_swap, fderiv_swap]
    sorry -- stuck here
  · sorry
  · sorry

I think the problem stems from the original form of the statement itself?

In PhysLean the corresponding statement is

lemma time_deriv_curl (fₜ : Time → Space → EuclideanSpace ℝ (Fin 3)) (t : Time) (x : Space) :
    ∂ₜ (fun t => (∇ × fₜ t) x) t = (∇ × (∂ₜ fₜ t)) x:= by

if that gives any insight.

[Tomas Skrivan]

Instead of curl (fderiv ℝ (fun t' => (fₜ t')) t 1) x I think you should have curl (fun x' => fderiv ℝ (fun t' => (fₜ t' x')) t 1) x.

The PhysLean statement has the same issue here (∇ × (∂ₜ fₜ t)) x as you are differentiating fₜ which has codomain Space → EuclideanSpace ℝ (Fin 3). I do not know how to reformulate it "correctly" with the PhysLean's fancy notation (correctly is relative here as we are fighting mathlib's deficiency).

You can of course write (∇ × (fun x' => ∂ₜ (fun t' => fₜ t' x') t)) x but it effectively looses the point of the nice notation.

In SciLean's derivative notation I would write ∇× (x':=x), ∂ (t':=t), fₜ t' x' except there is no ∇× operator defined right now. But there is notation like this for all kinds of derivatives ∂ ∇ ∂> <∂ (derivative, gradient, forward mode AD, reverse mode AD).

[ZhiKai Pong]

With this change
Tomas Skrivan said:

Instead of curl (fderiv ℝ (fun t' => (fₜ t')) t 1) x I think you should have curl (fun x' => fderiv ℝ (fun t' => (fₜ t' x')) t 1) x.

I'm still left with

(fderiv ℝ (fun t' => ft t' x' i) t) dt = (fderiv ℝ (fun t' => ft t' x) t) dt i

Maybe this is doable with fderiv_pi, let me try

[ZhiKai Pong]

ah ok this works! thanks

[ZhiKai Pong]

is there an idiomatic way to state the assumption that leads to DifferentiableAt ℝ (fun t' => f t' x i) t?

Edit: I think hf : Differentiable ℝ (↿f) works

[ZhiKai Pong]

@Tomas Skrivan I don't know how bad this is, can your PR (#24056) handle this?
I can imagine doing differentiability arguments on curried functions might be a terrible idea...

import Mathlib

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

example (ft : ℝ → ℝ³ → ℝ³) (hf : ContDiff ℝ 2 ↿ft) :
    DifferentiableAt ℝ (fun t =>
    (fderiv ℝ (fun x => ft t x 2) x) (EuclideanSpace.single 1 1)) t := by
  apply Differentiable.clm_apply
  . sorry
  · fun_prop

[Tomas Skrivan]

I think fun_prop should be able to do this, it is definitely designed to handle assumptions on uncurried functions. Right now I'm not at my computer so I can't test it

[ZhiKai Pong]

I'm not sure what I should do here, should I just wait for your PR to go through or will that take a long time?
Or is it the best to add the new lemmas manually for the time being then refactor later once the PR goes live?

Anyway, this is no hurry at all, so please don't feel pressured if you're busy, you are already extremely helpful and I appreciate it a lot :)

[Tomas Skrivan]

No idea what is the best approach. You can create a PR that depends on that PR but you won't have PhysLean unless you make a special branch that depends on that PR.

You(or me) could also harass someone to review it and merge it. Maybe I can make a topic in #mathlib4 about it to draw more attention. I don't know :man_shrugging:

[Joseph Tooby-Smith]

Sorry I've only managed to vaguely follow this conversation.

One option would be to, for the time being, make a definition of a Prop corresponding to the lemma you can't prove yet. Then

1. carry around this Prop as an assumption in further results.
2. Add that this Prop needs a proof, and that we are waiting on the relevant PR.

[Joseph Tooby-Smith]

Ok, this is not the nicest, and may not be what you actually want here, but this may hold over until we have this PR.

Code

import Mathlib

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


variable {k : Type} [NontriviallyNormedField k]
    {N W M : Type} [NormedAddCommGroup M] [NormedSpace k M]
    [NormedAddCommGroup N] [NormedSpace k N]
    [NormedAddCommGroup W] [NormedSpace k W]

private lemma fderiv_uncurry (f : N → W → M) (y : N × W) (w : W)
    (h : DifferentiableAt k (Function.uncurry f) y) :
    fderiv k (Function.uncurry f) y (0, w) =
    fderiv k (fun x => f y.1 x) y.2 w := by
  rw [show (fun x => f y.1 x) =
    (Function.uncurry f) ∘ (fun x => (y.1, x)) by {ext w; rfl}]
  rw [fderiv_comp _ (by fun_prop) (by fun_prop)]
  rw [(hasFDerivAt_prodMk_right (𝕜 := k) y.1 y.2).fderiv]
  rfl


example (ft : ℝ → ℝ³ → ℝ³) (hf : ContDiff ℝ 2 ↿ft) :
    DifferentiableAt ℝ (fun t =>
    (fderiv ℝ (fun x => ft t x 2) x) (EuclideanSpace.single 1 1)) t := by
  apply Differentiable.clm_apply
  . let incl : ℝ³ →L[ℝ] ℝ × ℝ³ := {
      toFun w := (0, w)
      map_add' := by simp
      map_smul' := by simp
      }
    let inclL : ℝ → ℝ × ℝ³ := fun y => (y, x)
    let ftt : ℝ → ℝ³ → ℝ := fun y x => ft y x 2
    let drop : ℝ³ →L[ℝ] ℝ  := {
      toFun x := x 2
      map_add' := by simp
      map_smul' := by simp
      cont := by fun_prop
    }
    have hd : ContDiff ℝ 2 (Function.uncurry ftt) := by
      change ContDiff ℝ 2 (fun x => (↿ft) x 2)
      change ContDiff ℝ 2 (drop ∘ (↿ft))
      apply ContDiff.comp
      · exact ContinuousLinearMap.contDiff drop
      · exact hf
    have hdd : Differentiable ℝ (Function.uncurry ftt) := by
      apply ContDiff.differentiable hd
      simp
    have h1 (y : ℝ) : fderiv ℝ (fun x => ftt y x) x
      = fderiv ℝ (Function.uncurry ftt) (y, x) ∘L incl:= by
      ext w
      simp [incl]
      rw [fderiv_uncurry]
      exact hdd (y, x)
    conv =>
      enter [2, y]
      change fderiv ℝ (fun x => ftt y x) x
      rw [h1]
    refine Differentiable.clm_comp ?_ ?_
    · have hn (y : ℝ) :  fderiv ℝ (Function.uncurry ftt) (y, x)=
        fderiv ℝ (Function.uncurry ftt) (inclL y) := rfl
      conv =>
        enter [2, y]
        rw [hn]
      refine Differentiable.comp' ?_ ?_
      · have hd'' : ContDiff ℝ (1 + 1) (Function.uncurry ftt) := hd
        rw [contDiff_succ_iff_fderiv] at hd''
        have hd2 := hd''.2.2
        apply ContDiff.differentiable hd2
        rfl
      · fun_prop
    · fun_prop
  · fun_prop

PhysLean already has fderiv_uncurry in the TimeSlice file because I needed this there.

[ZhiKai Pong]

I realized that the fderiv_swapoccurs at ℝ × ℝ³, but then what I actually need is ℝ × (fun x ↦ ℝ) i since I'm working with fin_cases...

what I mean by that is I ended up with this:

import Mathlib

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

example (f : ℝ → ℝ³ → ℝ³) (x dx : ℝ³) (t dt : ℝ)
    (h : (fderiv ℝ (fun t' => (fderiv ℝ (fun x' => f t' x') x) dx) t) dt
    =
    (fderiv ℝ (fun x => (fderiv ℝ (fun x' => f x' x) t) dt) x) dx) :
    (fderiv ℝ (fun t' => (fderiv ℝ (fun x' => f t' x' i) x) dx) t) dt
    =
    (fderiv ℝ (fun x' => (fderiv ℝ (fun t' => f t' x' i) t) dt) x) dx := by
  sorry

I think I'll have to reformulate the fderiv_uncurry and fderiv_wrt_prod to handle the FinType explicitly? I'll have a go but let me know if there's a simpler way to do this directly on what's given above...

[ZhiKai Pong]

have hf' : IsSymmSndFDerivAt ℝ (↿f) (t,x) :=
    sorry

ok I think it's just this^ statement has to be changed to be in in terms of the FinType, I'm just not sure how to state this

full code

import Mathlib

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

section

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

theorem fderiv_uncurry (f : X → Y → Z) (xy dxy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) :
    fderiv 𝕜 ↿f xy dxy
    =
    fderiv 𝕜 (f · xy.2) xy.1 dxy.1 + fderiv 𝕜 (f xy.1 ·) xy.2 dxy.2 := by

  have hx : (f · xy.2) = ↿f ∘ (fun x' => (x',xy.2)) := by rfl
  have hy : (f xy.1 ·) = ↿f ∘ (fun y' => (xy.1,y')) := by rfl
  rw[hx,hy]
  repeat rw[fderiv_comp (hg:=by fun_prop) (hf:=by fun_prop)]
  dsimp
  rw[←ContinuousLinearMap.map_add]
  congr
  repeat rw[DifferentiableAt.fderiv_prodMk (hf₁ := by fun_prop) (hf₂ := by fun_prop)]
  simp

theorem fderiv_uncurry' (f : X → Y → Z) (xy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) :
    fderiv 𝕜 ↿f xy
    =
    (fderiv 𝕜 (f · xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
    +
    (fderiv 𝕜 (f xy.1 ·) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := by
  apply ContinuousLinearMap.ext; intro dxy
  exact fderiv_uncurry f xy dxy hf

theorem fderiv_uncurry'' (f : X → Y → Z) (hf : Differentiable 𝕜 (↿f)) :
    fderiv 𝕜 ↿f
    =
    fun xy =>
      (fderiv 𝕜 (f · xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
      +
      (fderiv 𝕜 (f xy.1 ·) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := by
  funext xy; exact fderiv_uncurry' f xy (hf xy)

theorem fderiv_wrt_prod'' (f : X × Y → Z) (hf : Differentiable 𝕜 f) :
    fderiv 𝕜 f
    =
    fun xy =>
      (fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
      +
      (fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) :=
  fderiv_uncurry'' (fun x y => f (x,y)) hf

theorem fderiv_clm_apply' (f : X → Y →L[𝕜] Z) (y : Y) (x dx : X) (h : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 f x dx y
    =
    fderiv 𝕜 (f · y) x dx := by
  rw [fderiv_clm_apply] <;> first | simp | fun_prop
end

theorem fderiv_swap (f : ℝ  → ℝ³ → ℝ³) (t dt : ℝ ) (x dx : ℝ³) (hf : ContDiff ℝ 2 ↿f) :
    fderiv ℝ (fun t' => fderiv ℝ (fun x' => f t' x' i) x dx) t dt
    =
    (fderiv ℝ (fun x' => fderiv ℝ (fun t' => f t' x' i) t dt) x dx) := by
  have hf' : IsSymmSndFDerivAt ℝ (↿f) (t,x) :=
    sorry
  have h := IsSymmSndFDerivAt.eq hf' (dt,0) (0,dx)
  rw[fderiv_wrt_prod''] at h
  rw[fderiv_wrt_prod''] at h
  simp [-fderiv_eq_smul_deriv, Function.HasUncurry.uncurry] at h
  rw[fderiv_clm_apply'] at h
  rw[fderiv_clm_apply'] at h
  simp [-fderiv_eq_smul_deriv] at h
  sorry -- h is in ℝ³ but the goal is in coordinate form
  · sorry
  · sorry
  · sorry
  · sorry

[Joseph Tooby-Smith]

Wouldn't fderiv_pi work here? (may have to flip the arguments of f)

[Joseph Tooby-Smith]

Is something like the following what you are looking for?

code

import Mathlib

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

section

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

theorem fderiv_uncurry (f : X → Y → Z) (xy dxy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) :
    fderiv 𝕜 ↿f xy dxy
    =
    fderiv 𝕜 (f · xy.2) xy.1 dxy.1 + fderiv 𝕜 (f xy.1 ·) xy.2 dxy.2 := by

  have hx : (f · xy.2) = ↿f ∘ (fun x' => (x',xy.2)) := by rfl
  have hy : (f xy.1 ·) = ↿f ∘ (fun y' => (xy.1,y')) := by rfl
  rw[hx,hy]
  repeat rw[fderiv_comp (hg:=by fun_prop) (hf:=by fun_prop)]
  dsimp
  rw[←ContinuousLinearMap.map_add]
  congr
  repeat rw[DifferentiableAt.fderiv_prodMk (hf₁ := by fun_prop) (hf₂ := by fun_prop)]
  simp

theorem fderiv_uncurry' (f : X → Y → Z) (xy : X × Y) (hf : DifferentiableAt 𝕜 (↿f) xy) :
    fderiv 𝕜 ↿f xy
    =
    (fderiv 𝕜 (f · xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
    +
    (fderiv 𝕜 (f xy.1 ·) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := by
  apply ContinuousLinearMap.ext; intro dxy
  exact fderiv_uncurry f xy dxy hf

theorem fderiv_uncurry'' (f : X → Y → Z) (hf : Differentiable 𝕜 (↿f)) :
    fderiv 𝕜 ↿f
    =
    fun xy =>
      (fderiv 𝕜 (f · xy.2) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
      +
      (fderiv 𝕜 (f xy.1 ·) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) := by
  funext xy; exact fderiv_uncurry' f xy (hf xy)

theorem fderiv_wrt_prod'' (f : X × Y → Z) (hf : Differentiable 𝕜 f) :
    fderiv 𝕜 f
    =
    fun xy =>
      (fderiv 𝕜 (fun x' => f (x',xy.2)) xy.1).comp (ContinuousLinearMap.fst 𝕜 X Y)
      +
      (fderiv 𝕜 (fun y' => f (xy.1,y')) xy.2).comp (ContinuousLinearMap.snd 𝕜 X Y) :=
  fderiv_uncurry'' (fun x y => f (x,y)) hf

theorem fderiv_clm_apply' (f : X → Y →L[𝕜] Z) (y : Y) (x dx : X) (h : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 f x dx y
    =
    fderiv 𝕜 (f · y) x dx := by
  rw [fderiv_clm_apply] <;> first | simp | fun_prop
end

theorem fderiv_swap (f : ℝ  → ℝ³ → ℝ³) (t dt : ℝ ) (x dx : ℝ³) (hf : ContDiff ℝ 2 ↿f) :
    fderiv ℝ (fun t' => fderiv ℝ (fun x' => f t' x' i) x dx) t dt
    =
    (fderiv ℝ (fun x' => fderiv ℝ (fun t' => f t' x' i) t dt) x dx) := by
  have hf' : IsSymmSndFDerivAt ℝ (↿f) (t,x) :=
    sorry
  have h := IsSymmSndFDerivAt.eq hf' (dt,0) (0,dx)
  rw[fderiv_wrt_prod''] at h
  rw[fderiv_wrt_prod''] at h
  simp [-fderiv_eq_smul_deriv, Function.HasUncurry.uncurry] at h
  rw[fderiv_clm_apply'] at h
  rw[fderiv_clm_apply'] at h
  simp [-fderiv_eq_smul_deriv] at h
  let drop : ℝ³ →L[ℝ] ℝ  := {
      toFun x := x i
      map_add' := by simp
      map_smul' := by simp
      cont := by fun_prop
    }
  change (fderiv ℝ
      (fun t' => (fderiv ℝ (drop ∘ (fun x' => f t' x')) x) dx) t) dt = _
  trans (fderiv ℝ
      (fun t' => ((fderiv ℝ (⇑drop) (f t' x)).comp (fderiv ℝ (fun x' => f t' x') x)) dx) t) dt
  · congr
    funext t'
    rw [fderiv_comp]
    · fun_prop
    · sorry
  simp only [ContinuousLinearMap.fderiv, ContinuousLinearMap.coe_comp',
    Function.comp_apply,  smul_eq_mul]
  rw [fderiv_comp']
  simp [-fderiv_eq_smul_deriv]
  rw [h]
  change _ =
    (fderiv ℝ (fun x' => (fderiv ℝ (drop ∘ (fun t' => f t' x')) t) dt) x) dx
  trans (fderiv ℝ (fun x' => ((fderiv ℝ (⇑drop) (f t x')).comp (fderiv ℝ (fun t' => f t' x') t)) dt) x) dx
  swap
  · congr
    funext x'
    rw [fderiv_comp]
    · fun_prop
    · sorry
  simp  [-fderiv_eq_smul_deriv]
  rw [fderiv_comp']
  simp
  · fun_prop
  · sorry
  · fun_prop
  · sorry
  · sorry
  · sorry
  · sorry
  · sorry

[Joseph Tooby-Smith]

I think all the remaining sorry’s (except the first which is easy) here could be relatively straight forward applications of the same principal I used. Define a functions through compositions of functions which are known to be differentiable.

[ZhiKai Pong]

oh my, thanks a lot... I'll try to understand this and clean this up over the next few days.

Just curious, may I ask is this annoying and complicated for you as well or is it more or less straightforward with experience?

[Kevin Buzzard]

For some of us, solving these complicated problems is part of the fun :-)

[Joseph Tooby-Smith]

Yeah I agree with Kevin - its all part of the fun :)

I would say this is probably something that comes with time though, you get to know where to look, what sort of things are likely to work and what things are likely to be called etc. These all make some of the more annoying bits easier, and probably more enjoyable. Getting to know how to use loogle effectively helped me an awful lot.

[Joseph Tooby-Smith]

Here is a complete proof of fderiv_swap. It is very much a mess, but is sorry-free. It can very likely be broken down into a series of smaller lemmas.

The code below needs the preliminary material of the code in my last but one message (it goes over the character limit if I include it here).

Code

theorem fderiv_swap (f : ℝ  → ℝ³ → ℝ³) (t dt : ℝ ) (x dx : ℝ³) (hf : ContDiff ℝ 2 ↿f) :
    fderiv ℝ (fun t' => fderiv ℝ (fun x' => f t' x' i) x dx) t dt
    =
    (fderiv ℝ (fun x' => fderiv ℝ (fun t' => f t' x' i) t dt) x dx) := by
  have hf' : IsSymmSndFDerivAt ℝ (↿f) (t,x) := by
    apply ContDiffAt.isSymmSndFDerivAt (n := 2)
    · exact ContDiff.contDiffAt hf
    · simp
  have hd : Differentiable ℝ (↿f) :=
    ContDiff.differentiable hf (by simp)
  have hdd (xt : ℝ × ℝ³) : Differentiable ℝ (fderiv ℝ (↿f)) :=  by
    change ContDiff ℝ (1 + 1) ↿f at hf
    rw [contDiff_succ_iff_fderiv] at hf
    have hd2 := hf.2.2
    apply ContDiff.differentiable hd2
    rfl
  let inclT (x' : ℝ³) : ℝ → ℝ × ℝ³ := fun t' => (t', x')
  let inclX (t' : ℝ) : ℝ³ → ℝ × ℝ³ := fun x' => (t', x')
  have h_fderiv_t_differentiable (dt : ℝ) :
        Differentiable ℝ (fun x' => (fderiv ℝ (fun t' => f t' x') t) dt):= by
    intro x'
    have hl (x' : ℝ³) : (fun t' => f t' x') = ↿f ∘ inclT x' := by
      funext x'
      rfl
    have hdl (x' : ℝ³) : (fderiv ℝ (fun t' => f t' x') t) dt
      = (fderiv ℝ (↿f) (inclT x' t)) ((fderiv ℝ (inclT x') t) dt) := by
      rw [hl]
      rw [fderiv_comp]
      simp [-fderiv_eq_smul_deriv]
      · fun_prop
      · fun_prop
    conv_lhs =>
      enter [x']
      rw [hdl x']
    refine DifferentiableAt.clm_apply ?_ ?_
    · simp [inclT]
      change DifferentiableAt ℝ  (fderiv ℝ (↿f) ∘ inclX t ) x'
      refine DifferentiableAt.comp x' ?_ ?_
      · exact hdd (inclT x t) (inclX t x')
      · fun_prop
    · have hl(x' : ℝ³) : (fderiv ℝ (inclT x') t) dt = (dt, 0) := by
        simp only [inclT]
        rw [(hasFDerivAt_prodMk_left (𝕜 := ℝ) t x').fderiv ]
        simp
      conv_lhs =>
        enter [x']
        rw [hl x']
      fun_prop

  have h := IsSymmSndFDerivAt.eq hf' (dt,0) (0,dx)
  rw[fderiv_wrt_prod''] at h
  rw[fderiv_wrt_prod''] at h
  simp [-fderiv_eq_smul_deriv, Function.HasUncurry.uncurry] at h
  rw[fderiv_clm_apply'] at h
  rw[fderiv_clm_apply'] at h
  simp [-fderiv_eq_smul_deriv] at h
  let drop : ℝ³ →L[ℝ] ℝ  := {
      toFun x := x i
      map_add' := by simp
      map_smul' := by simp
      cont := by fun_prop
    }
  change (fderiv ℝ
      (fun t' => (fderiv ℝ (drop ∘ (fun x' => f t' x')) x) dx) t) dt = _
  trans (fderiv ℝ
      (fun t' => ((fderiv ℝ (⇑drop) (f t' x)).comp (fderiv ℝ (fun x' => f t' x') x)) dx) t) dt
  · congr
    funext t'
    rw [fderiv_comp]
    · fun_prop
    · let inclX : ℝ³ → ℝ × ℝ³ := fun x' => (t', x')
      have hl : (fun x' => f t' x') = ↿f ∘ inclX := by
        funext x'
        rfl
      rw [hl]
      apply DifferentiableAt.comp
      · fun_prop
      · fun_prop
  simp only [ContinuousLinearMap.fderiv, ContinuousLinearMap.coe_comp',
    Function.comp_apply,  smul_eq_mul]
  rw [fderiv_comp']
  simp [-fderiv_eq_smul_deriv]
  rw [h]
  change _ =
    (fderiv ℝ (fun x' => (fderiv ℝ (drop ∘ (fun t' => f t' x')) t) dt) x) dx
  trans (fderiv ℝ (fun x' => ((fderiv ℝ (⇑drop) (f t x')).comp (fderiv ℝ (fun t' => f t' x') t)) dt) x) dx
  swap
  · congr
    funext x'
    rw [fderiv_comp]
    · fun_prop
    · let inclT : ℝ → ℝ × ℝ³ := fun t' => (t', x')
      have hl : (fun t' => f t' x') = ↿f ∘ inclT := by
        funext x'
        rfl
      rw [hl]
      apply DifferentiableAt.comp
      · fun_prop
      · fun_prop
  simp  [-fderiv_eq_smul_deriv]
  rw [fderiv_comp']
  simp
  /- Start of differenitablity conditions. -/
  · fun_prop
  · exact h_fderiv_t_differentiable dt x
  · fun_prop
  · have hl (t' : ℝ) : (fun x' => f t' x') = ↿f ∘ inclX t' := by
      funext x'
      rfl
    have hdl (t' : ℝ) : (fderiv ℝ (fun x' => f t' x') x) dx
      = (fderiv ℝ (↿f) (inclX t' x)) ((fderiv ℝ (inclX t') x) dx) := by
      rw [hl]
      rw [fderiv_comp]
      simp [-fderiv_eq_smul_deriv]
      · fun_prop
      · fun_prop
    conv_lhs =>
      enter [x']
      rw [hdl x']
    refine DifferentiableAt.clm_apply ?_ ?_
    · simp [inclT]
      change DifferentiableAt ℝ  (fderiv ℝ (↿f) ∘ inclT x ) t
      refine DifferentiableAt.comp t ?_ ?_
      · exact hdd (inclT x t) (inclT x t)
      · fun_prop
    · have hl(t' : ℝ) : (fderiv ℝ (inclX t') x) dx = (0, dx) := by
        simp only [inclT]
        rw [(hasFDerivAt_prodMk_right (𝕜 := ℝ) t' x).fderiv ]
        simp
      conv_lhs =>
        enter [x']
        rw [hl x']
      fun_prop
  · refine (DifferentiableAt.add_iff_right ?_).mpr ?_
    · refine DifferentiableAt.clm_comp ?_ ?_
      ·
        -- DifferentiableAt ℝ (fun y' => fderiv ℝ (fun x' => f x' y') t) x
        have hl (x' : ℝ³) : (fun t' => f t' x') = ↿f ∘ inclT x' := by
          funext x'
          rfl
        have hdl (x' : ℝ³) : (fderiv ℝ (fun t' => f t' x') t)
          =  (fderiv ℝ (↿f) (inclT x' t)).comp (fderiv ℝ (inclT x') t) := by
          rw [hl]
          rw [fderiv_comp]
          · fun_prop
          · fun_prop
        conv_lhs =>
          enter [x']
          rw [hdl x']
        simp
        apply DifferentiableAt.clm_comp
        · apply DifferentiableAt.comp
          · exact hdd (inclT x t) (inclT x t)
          · fun_prop
        · have hl(x' : ℝ³) : (fderiv ℝ (inclT x') t)  =  ContinuousLinearMap.inl ℝ ℝ ℝ³ := by
            simp only [inclT]
            rw [(hasFDerivAt_prodMk_left (𝕜 := ℝ) t x').fderiv ]
          conv_lhs =>
            enter [x']
            rw [hl x']
          fun_prop
      · fun_prop
    · refine DifferentiableAt.clm_comp ?_ ?_
      · -- DifferentiableAt ℝ (fderiv ℝ fun y' => f t y') x
        have hl (t' : ℝ) : (fun x' => f t' x') = ↿f ∘ inclX t' := by
          funext x'
          rfl
        have hdl (x' : ℝ³) : fderiv ℝ (fun y' => f t y') x'
          = (fderiv ℝ (↿f) (inclX t x')).comp (fderiv ℝ (inclX t) x')   := by
          rw [hl]
          rw [fderiv_comp]
          · fun_prop
          · fun_prop
        conv_lhs =>
          enter [x']
          rw [hdl x']
        apply DifferentiableAt.clm_comp
        · apply DifferentiableAt.comp
          · exact hdd (inclT x t) (inclT x t)
          · fun_prop
        · fun_prop
      · fun_prop
  · refine (DifferentiableAt.add_iff_right ?_).mpr ?_
    · refine DifferentiableAt.clm_comp ?_ ?_
      · --  DifferentiableAt ℝ (fderiv ℝ fun x' => f x' x) t
        have hl (x' : ℝ³) : (fun t' => f t' x') = ↿f ∘ inclT x' := by
          funext x'
          rfl
        have hdl (x' : ℝ³) : (fderiv ℝ (fun t' => f t' x') )
          =  fun x => (fderiv ℝ (↿f) (inclT x' x)).comp (fderiv ℝ (inclT x') x) := by
          rw [hl]
          funext x
          rw [fderiv_comp]
          · fun_prop
          · fun_prop
        conv_lhs =>
          rw [hdl ]
        simp
        apply DifferentiableAt.clm_comp
        · apply DifferentiableAt.comp
          · exact hdd (inclT x t) (inclT x t)
          · fun_prop
        · fun_prop
      · fun_prop
    · refine DifferentiableAt.clm_comp ?_ ?_
      · -- DifferentiableAt ℝ (fun x' => fderiv ℝ (fun y' => f x' y') x) t
        have hl (t' : ℝ) : (fun x' => f t' x') = ↿f ∘ inclX t' := by
          funext x'
          rfl
        have hdl (t' : ℝ) : (fderiv ℝ (fun x' => f t' x') x)
          =  (fderiv ℝ (↿f) (inclX t' x)).comp (fderiv ℝ (inclX t') x) := by
          rw [hl]
          rw [fderiv_comp]
          · fun_prop
          · fun_prop
        conv_lhs =>
          enter [x']
          rw [hdl x']
        apply DifferentiableAt.clm_comp
        · apply DifferentiableAt.comp
          · exact hdd (inclT x t) (inclT x t)
          · fun_prop
        · have hl(t' : ℝ) : (fderiv ℝ (inclX t') x)  = ContinuousLinearMap.inr ℝ ℝ ℝ³ := by
            simp only [inclT]
            rw [(hasFDerivAt_prodMk_right (𝕜 := ℝ) t' x).fderiv ]
          conv_lhs =>
            enter [x']
            rw [hl x']
          fun_prop
      · fun_prop
  · fun_prop
  · exact hdd (inclT x t)

[ZhiKai Pong]

@Joseph Tooby-Smith

(fderiv 𝕜 (↿f) xy) dxy = (fderiv 𝕜 (Function.uncurry f) xy) dxy

this is resolvable by rflbut rw can't see through this. Which version do we want?

[Joseph Tooby-Smith]

IMO I think the former is better.

[ZhiKai Pong]

variable {k : Type} [NontriviallyNormedField k]
    {N W M : Type} [NormedAddCommGroup M] [NormedSpace k M]
    [NormedAddCommGroup N] [NormedSpace k N]
    [NormedAddCommGroup W] [NormedSpace k W]

In a declaration like this is it more idiomatic to write {k : Type} or just {k}?

[Joseph Tooby-Smith]

I prefer the former i.e. {k : Type}. My brain has to do slightly less thinking to process it :).

[ZhiKai Pong]

@Tomas Skrivan may I ask why is docs#Differentiable.comp' in Mathlib.Tactic.FunProp.Differentiable but not in Mathlib.Analysis.Calculus.FDeriv.Comp like docs#Differentiable.comp? I tried to find the former in FDeriv.Comp and only realized they're in a different directory later on...

[Tomas Skrivan]

Ohh that is for historical reasons, that file should be removed and those theorems moved/removed.

The reason was while developing fun_prop I didn't have to recompile the whole mathlib when I made changes to fun_prop tactic.

[ZhiKai Pong]

I was puzzled for a while why it runs fine on the web editor but not on my own setup until I realized I didn't have the right imports :melting_face:

[ZhiKai Pong]

@Tomas Skrivan does this actually require x and y to be real?

import Mathlib

variable {𝕜 : Type} [NontriviallyNormedField 𝕜]
    {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
    [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
    [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]

example (x : X) (y : Y) : DifferentiableAt 𝕜 (fderiv 𝕜 fun y' => (x, y')) y := by
  fun_prop --doesn't work

example (x : ℝ) (y : ℝ) : DifferentiableAt ℝ (fderiv ℝ fun y' => (x, y')) y := by
  fun_prop --goes through analytic and requires CompleteSpace (X × Y)

[ZhiKai Pong]

import Mathlib

variable {𝕜 : Type} [NontriviallyNormedField 𝕜]
    {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
    [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
    [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]

example (x : X) (y : Y) : DifferentiableAt 𝕜 (fderiv 𝕜 fun y' => (x, y')) y := by
  have hl (y' : Y) : (fderiv 𝕜 fun y' => (x, y')) y' = ContinuousLinearMap.inr 𝕜 X Y := by
    rw [(hasFDerivAt_prodMk_right x y').fderiv]
  conv_lhs =>
    enter [y]
    rw [hl]
  fun_prop

managed to prove it, probably just a matter of missing API then

[Tomas Skrivan]

Nice! I didn't test it but I would expect that this should be provable with #24056 by using just fun_prop

[ZhiKai Pong]

variable {𝕜 : Type} [NontriviallyNormedField 𝕜]
    {X Y Z : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
    [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
    [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]

lemma ContDiff.uncurry (f : X → Y → Z) (x : X) (hf : ContDiff 𝕜 2 ↿f) :
    ContDiff 𝕜 2 (f x) := by
  sorry

this looks like it's straightforward but I can't figure out how to proceed, suggestions appreciated

[Joseph Tooby-Smith]

I would expect something like the following:
f x is the composite of ↿f and the inclusion Y → X x Y taking y to (x, y). Then something like a comp property of ContDiff.