Using crossProduct in EuclideanSpace (Fin 3)

Stream: new members

[ZhiKai Pong]

I want to work on some vector calculus in EuclideanSpace (Fin 3) in PhysLean but it seems to me that docs#crossProduct is defined more generally? from this discussion #Is there code for X? > generalizing docs#crossProduct over input types is the correct notation still to use the following?

variable (a b : EuclideanSpace ℝ (Fin 3))
WithLp.equiv _ _ a ×₃ WithLp.equiv _ _ b

[Eric Wieser]

Can you make that a #mwe ?

[ZhiKai Pong]

import Mathlib

open Matrix

example
    (B s : EuclideanSpace ℝ (Fin 3))
    (E : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) :
    B = (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ ((fderiv ℝ (fun t => E t x) 1) t)) := by
  sorry

obviously missing a lot of context, but the statement looks something like this, basically I want to show a vector is equal to a cross product of two other vectors but all the WithLp.equiv is quite confusing and I'm just wondering is there a more elegant way to state this

[Eric Wieser]

That looks correct to me, in your original you were missing the outer (WithLp.equiv _ _).symm

[Eric Wieser]

There is ongoing work to make things less clumsy here

[ZhiKai Pong]

I'm trying to prove the following:

import Mathlib

open Matrix

lemma fderiv_cross_commute (s : EuclideanSpace ℝ (Fin 3)) (f : ℝ → EuclideanSpace ℝ (Fin 3)) :
    (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (fderiv ℝ (fun t => f t) t 1))
    =
    fderiv ℝ (fun t => (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (f t))) t 1 := by
  rw [crossProduct]
  simp
  sorry

I can think of two ways:

1. since cross product is bilinear, this is just a composition of fderiv with the second entry
2. after simp as above, differentiation composed with a vector is just a vector of elementwise differentiation of each of the components

but I'm not sure how to state either of those. To be more specific, for (1) I'm still not quite sure how to state composition of continuous linear maps, and for (2) I couldn't find related theorems and don't really understand how matrix/vector is set up

[Kevin Buzzard]

You should use deriv not fderiv as I tried to tell you in the other thread

[ZhiKai Pong]

My understanding is that deriv is not defined as a ContinuousLinearMap, and the first idea wouldn't work.

Also the functions I'm working with are defined in terms of fderiv, and I've only simplified the question so it seems like fderiv properties are not necessary for this particular part, but it's easier for me since I don't have to translate the deriv version back to the fderiv version. If you're suggestion is that asking in terms of deriv makes it easier to understand the question I apologize. Here's the deriv version:

import Mathlib

open Matrix

lemma deriv_cross_commute (s : EuclideanSpace ℝ (Fin 3)) (f : ℝ → EuclideanSpace ℝ (Fin 3)) :
    (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (deriv (fun t => f t) t))
    =
    deriv (fun t => (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (f t))) t := by
  sorry

[Kevin Buzzard]

My understanding is that deriv is not defined as a ContinuousLinearMap, and the first idea wouldn't work.

Oh you're absolutely right, that's definitely an argument for fderiv giving you more. On the other hand every single fderivyou use has 4th argument equal to 1.

[Kevin Buzzard]

Surely you need a differentiability hypothesis on f for this to be true?

[ZhiKai Pong]

you're right, I guess subconsciously I'm still using a physics mindset where everything is assumed to be differentiable, and even in lean differentiability conditions usually come at the end of the proof in the form of new goals so I had the habit of just adding the corresponding assumptions when I have to. Probably this is sufficient:

import Mathlib

open Matrix

lemma deriv_cross_commute (s : EuclideanSpace ℝ (Fin 3)) (f : ℝ → EuclideanSpace ℝ (Fin 3))
    (hf : Differentiable ℝ f) :
    (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (deriv (fun t => f t) t))
    =
    deriv (fun t => (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (f t))) t := by
  sorry

[ZhiKai Pong]

done, just for the record:

import Mathlib

open Matrix

lemma deriv_cross_commute (s : EuclideanSpace ℝ (Fin 3)) (f : ℝ → EuclideanSpace ℝ (Fin 3))
    (hf : Differentiable ℝ f) :
    (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (deriv (fun t => f t) t))
    =
    deriv (fun t => (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv _ _ s ×₃ WithLp.equiv _ _ (f t))) t := by
  have h (u v : Fin 3): s u * deriv (fun t => f t) t v - s v * deriv (fun t => f t) t u =
      deriv (fun t => s u * f t v - s v * f t u) t := by
    rw [deriv_sub, deriv_const_mul, deriv_const_mul]
    rw [deriv_pi]
    intro i
    repeat fun_prop
  rw [crossProduct]
  simp
  ext i
  fin_cases i <;>
  · simp
    rw [h]
    rw [deriv_pi]
    simp
    · intro i
      fin_cases i <;>
      · simp
        fun_prop

[Eric Wieser]

This is probably a version we want in mathlib:

variable {𝕜 𝔸} [NontriviallyNormedField 𝕜] [NormedCommRing 𝔸] [NormedAlgebra 𝕜 𝔸]

protected lemma HasDerivAt.crossProduct {f g : 𝕜 → Fin 3 → 𝔸} {f' g' : Fin 3 → 𝔸} {x : 𝕜}
    (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) :
    HasDerivAt (fun x => f x ×₃ g x) (f' ×₃ g x + f x ×₃ g') x := by
  rw [hasDerivAt_pi] at hf hg
  have h0 := ((hf 1).mul (hg 2)).sub ((hf 2).mul (hg 1))
  have h1 := ((hf 2).mul (hg 0)).sub ((hf 0).mul (hg 2))
  have h2 := ((hf 0).mul (hg 1)).sub ((hf 1).mul (hg 0))
  refine
    (h0.finCons (F' := fun _ => _) (h1.finCons (h2.finCons <| hasDerivAt_const x ![]))).congr_deriv ?_
  rw [← Matrix.vecCons, ← Matrix.vecCons, ← Matrix.vecCons, Subsingleton.elim 0 ![]]
  simp_rw [add_sub_add_comm, ← vec3_add]
  rfl

lemma deriv_crossProduct (f g : 𝕜 → Fin 3 → 𝔸) {x : 𝕜}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    deriv (fun x => f x ×₃ g x) x = deriv f x ×₃ g x + f x ×₃ deriv g x :=
  (hf.hasDerivAt.crossProduct hg.hasDerivAt).deriv

[Eric Wieser]

@Yury G. Kudryashov was right that I should have defined vecCons as well as docs#HasDerivAt.finCons, because the latter si very annoying to use here

[Eric Wieser]

If you showed that crossProduct was continuous in both arguments, you could make the first proof much shorter with docs#ContinuousLinearMap.hasDerivAt_of_bilinear

[Eric Wieser]

Maybe something to note from the above; you don't want to differentiate crossProduct in EuclideanSpace (Fin 3); just differentiate it in Fin 3 → ℝ, and also differentiate through WithLp.equiv.

[ZhiKai Pong]

Eric Wieser said:

Maybe something to note from the above; you don't want to differentiate crossProduct in EuclideanSpace (Fin 3); just differentiate it in Fin 3 → ℝ, and also differentiate through WithLp.equiv.

Are you referring to general computations?

I'm not really trying to do fancy calculations here, my specific use case is that I want to show E = s ×₃ B (+ C) from E' = s ×₃ B', so my logic goes something like

-- "pseudocode"
example (E B : ℝ → EuclideanSpace ℝ (Fin 3)) (h : E' = s ×₃ B') :
    ∃ C, E = (s ×₃ B) + C := by
  have h' : E' = (s ×₃ B)' := by (proof above)
  ...

which I managed to get it to work (with a lot of simps).

[ZhiKai Pong]

Not really a question, but I'm surprised to find that

import Mathlib

variable {R : Type*} [CommRing R]

open Matrix

theorem cross_cross' (u v w : Fin 3 → R) : u ×₃ (v ×₃ w) = (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w := by
  simp [cross_apply, vec3_dotProduct]
  ext i
  fin_cases i <;>
  · simp
    ring

this is not proved in the crossProduct folder. I'm not sure if there's an equivalent for Lie algebra, but this is what I first think of for cross_cross in vector caculus. It's fine if I prove this separately but just wondering would it be useful for Mathlib as well.

[ZhiKai Pong]

(also any suggestions for a name for this? cross_cross refers to something quite different so I'm not sure if just adding a prime causes confusion)

[Eric Wieser]

I'd be ok with cross_cross', but you should probably write the other version with u ×₃ v ×₃ w on the LHS

[ZhiKai Pong]

Eric Wieser said:

I'd be ok with cross_cross', but you should probably write the other version with u ×₃ v ×₃ w on the LHS

do you mean this version is preferred?

import Mathlib

variable {R : Type*} [CommRing R]

open Matrix

theorem cross_cross' (u v w : Fin 3 → R) : u ×₃ v ×₃ w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u := by
  simp [cross_apply, vec3_dotProduct]
  ext i
  fin_cases i <;>
  · simp
    ring

I think the convention I've seen typically uses the other form (e.g. wikipedia) but they are equivalent anyway

[Eric Wieser]

I guess we probably want both versions, but I claim that one should have priority over the cross_cross' name since it matches docs#cross_cross on the LHS

[Eric Wieser]

I guess you could call the two theorems cross_cross_eq_smul_sub_smul and cross_cross_eq_smul_sub_smul'

[ZhiKai Pong]

I'll try to make a PR to mathlib :)

[ZhiKai Pong]

import Mathlib

open Matrix

example (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v (v ×₃ w) =  0  := by
  rw [cross_apply]
  simp
  rw [Finset.sum]
  simp
  ring

is there a simple way that translates inner to docs#vec3_dotProduct?

I would hope that a statement of this form can be transformed into docs#dot_self_cross directly, otherwise I have to pretty much reprove everything currently in docs#crossProduct

[Eric Wieser]

This statement is unfortunately type-incorrect, as I think was alluded to up-thread

[Eric Wieser]

You need to write WithLp.equiv _ _ v before passing it to the cross product operator

[ZhiKai Pong]

Yea I'm aware the full correct form should be

import Mathlib

open Matrix

example (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v ((WithLp.equiv 2 (Fin 3 → ℝ)).symm (WithLp.equiv _ _ v ×₃ WithLp.equiv _ _ w)) =  0  := by
  rw [cross_apply]
  simp
  rw [Finset.sum]
  simp
  ring

(if it is type-incorrect shouldn't it throw an error?)

but then proving this just seems like its duplicating effort from docs#dot_self_cross.

[Eric Wieser]

This seems like the right approach:

import Mathlib

open Matrix

@[elab_as_elim, cases_eliminator]
def WithLp.rec {V} {p} (motive : WithLp p V → Sort*) (toLp : ∀ v, motive ((WithLp.equiv p _).symm v)) : ∀ v, motive v := toLp

example (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v ((WithLp.equiv 2 (Fin 3 → ℝ)).symm (WithLp.equiv _ _ v ×₃ WithLp.equiv _ _ w)) =  0  := by
  cases v using WithLp.rec with | _ v =>
  cases w using WithLp.rec with | _ w =>
  simp [-PiLp.inner_apply, EuclideanSpace.inner_piLp_equiv_symm]
  rw [dotProduct_comm, dot_self_cross]

[Eric Wieser]

I guess we should also increase the priority on docs#EuclideanSpace.inner_piLp_equiv_symm

[ZhiKai Pong]

thanks... I guess technically that's what I want but to me just expanding everything out is simpler at the moment. this looks more like what I expect to be the underlying API for what you mentioned about better support for vectors in EuclideanSpace ℝ (Fin 3)? I'll keep a mental note of this, thanks again :)

[Eric Wieser]

I think the way to think about this is that, because there is no support for cross product in EuclideanSpace, you should start your proof by leaving euclidean space. The WithLp.rec above (#25193) is the easiest way to do that.

[Eric Wieser]

ZhiKai Pong said:

(if it is type-incorrect shouldn't it throw an error?)

Ideally, yes; the issue here is that it's type correct according to the Lean kernel, but not according to how the API is written. Writing things wrongly will just strand you in a place where very few lemmas apply, making it more likely that you resort to proving things from scratch.

[ZhiKai Pong]

import Mathlib

open Matrix

example (c: ℝ) (u v : Fin 3 → ℝ) : u ×₃ (c • v) = c • u ×₃ v := by
  rw [← cross_anticomm]
  apply LinearMap.map_smul₂ --doesn't work

example (c: ℝ) (u v : EuclideanSpace ℝ (Fin 3)) : (WithLp.equiv 2 (Fin 3 → ℝ)).symm (WithLp.equiv 2 (Fin 3 → ℝ) u) ×₃
    (WithLp.equiv 2 (Fin 3 → ℝ) (c • v)) = c • (WithLp.equiv 2 (Fin 3 → ℝ) u) ×₃ (WithLp.equiv 2 (Fin 3 → ℝ) v) := by
  rw [← cross_anticomm]
  apply LinearMap.map_smul₂

Is there a more standard way to prove this? I can expand everything out, (i.e. rw [crossProduct]; simp works) but I'm not sure what's the proper way of proving this. (I want to prove the second one but I hope the proof would work for both versions.)

[Kenny Lau]

@ZhiKai Pong

example (c: ℝ) (u v : Fin 3 → ℝ) : u ×₃ (c • v) = c • u ×₃ v := by
  rw [LinearMap.map_smul]

[Kenny Lau]

@ZhiKai Pong

example (c: ℝ) (u v : EuclideanSpace ℝ (Fin 3)) : (WithLp.equiv 2 (Fin 3 → ℝ)).symm (WithLp.equiv 2 (Fin 3 → ℝ) u) ×₃
    (WithLp.equiv 2 (Fin 3 → ℝ) (c • v)) = c • (WithLp.equiv 2 (Fin 3 → ℝ) u) ×₃ (WithLp.equiv 2 (Fin 3 → ℝ) v) := by
  rw [WithLp.equiv_smul, LinearMap.map_smul]
  rfl

I don't know what's going on here, I'm confused by too many WithLp.equiv

[Kenny Lau]

since WithLp is a type synonyms everything ends up being definitionally equal

[ZhiKai Pong]

@Kenny Lau My understanding is that it has something to do with #mathlib4 > defeq abuse in `WithLp` @ 💬 , but I'm still learning and not entirely sure. @Eric Wieser can probably give you a better explanation.

[Notification Bot]

A message was moved from this topic to #mathlib4 > Notation for crossProduct by Eric Wieser.