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.

[ZhiKai Pong]

I guess this is a more general question rather than vector calculus specific but might as well ask here:

lemma curl_smul (f : Space → EuclideanSpace ℝ (Fin 3)) (k : ℝ)
    (hf : Differentiable ℝ f) :
    ∇ × (k • f) = k • ∇ × f

I have the above, if I have something of the form

 (∇ × (k • f)) x = k • (fun x => (∇ × f) x) x

is it possible to use curl_smul or do I have to define something separately like the following?

lemma curl_smul_apply (f : Space → EuclideanSpace ℝ (Fin 3)) (k : ℝ)
    (hf : Differentiable ℝ f) (x : Space):
    (∇ × (k • f)) x = k • (fun x => (∇ × f) x) x

[Joseph Tooby-Smith]

You should be able to use curl_smul to rewrite

(∇ × (k • f)) x = (k • ∇ × f) x

I think then this should be definitionally equal to k • (fun x => (∇ × f) x) x
So e.g.

rw [curl_smul, show (k • ∇ × f) x = k • (fun x => (∇ × f) x) x from rfl]

might work.

[ZhiKai Pong]

ah I think I figured it out, lean parses the right hand side as k • ((∇ × f) x), and I have to explicitly tell it to parse this as (k • (∇ × f)) x... thanks!

[Tomas Skrivan]

@ZhiKai Pong this topic might be an interesting read which discusses convention fun x => k * f x vs k*f and similar. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Convention.20for.20.60f.20*.20g.60.20and.20.2F.20or.20.60fun.20x.20.E2.86.A6.20f.20x.20*.20g.20x.60

[ZhiKai Pong]

I'm looking at trying to state the stokes theorem in this or some similar form (If I understand correctly mathlib is still quite some way from having the differential forms version):
https://people.bath.ac.uk/masrs/ma20010/stokesproofs.pdf

there's not much in the integration chapter of #mil and I don't actually know much about measure theory so I have no idea how difficult this is, so I'd like to ask how feasible would this be, and also if anyone is more familiar with the integration-related part of mathlib.

I found docs#MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable which looks somewhat useful, but would appreciate pointers as to where I should start looking at.

[Joseph Tooby-Smith]

There is some integration stuff in this file:

https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean

which might be worth taking a look at.

[Joseph Tooby-Smith]

I'm not sure the difference but there are also Stokes-like theorems in this file

[ZhiKai Pong]

@Joseph Tooby-Smith I think I'm still not quite fully understanding how HasFDerivAt works.

looking at docs#fderiv_eq, it seems to me that the (f₀' x) term in ((h' : ∀ x, HasFDerivAt f₀ (f₀' x) x) is just to make sure fderiv 𝕜 f = f type checks, but it should in fact be the same x? In this case, I'm confused by where the 1 in the second derivative (h'' : ∀ x, HasFDerivAt (fun x => f₀' x 1) (f₀'' x) x) comes from, or whether it should be some other expression.

Playing around with the code I have (h'' : ∀ x x'', HasFDerivAt (fun x' => f₀' x' x'') (f₀'' x) x) that kind of works, but I've completely lost track of the mathematical meaning.

[ZhiKai Pong]

currently I have this end goal:

import Mathlib

variable {d : ℕ} (f₀'' : ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d))

example (i j : Fin d) (x s : EuclideanSpace ℝ (Fin d)) (c t : ℝ) :
    ∑ j, inner ((f₀'' (inner x s - c * t)) (inner (EuclideanSpace.single j (1:ℝ)) s))
    (EuclideanSpace.single i (1:ℝ)) = (f₀'' (inner x s - c * t)) 1 i := by
  sorry

but this doesn't really make sense to me. (not really a mwe, still figuring out what conditions am I missing to make this compile without errors)

[Joseph Tooby-Smith]

Let me try and break down my understanding of things:

fderiv 𝕜 f has type ℝ → ℝ →L[ℝ] EuclideanSpace ℝ (Fin d). The first ℝ in this type is the position where we want the derivative. The second ℝ is the direction in which we want the derivative. For ℝ there is only really one direction we would want to take a derivative, so we use 1 for this second ℝ.
Thus fderiv 𝕜 f x 1 is the derivative of f at the position x projected along 1 - the is the normal derivative of x. This mirrors the definition of docs#deriv.

Now turning to HasFDerivAt. The condition ∀ x, HasFDerivAt f (f' x) x says that f has a derivative equal to f' x at x. In otherwords, that fderiv 𝕜 f x = f' x, or
that fderiv 𝕜 f = f'.
Note that f' x does not yet specify the direction of that derivative, it is a function ℝ →L[ℝ] EuclideanSpace ℝ (Fin d). We only take the derivatives in the direction 1 so actually care about f' x 1. One could probably use docs#HasDerivAt here instead, and not carry around this direction.

Given this: (h'' : ∀ x, HasFDerivAt (fun x => f' x 1) (f'' x) x) says that the function (fun x => f' x 1) (that is the derivative of f in the direction 1) has derivative at x equal to f'' x, for all x. Again f'' x does not specify a direction so is a function ℝ →L[ℝ] EuclideanSpace ℝ (Fin d) and thus we will really get f'' x 1 appearing.

[Joseph Tooby-Smith]

Concerning your mwe, I wouldn't expect something like f'' (inner x s - c * t) _ to appear where _ is equal to (inner (EuclideanSpace.single j (1:ℝ)) s), namely the presences of s in this expression worries me.

[ZhiKai Pong]

import Mathlib

variable (f : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example {s : EuclideanSpace ℝ (Fin 3)} (h : ∀ x, inner ℝ (fderiv ℝ f x s) s = 0)
    (hf : Differentiable ℝ f) :
    ∃ C, ∀ x, inner ℝ (f x - C) s = 0 := by
  have h' : ∀ x, fderiv ℝ (fun x => (inner ℝ (f x) s)) x s = 0 := by
    intro x
    rw [fderiv_inner_apply]
    simp [-PiLp.inner_apply]
    rw [h]
    repeat fun_prop
  apply is_const_of_fderiv_eq_zero at h' --I want this but only restricted in direction of s

I've been stuck at this for a while, couldn't find any equivalent of docs#is_const_of_fderiv_eq_zero for a specific direction. docs#lineDeriv looks like it might be useful but I couldn't find anything. Any suggestions on where to look and what might be useful? Not sure if I'm missing something very obvious from Mathlib or this is not as trivial as it looks

[Joseph Tooby-Smith]

I do not think this result is true.

To give an explicit example, and using $(x,y,z)$ instead of $x$ for a position in EuclideanSpace ℝ (Fin 3). Let $f(x,y,z) = (y, x, 0)$ and let $s = e_y$. Thenfderiv ℝ f (x, y, z) s is $e_x$. Thus h is satisfied. But the goal is not true since the goal would imply that inner ℝ (f (x, y, z)) s = x is a constant, which it is not.

[Joseph Tooby-Smith]

Correct me if I'm wrong but I think the statement you are trying to prove is: If f is constant along the direction s then ∃ C, ∀ x, inner ℝ (f x - C) s = 0. The statement that f is constant along the direction s is equivalent to h : ∀ y, ∀ x, inner ℝ (fderiv ℝ f x y) s = 0. Then

import Mathlib

variable (f : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example {s : EuclideanSpace ℝ (Fin 3)} (h : ∀ y, ∀ x, inner ℝ (fderiv ℝ f x y) s = 0)
    (hf : Differentiable ℝ f) :
    ∃ C, ∀ x, inner ℝ (f x - C) s = 0 := by
  have h' :  ∀ x, fderiv ℝ (fun x => (inner ℝ (f x) s)) x  = 0 := by
    intro x
    ext y
    rw [fderiv_inner_apply]
    simp [-PiLp.inner_apply]
    rw [h]
    repeat fun_prop
  apply is_const_of_fderiv_eq_zero at h'
  · use f 0
    intro x
    rw [inner_sub_left, h' 0 x]
    simp
  · sorry

where the goal at sorry is of the form Differentiable _ _.

In my example of $f$ in my previous message, it does not satisfy my condition $h$ but does satisfy yours. It is also not constant in the direction $s$.

[ZhiKai Pong]

Joseph Tooby-Smith said:

The statement that f is constant along the direction s is equivalent to h : ∀ y, ∀ x, inner ℝ (fderiv ℝ f x y) s = 0.

This is precisely what I'm getting it wrong, thanks!

[ZhiKai Pong]

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example {s : EuclideanSpace ℝ (Fin 3)} (h : ∀ t x, fderiv ℝ (fun t => f t x) t = 0)
    (hf : Differentiable ℝ f) :
    ∃ C, ∀ t x, f t x = C := by
  apply is_const_of_fderiv_eq_zero at h

If f takes two different variables how should I apply is_const_of_fderiv_eq_zero ?

[ZhiKai Pong]

Or is this not true and I have to state it as ∀ x, ∃ C, ∀ t, f t x = C? trying to wrap my head around the quantifiers

[ZhiKai Pong]

Previously I just left the quantifiers out and assumed it works, but Kevin convinced me that they mean different things and I'm now realizing that it is indeed causing me trouble

[Joseph Tooby-Smith]

The hypothesis ∀ t x, fderiv ℝ (fun t => f t x) t = 0 states that for a fixed x the function t => f t x is constant. For example $f(t, x) = x$ satisfies this but does not satisfy your goal.

I believe ∀ x, ∃ C, ∀ t, f t x = C is correct here.

[Joseph Tooby-Smith]

The result you want to show is something along the following lines? If f t x is a function whose derivative with respect to time is zero everywhere, then the function f t x is independent of time.

[Tomas Skrivan]

Only the differentiability assumption hf should be stated as forall x, Differentiable R (f . x) or likely that uncurried f is differentiable i.e. differentiable in t and x jointly.

[ZhiKai Pong]

Joseph Tooby-Smith said:

The result you want to show is something along the following lines? If f t x is a function whose derivative with respect to time is zero everywhere, then the function f t x is independent of time.

I think I want it to be constant with respect to both space and time, and now I think I have to differentiate with respect to both and combine the results

[ZhiKai Pong]

I think ultimately I want something like this :

code

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example (ht: ∀ t x, fderiv ℝ (fun t => f t x) t = 0) (hx : ∀ t x y, fderiv ℝ (fun x => f t x) x y = 0)
    (hf : Differentiable ℝ ↿f) :
    ∃ C, ∀ t x, f t x = C := by
  have hct : ∀ x, ∃ Ct, ∀ t, f t x = Ct := by
    intro x
    have ht' := fun t => ht t x
    apply is_const_of_fderiv_eq_zero at ht'
    use f 0 x
    intro t
    rw [ht' t 0]
    fun_prop
  have hcx : ∀ t, ∃ Cx, ∀ x, f t x = Cx := by
    intro t
    have hx' : ∀ x, fderiv ℝ (fun x => f t x) x = 0 := by
      intro x
      ext1 y
      rw [hx]
      simp
    apply is_const_of_fderiv_eq_zero at hx'
    use f t 0
    intro x
    rw [hx' x 0]
    fun_prop
  obtain ⟨Ct, ht⟩ := hct 0
  obtain ⟨Cx, hx⟩ := hcx 0
  use (Ct + Cx)
  intro t x
  rw [← ht t, ← hx x]
  have hf : f = Function.curry ↿f := by
    rfl
  rw [hf]
  simp
  have hf_uncurry_add : (↿f) (t, x) = (↿f) ((t, 0) + (0, x)) := by
    congr
    simp
    simp
  rw [hf_uncurry_add]
  rw [← ContinuousLinearMap.map_add] -- need assumption that ↿f is a linear map?

where f is either ElectricField or MagneticField. What's the most idiomatic way to state ElectricField or MagneticField is linear? do I show it follows from Maxwell's equations? I'm not quite sure how

[Joseph Tooby-Smith]

I don't see any reason why an ElectricField or MagneticField should be linear function from space-time to the vector space of electric or magnetic fields.

[ZhiKai Pong]

Yea after typing that out I realized that's obviously false. I think saying that ∃ C, ∀ t x, f t x = C in the context of EMwaves is the correct statement, as in the constant field is independent of space and time. I'm trying to sketch out what's needed to reach this final statement, if what's shown in the above code isn't sufficient or not the right approach.

[Joseph Tooby-Smith]

I agree with this, and I think your code snippet above should be true.

[ZhiKai Pong]

how do I close the final step then?

[Joseph Tooby-Smith]

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example (ht: ∀ t x, fderiv ℝ (fun t => f t x) t = 0)
    (hx : ∀ t x , fderiv ℝ (fun x => f t x) x  = 0)
    (hf : Differentiable ℝ ↿f) :
    ∃ C, ∀ t x, f t x = C := by
  have hct :  ∃ (c : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)), ∀ t, f t = c := by
    use f 0
    intro t
    funext x
    have ht' := fun t => ht t x
    apply is_const_of_fderiv_eq_zero at ht'
    rw [ht' t 0]
    fun_prop
  obtain ⟨c, hc⟩ := hct
  use c 0
  intro t
  rw [hc t]
  have hc_deriv : ∀ x, fderiv ℝ (fun x => c x) x  = 0 := by
    rw [← hc t]
    exact fun x => hx t x
  apply is_const_of_fderiv_eq_zero at hc_deriv
  · intro x
    exact hc_deriv x 0
  · rw [← hc 0]
    fun_prop

[Joseph Tooby-Smith]

(basically just a slight reworking of what you had)

[ZhiKai Pong]

ahhh... I was overthinking it too much, thanks!!

[Joseph Tooby-Smith]

No worries :slight_smile:

[ZhiKai Pong]

@Tomas Skrivan fun_prop solves the second one but not the first one, is this to be expected?

import Mathlib

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

set_option trace.Meta.Tactic.fun_prop true

lemma ContDiff.two_differentiable (f : X → Y → Z) (hf : ContDiff 𝕜 2 ↿f) :
    Differentiable 𝕜 (↿f) := by
  fun_prop --`fun_prop` was unable to prove `Differentiable 𝕜 ↿f`

lemma ContDiff.two_fderiv_differentiable (f : X → Y → Z) (hf : ContDiff 𝕜 2 ↿f) :
    Differentiable 𝕜 (fderiv 𝕜 (↿f)) := by
  fun_prop

[Tomas Skrivan]

There has to be a theorem missing, what is set_option trace.Meta.Tactic.fun_prop true saying?

[ZhiKai Pong]

should ContDiff.differentiable be tagged or is it intentionally left out?

[ZhiKai Pong]

Tomas Skrivan said:

There has to be a theorem missing, what is set_option trace.Meta.Tactic.fun_prop true saying?

`fun_prop` was unable to prove `Differentiable 𝕜 ↿f`

Issues:
  No theorems found for `f` in order to prove `Differentiable 𝕜 fun a => f a.1 a.2`
mathlib-demo.lean:12:2
[Meta.Tactic.fun_prop] [❌️] Differentiable 𝕜 ↿f ▼
  [] candidate local theorems for f #[]
  [] candidate transition theorems: [@IsBoundedBilinearMap.differentiable,
       Differentiable.restrictScalars,
       @IsBoundedLinearMap.differentiable,
       @differentiable_one]
  [] [❌️] applying: IsBoundedBilinearMap.differentiable ▶
  [] [❌️] applying: Differentiable.restrictScalars ▶
  [] [❌️] applying: IsBoundedLinearMap.differentiable ▶
  [] [❌️] applying: ContDiff.differentiable_one ▶

[Tomas Skrivan]

That is intentional, there is ContDiff.differentiable_one. fun_prop can't figure out n in CibtDiff.differentiable

[Tomas Skrivan]

  [] [❌️] applying: ContDiff.differentiable_one ▶

This branch should solve the goal, can you expand it?

[ZhiKai Pong]

expanding error message for ContDiff.differentiable_one:

[] [❌️] applying: ContDiff.differentiable_one ▼
    [] [❌️] ContDiff 𝕜 1 fun a => f a.1 a.2 ▼
      [] candidate local theorems for f #[hf : ContDiff 𝕜 2 ↿f]
      [] [❌️] applying: hf : ContDiff 𝕜 2 ↿f ▼
        [] failed to unify hf
            ContDiff 𝕜 2 ↿f
            with
            ContDiff 𝕜 1 fun a => f a.1 a.2
      [] maximum transition depth (1) reached
              if you want `fun_prop` to continue then increase the maximum depth with `fun_prop (config := {maxTransitionDepth := 2})`
    [] @differentiable_one, failed to discharge hypotheses
          ContDiff 𝕜 1 fun a => f a.1 a.2

[Tomas Skrivan]

Ahh, you need to increase maxTransitionDepth there are two transitions: Differentiable -> ContDiff 1 -> ContDiff 2

[Tomas Skrivan]

fun_prop (maxTransitionDepth := 2) (disch:=aesop) should solve the goal

[Tomas Skrivan]

Or with whatever tactic capable showing 1 <= 2 as discharger

[Tomas Skrivan]

Does it work? (I'm on the phone so I can't test it myself)

[ZhiKai Pong]

yep it works

[Tomas Skrivan]

Maybe the default value of 1 for maxTransitionDepth is too low. Too high value would like to make fun_prop slow in failure cases.

[ZhiKai Pong]

but is this intended? the second one with fderiv surely looks more complicated

[Tomas Skrivan]

ZhiKai Pong said:

but is this intended? the second one with fderiv surely looks more complicated

Yeah it is an unexpected consequence how the tactic work. If you would assume that the function is three times differentiable then the second proof would fail too and would require the same config as the first proof.

[Tomas Skrivan]

Similarly the first proof would work just with fun_prop if you just assume ContDiff 1

[ZhiKai Pong]

would this be fixed in the future or should I just carry around the (maxTransitionDepth := 2) (disch:=aesop) for now?

[Tomas Skrivan]

This all comes from the difficulty of dealing with ContDiff n where you can have different n flying around.

[Tomas Skrivan]

ZhiKai Pong said:

would this be fixed in the future or should I just carry around the (maxTransitionDepth := 2) (disch:=aesop) for now?

For now, use this.

A potential solution could be:

• not to count ContDiff.of_le as a transition theorem
• increase default maxTransitionDepth

Not sure what is a better choice.

[Tomas Skrivan]

Do you get a sensible error when you increase maxTransitionDepth but do not provide a discharger?

[ZhiKai Pong]

If I remove the disch:=aesop this is the error:

`fun_prop` was unable to prove `Differentiable 𝕜 ↿f`

Issues:
  No theorems found for `f` in order to prove `Differentiable 𝕜 fun a => f a.1 a.2`
mathlib-demo.lean:12:2
[Meta.Tactic.fun_prop] [❌️] Differentiable 𝕜 ↿f ▼
  [] candidate local theorems for f #[]
  [] candidate transition theorems: [@IsBoundedBilinearMap.differentiable,
       Differentiable.restrictScalars,
       @IsBoundedLinearMap.differentiable,
       @differentiable_one]
  [] [❌️] applying: IsBoundedBilinearMap.differentiable ▶
  [] [❌️] applying: Differentiable.restrictScalars ▶
  [] [❌️] applying: IsBoundedLinearMap.differentiable ▶
  [] [❌️] applying: ContDiff.differentiable_one ▼
    [] [❌️] ContDiff 𝕜 1 fun a => f a.1 a.2 ▼
      [] candidate local theorems for f #[hf : ContDiff 𝕜 2 ↿f]
      [] [❌️] applying: hf : ContDiff 𝕜 2 ↿f ▼
        [] failed to unify hf
            ContDiff 𝕜 2 ↿f
            with
            ContDiff 𝕜 1 fun a => f a.1 a.2
      [] candidate transition theorems: [@of_le]
      [] [❌️] applying: ContDiff.of_le ▼
        [] [✅️] ContDiff 𝕜 2 fun a => f a.1 a.2 ▶
        [] [❌️] discharging: 1 ≤ 2
        [] @of_le, failed to discharge hypotheses
              1 ≤ 2
    [] @differentiable_one, failed to discharge hypotheses
          ContDiff 𝕜 1 fun a => f a.1 a.2

[Tomas Skrivan]

Yeah this is not good. The error failed to discharge hypotheses, 1 ≤ 2 should show up under Issues at the top but I don't know how to fix that without producing lots of noise messages in other cases.

[Yakov Pechersky]

docs#ContDiff.of_le

[Yakov Pechersky]

Perhaps one can make a variant of that lemmas where the proof obligation has an autoparam?

[Tomas Skrivan]

Yes that would definitely be an option. fun_prop does not run autoParam but I have such a feature working with another tactic so it should be easy to get to work.

[ZhiKai Pong]

thank you Tomas for looking into this :)

[Joseph Tooby-Smith]

Just a quick comment: It is probably worth keeping an eye on #25427, and if it gets merged into Mathlib, how we can use it in PhysLean.

[Joseph Tooby-Smith]

I've added a new file (this PR) containing the div, grad and curl of distributions. These are much more nicely behaved than those of ordinary functions, and I suspect in the long run easier to work with. What needs to be done at some point, is create a good API around them including reproducing the vector identities we have for ordinary functions.

[ZhiKai Pong]

I came across this reference randomly, at the moment it's probably a long way away from formalizable but I feel like this is a good long term goal to work towards and build API around. I hope one day we can build electrodynamics etc. on top of this framework in lean :)

https://www.tandfonline.com/doi/epdf/10.1080/00029890.2002.11919870

[Joseph Tooby-Smith]

If anyone has some free time, I think the following lemma would be nice to prove and add to PhysLean:

import PhysLean.SpaceAndTime.Space.Basic
import PhysLean.SpaceAndTime.Space.VectorIdentities
import Mathlib.Analysis.InnerProductSpace.Calculus
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
import Mathlib.Analysis.Calculus.Gradient.Basic

namespace Space

open InnerProductSpace

lemma grad_dot_unit_vector {d} (x : Space d) (f : Space d → ℝ) :
    ⟪∇ f x, ‖x‖⁻¹ • x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ := by
  sorry

end Space

Open in the online version of PhysLean here.

[Joseph Tooby-Smith]

Never mind - ended up being a simple application of the chain rule:

lemma grad_dot_unit_vector {d} (x : Space d) (f : Space d → ℝ) (hd : Differentiable ℝ f) :
    ⟪∇ f x, ‖x‖⁻¹ • x⟫_ℝ = _root_.deriv (fun r => f (r • ‖x‖⁻¹ • x)) ‖x‖ := by
  by_cases hx : x = 0
  · subst hx
    simp
  symm
  calc _
    _ = fderiv ℝ (f ∘ (fun r => r • ‖x‖⁻¹ • x)) ‖x‖ 1 := by rfl
    _ =  (fderiv ℝ f (‖x‖ • ‖x‖⁻¹ • x)) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) := by
      rw [fderiv_comp _ (by fun_prop) (by fun_prop)]
      simp
    _ = (fderiv ℝ f x) (_root_.deriv (fun r => r • ‖x‖⁻¹ • x) ‖x‖) := by
      have hx : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx
      field_simp [smul_smul]
  rw [grad_inner_eq f x (‖x‖⁻¹ • x)]
  congr
  rw [deriv_smul_const (by fun_prop)]
  simp

[Joseph Tooby-Smith]

FYI, I am planning a big refactor of the vector calculus stuff, primarily to move it into the SpaceAndTime directory, and to put all similar results next to each other. A the minute we have results about derivatives in a number of different modules which is not ideal.

[Joseph Tooby-Smith]

This is done here PhysLean#796, the main things I have done are:

1. Give deriv, curl, div, grad, on Space their own directory. Similar with Time and SpaceTime.
2. Put the derivatives of functions and distributions in the same module
3. Clean up some of the notation.
4. Move all the vector-caculus results to the SpaceAndTime directory.

I've been using lake exe module_doc_lint to help enforce good module documentation, and have followed this in this PR.