Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.SpaceTime.LorentzAction public import Physlib.Relativity.Tensors.RealTensor.CoVector.Tensorial public import Mathlib.Analysis.InnerProductSpace.TensorProduct public import Physlib.SpaceAndTime.Space.Derivatives.Basic public import Physlib.SpaceAndTime.Time.Derivatives

Derivatives on SpaceTime

i. Overview

In this module we define and prove basic lemmas about derivatives of functions and distributions on SpaceTime d.

ii. Key results

    deriv : The derivative of a function SpaceTime d → M along the μ coordinate.

    manifoldDeriv : The derivative of a function from SpaceTime d to a manifold along the μ coordinate.

    contDiff_deriv : If f is C^{n+1} then ∂_ μ f is C^n.

    differentiable_deriv : If f is C^2 then ∂_ μ f is differentiable.

    deriv_commute : Derivatives on SpaceTime d commute (Clairaut's theorem).

    deriv_sum_inr : The derivative along a spatial coordinate in terms of the derivative on Space d.

    deriv_sum_inl : The derivative along the temporal coordinate in terms of the derivative on Time.

    distDeriv : The derivative of a distribution on SpaceTime d along the μ coordinate.

    distDeriv_commute : Derivatives of distributions on SpaceTime d commute.

iii. Table of contents

    A. Derivatives of functions on SpaceTime d

      A.1. The definition of the derivative

      A.2. Basic equality lemmas

      A.3. Derivative of the zero function

      A.4. Smoothness and differentiability of the derivative

      A.5. Derivatives commute

      A.6. The derivative of a function composed with a Lorentz transformation

      A.7. Spacetime derivatives in terms of time and space derivatives

    B. Derivatives of distributions

      B.1. Commutation of derivatives of distributions

      B.2. Lorentz group action on derivatives of distributions

    C. Derivatives of tensors

      C.1. Derivatives of tensors for distributions

iv. References

@[expose] public section

A. Derivatives of functions on SpaceTime d

A.1. The definition of the derivative

@[inherit_doc deriv] scoped notation "∂_" => derivlemma deriv_eq {M : Type} [AddCommGroup M] [Module M] [TopologicalSpace M] {d : } (μ : Fin 1 Fin d) (f : SpaceTime d M) (y : SpaceTime d) : ∂_ μ f y = fderiv f y (Lorentz.Vector.basis μ) := M:Typeinst✝²:AddCommGroup Minst✝¹:Module Minst✝:TopologicalSpace Md:μ:Fin 1 Fin df:SpaceTime d My:SpaceTime d∂_ μ f y = (fderiv f y) (Lorentz.Vector.basis μ) All goals completed! 🐙lemma manifoldDeriv_eq {E H N : Type} [NormedAddCommGroup E] [NormedSpace E] [TopologicalSpace H] (I : ModelWithCorners E H) [TopologicalSpace N] [ChartedSpace H N] {d : } (μ : Fin 1 Fin d) (f : SpaceTime d N) (y : SpaceTime d) : manifoldDeriv I μ f y = mfderiv 𝓘(, SpaceTime d) I f y ((Lorentz.Vector.basis μ : SpaceTime d) : TangentSpace 𝓘(, SpaceTime d) y) := rfl

The spacetime derivative is the manifold derivative for functions into normed spaces.

M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d My:SpaceTime d(mfderiv% f y) (Lorentz.Vector.basis μ) = (mfderiv% f y) (Lorentz.Vector.basis μ) All goals completed! 🐙
All goals completed! 🐙@[simp] lemma manifoldDeriv_const {E H N : Type} [NormedAddCommGroup E] [NormedSpace E] [TopologicalSpace H] (I : ModelWithCorners E H) [TopologicalSpace N] [ChartedSpace H N] {d : } (μ : Fin 1 Fin d) (n : N) (y : SpaceTime d) : manifoldDeriv I μ (fun _ : SpaceTime d => n) y = 0 := E:TypeH:TypeN:Typeinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace Einst✝²:TopologicalSpace HI:ModelWithCorners E Hinst✝¹:TopologicalSpace Ninst✝:ChartedSpace H Nd:μ:Fin 1 Fin dn:Ny:SpaceTime dmanifoldDeriv I μ (fun x => n) y = 0 All goals completed! 🐙

A.2. Basic equality lemmas

d:f:SpaceTime d Lorentz.Vector dh: (ν : Fin 1 Fin d), Differentiable fun x => f x νDifferentiable ((Lorentz.Vector.equivPi d) f) All goals completed! 🐙 d:f:SpaceTime d Lorentz.Vector dh:Differentiable fν:Fin 1 Fin dDifferentiable fun x => f x ν All goals completed! 🐙n:WithTop ℕ∞d:f:SpaceTime d Lorentz.Vector dh: (ν : Fin 1 Fin d), ContDiff n fun x => f x νContDiff n ((Lorentz.Vector.equivPi d) f) All goals completed! 🐙 n:WithTop ℕ∞d:f:SpaceTime d Lorentz.Vector dh:ContDiff n fν:Fin 1 Fin dContDiff n fun x => f x ν All goals completed! 🐙d:f:SpaceTime d Lorentz.Vector dhf:Differentiable fy:SpaceTime ddt:SpaceTime dν:Fin 1 Fin d(fderiv f y) dt ν = (fderiv (⇑(Lorentz.Vector.coordCLM ν)) (f y) ∘SL fderiv f y) dt All goals completed! 🐙lemma deriv_apply_eq {d : } (μ ν : Fin 1 Fin d) (f : SpaceTime d Lorentz.Vector d) (hf : Differentiable f) (y : SpaceTime d) : ∂_ μ f y ν = fderiv (fun x => f x ν) y (Lorentz.Vector.basis μ) := fderiv_vector f hf y _ νd:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime d(fderiv (⇑(coordCLM ν)) x) (Lorentz.Vector.basis μ) = (if μ = ν then 1 else 0) x d:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime d(coordCLM ν) (Lorentz.Vector.basis μ) = (if μ = ν then 1 else 0) x d:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime d(if μ = ν then 1 else 0) = (if μ = ν then 1 else 0) x d:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime dh✝:μ = ν1 = 1 xd:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime dh✝:¬μ = ν0 = 0 x d:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime dh✝:μ = ν1 = 1 xd:μ:Fin 1 Fin dν:Fin 1 Fin dx:SpaceTime dh✝:¬μ = ν0 = 0 x All goals completed! 🐙

A.3. Derivative of the zero function

@[simp] lemma deriv_zero {d : } (μ : Fin 1 Fin d) : SpaceTime.deriv μ (fun _ => (0 : )) = 0 := d:μ:Fin 1 Fin d(∂_ μ fun x => 0) = 0 d:μ:Fin 1 Fin dy:SpaceTime d∂_ μ (fun x => 0) y = 0 y All goals completed! 🐙attribute [-simp] Fintype.sum_sum_type

A.4. Smoothness and differentiability of the derivative

If f is C^{n+1} then ∂_ μ f is C^n.

@[fun_prop] lemma contDiff_deriv {M : Type} [NormedAddCommGroup M] [NormedSpace M] {d : } {n : WithTop ℕ∞} (μ : Fin 1 Fin d) (f : SpaceTime d M) (hf : ContDiff (n + 1) f) : ContDiff n (∂_ μ f) := M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:n:WithTop ℕ∞μ:Fin 1 Fin df:SpaceTime d Mhf:ContDiff (n + 1) fContDiff n (∂_ μ f) -- `∂_ μ f = fun x => fderiv ℝ f x (Lorentz.Vector.basis μ)`; use -- `ContDiff.clm_apply` with `ContDiff.fderiv_right`. exact (ContDiff.fderiv_right (m := n) hf (M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:n:WithTop ℕ∞μ:Fin 1 Fin df:SpaceTime d Mhf:ContDiff (n + 1) fn + 1 n + 1 All goals completed! 🐙)).clm_apply contDiff_const

If f is C^2 then ∂_ μ f is differentiable.

@[fun_prop] lemma differentiable_deriv {M : Type} [NormedAddCommGroup M] [NormedSpace M] {d : } (μ : Fin 1 Fin d) (f : SpaceTime d M) (hf : ContDiff 2 f) : Differentiable (∂_ μ f) := (contDiff_deriv μ f (n := 1) (M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fContDiff (1 + 1) f All goals completed! 🐙)).differentiable one_ne_zero

A.5. Derivatives commute

Derivatives on spacetime commute with one another (Clairaut's theorem).

M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dIsSymmSndFDerivAt f xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dDifferentiableAt (fderiv f) xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dDifferentiableAt (fun y => Lorentz.Vector.basis μ) xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dDifferentiableAt (fderiv f) xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dDifferentiableAt (fun y => Lorentz.Vector.basis ν) x M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dIsSymmSndFDerivAt f x exact hf.contDiffAt.isSymmSndFDerivAt (M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin dν:Fin 1 Fin df:SpaceTime d Mhf:ContDiff 2 fx:SpaceTime dminSmoothness 2 2 All goals completed! 🐙) all_goals All goals completed! 🐙

A.6. The derivative of a function composed with a Lorentz transformation

M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime d(fderiv f (Λ x)) (∑ ν, Λ ν μ Lorentz.Vector.basis ν) = ν, Λ ν μ ∂_ ν f (Λ x)M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime dDifferentiableAt f ((Lorentz.Vector.actionCLM Λ) x)M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime dDifferentiableAt (⇑(Lorentz.Vector.actionCLM Λ)) x M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime dDifferentiableAt f ((Lorentz.Vector.actionCLM Λ) x)M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime dDifferentiableAt (⇑(Lorentz.Vector.actionCLM Λ)) x M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime dDifferentiableAt f ((Lorentz.Vector.actionCLM Λ) x) All goals completed! 🐙 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Md:μ:Fin 1 Fin df:SpaceTime d Mhf:Differentiable fΛ:(LorentzGroup d)x:SpaceTime dDifferentiableAt (⇑(Lorentz.Vector.actionCLM Λ)) x All goals completed! 🐙n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fμ:Fin 1 Fin dh1: (μ : Fin 1 Fin d) (x : SpaceTime d), ∂_ μ (fun x => Λ f (Λ⁻¹ x)) x = Λ ∂_ μ (fun x => f (Λ⁻¹ x)) xΛ ν, Λ⁻¹ ν μ ∂_ ν f (Λ⁻¹ x) = ν, Λ⁻¹ ν μ Λ ∂_ ν f (Λ⁻¹ x)n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fμ:Fin 1 Fin dh1: (μ : Fin 1 Fin d) (x : SpaceTime d), ∂_ μ (fun x => Λ f (Λ⁻¹ x)) x = Λ ∂_ μ (fun x => f (Λ⁻¹ x)) xDifferentiable f n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fμ:Fin 1 Fin dh1: (μ : Fin 1 Fin d) (x : SpaceTime d), ∂_ μ (fun x => Λ f (Λ⁻¹ x)) x = Λ ∂_ μ (fun x => f (Λ⁻¹ x)) x(Tensorial.actionCLM (realLorentzTensor d) Λ) (∑ ν, Λ⁻¹ ν μ ∂_ ν f (Λ⁻¹ x)) = ν, Λ⁻¹ ν μ Λ ∂_ ν f (Λ⁻¹ x)n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fμ:Fin 1 Fin dh1: (μ : Fin 1 Fin d) (x : SpaceTime d), ∂_ μ (fun x => Λ f (Λ⁻¹ x)) x = Λ ∂_ μ (fun x => f (Λ⁻¹ x)) xDifferentiable f n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fμ:Fin 1 Fin dh1: (μ : Fin 1 Fin d) (x : SpaceTime d), ∂_ μ (fun x => Λ f (Λ⁻¹ x)) x = Λ ∂_ μ (fun x => f (Λ⁻¹ x)) xDifferentiable f n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fμ:Fin 1 Fin dh1: (μ : Fin 1 Fin d) (x : SpaceTime d), ∂_ μ (fun x => Λ f (Λ⁻¹ x)) x = Λ ∂_ μ (fun x => f (Λ⁻¹ x)) xDifferentiable f All goals completed! 🐙

A.7. Spacetime derivatives in terms of time and space derivatives

d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime di:Fin dLorentz.Vector.basis (Sum.inr i) = (toTimeAndSpace c).symm ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))) All goals completed! 🐙 d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime di:Fin d(toTimeAndSpace c).symm (0, Space.basis i) = (toTimeAndSpace c).symm (0, Space.basis i) All goals completed! 🐙 repeat' All goals completed! 🐙d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dLorentz.Vector.basis (Sum.inl 0) = (toTimeAndSpace c).symm ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0)))d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (fun t => t) ((toTimeAndSpace c) x).1d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (fun t => ((toTimeAndSpace c) x).2) ((toTimeAndSpace c) x).1d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (toTimeAndSpace c).symm (((toTimeAndSpace c) x).1, ((toTimeAndSpace c) x).2)d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (fun t => (t, ((toTimeAndSpace c) x).2)) ((toTimeAndSpace c) x).1 d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (fun t => t) ((toTimeAndSpace c) x).1d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (fun t => ((toTimeAndSpace c) x).2) ((toTimeAndSpace c) x).1d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (toTimeAndSpace c).symm (((toTimeAndSpace c) x).1, ((toTimeAndSpace c) x).2)d:M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mc:SpeedOfLightf:SpaceTime d Mhf:Differentiable fx:SpaceTime dDifferentiableAt (fun t => (t, ((toTimeAndSpace c) x).2)) ((toTimeAndSpace c) x).1 repeat' All goals completed! 🐙

B. Derivatives of distributions

lemma distDeriv_apply {M d} [NormedAddCommGroup M] [NormedSpace M] (μ : Fin 1 Fin d) (f : (SpaceTime d) →d[] M) (ε : 𝓢(SpaceTime d, )) : distDeriv μ f ε = fderivD f ε (Lorentz.Vector.basis μ) := M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin df:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )((distDeriv μ) f) ε = (((fderivD ) f) ε) (Lorentz.Vector.basis μ) All goals completed! 🐙lemma distDeriv_apply' {M d} [NormedAddCommGroup M] [NormedSpace M] (μ : Fin 1 Fin d) (f : (SpaceTime d) →d[] M) (ε : 𝓢(SpaceTime d, )) : distDeriv μ f ε = - f ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ε)) := M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin df:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )((distDeriv μ) f) ε = -f ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ε)) All goals completed! 🐙lemma apply_fderiv_eq_distDeriv {M d} [NormedAddCommGroup M] [NormedSpace M] (μ : Fin 1 Fin d) (f : (SpaceTime d) →d[] M) (ε : 𝓢(SpaceTime d, )) : f ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ε)) = - distDeriv μ f ε := M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin df:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )f ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ε)) = -((distDeriv μ) f) ε All goals completed! 🐙

B.1. Commutation of derivatives of distributions

lemma distDeriv_commute {M d} [NormedAddCommGroup M] [NormedSpace M] (μ ν : Fin 1 Fin d) (f : (SpaceTime d) →d[] M) : distDeriv μ (distDeriv ν f) = distDeriv ν (distDeriv μ f) := M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin dν:Fin 1 Fin df:(SpaceTime d)→d[] M(distDeriv μ) ((distDeriv ν) f) = (distDeriv ν) ((distDeriv μ) f) M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin dν:Fin 1 Fin df:(SpaceTime d)→d[] Mκ:𝓢(SpaceTime d, )((distDeriv μ) ((distDeriv ν) f)) κ = ((distDeriv ν) ((distDeriv μ) f)) κ M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin dν:Fin 1 Fin df:(SpaceTime d)→d[] Mκ:𝓢(SpaceTime d, )f ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis ν)) ((fderivCLM (SpaceTime d) ) ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) κ)))) = f ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis ν)) ((fderivCLM (SpaceTime d) ) κ)))) M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin dν:Fin 1 Fin df:(SpaceTime d)→d[] Mκ:𝓢(SpaceTime d, )(SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis ν)) ((fderivCLM (SpaceTime d) ) ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) κ))) = (SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis ν)) ((fderivCLM (SpaceTime d) ) κ))) M:Typed:inst✝¹:NormedAddCommGroup Minst✝:NormedSpace Mμ:Fin 1 Fin dν:Fin 1 Fin df:(SpaceTime d)→d[] Mκ:𝓢(SpaceTime d, )x:SpaceTime d((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis ν)) ((fderivCLM (SpaceTime d) ) ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) κ)))) x = ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis μ)) ((fderivCLM (SpaceTime d) ) ((SchwartzMap.evalCLM (SpaceTime d) (Lorentz.Vector.basis ν)) ((fderivCLM (SpaceTime d) ) κ)))) x All goals completed! 🐙

B.2. Lorentz group action on derivatives of distributions

We now show how the Lorentz group action on distributions interacts with derivatives.

n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mμ:Fin 1 Fin dΛ:(LorentzGroup d)f:(SpaceTime d)→d[] Mx:SpaceTime dη:𝓢(SpaceTime d, ) ν, Λ⁻¹ ν μ ∂_ ν (⇑η) (Λ⁻¹ Λ x) = x_1, Λ⁻¹ x_1 μ * ∂_ x_1 (⇑η) xn:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mμ:Fin 1 Fin dΛ:(LorentzGroup d)f:(SpaceTime d)→d[] Mx:SpaceTime dη:𝓢(SpaceTime d, )Differentiable η n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mμ:Fin 1 Fin dΛ:(LorentzGroup d)f:(SpaceTime d)→d[] Mx:SpaceTime dη:𝓢(SpaceTime d, )Differentiable η All goals completed! 🐙

C. Derivatives of tensors

Given a function f : SpaceTime d → M where M is a tensor space, we can define the derivative of f as a tensor. In particular this is ∂_μ f viewed as a tensor in Lorentz.CoVector d ⊗[ℝ] M.

The derivative of a tensor, as a tensor.

def tensorDeriv (f : SpaceTime d M) : SpaceTime d Lorentz.CoVector d ⊗[] M := fun x => μ, (Lorentz.CoVector.basis μ) ⊗ₜ (∂_ μ f x)
n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable f y, x_1, (Λ⁻¹ y x_1 Lorentz.CoVector.basis x_1) ⊗ₜ[] (Λ ∂_ y f (Λ⁻¹ x)) = Λ μ, Lorentz.CoVector.basis μ ⊗ₜ[] ∂_ μ f (Λ⁻¹ x) conv_lhs => n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fν:Fin 1 Fin d| x_1, (Λ⁻¹ ν x_1 Lorentz.CoVector.basis x_1) ⊗ₜ[] (Λ ∂_ ν f (Λ⁻¹ x)) n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable fν:Fin 1 Fin d| Λ Lorentz.CoVector.basis ν ⊗ₜ[] ∂_ ν f (Λ⁻¹ x) n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d MΛ:(LorentzGroup d)x:SpaceTime dhf:Differentiable f ν, Λ Lorentz.CoVector.basis ν ⊗ₜ[] ∂_ ν f (Λ⁻¹ x) = (Tensorial.smulLinearMap Λ) (∑ μ, Lorentz.CoVector.basis μ ⊗ₜ[] ∂_ μ f (Λ⁻¹ x)) All goals completed! 🐙n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)μ:Fin 1 Fin dν:ComponentIdx ch1: (x : SpaceTime d), ((basis c).repr (toTensor (f x))) ν = (ContinuousLinearMap.proj ν ∘SL ((basis c).map toTensor.symm).equivFunL) (f x)((basis c).repr (toTensor (∂_ μ f x))) ν = ((ContinuousLinearMap.proj ν ∘SL ((basis c).map toTensor.symm).equivFunL) ∘SL fderiv f x) (Vector.basis μ) All goals completed! 🐙 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c) b_1 Finset.univ, b_1 CoVector.indexEquiv (ComponentIdx.prod b).1 (if CoVector.indexEquiv.symm b_1 = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (∂_ b_1 f x))) (ComponentIdx.prod b).2 else 0) = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)b':Fin 1 Fin da✝:b' Finset.univhb:b' CoVector.indexEquiv (ComponentIdx.prod b).1(if CoVector.indexEquiv.symm b' = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (∂_ b' f x))) (ComponentIdx.prod b).2 else 0) = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)b':Fin 1 Fin da✝:b' Finset.univhb:b' CoVector.indexEquiv (ComponentIdx.prod b).1CoVector.indexEquiv.symm b' = (ComponentIdx.prod b).1 ((basis c).repr (toTensor (∂_ b' f x))) (ComponentIdx.prod b).2 = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)b':Fin 1 Fin da✝:b' Finset.univhb:b' CoVector.indexEquiv (ComponentIdx.prod b).1hx:CoVector.indexEquiv.symm b' = (ComponentIdx.prod b).1((basis c).repr (toTensor (∂_ b' f x))) (ComponentIdx.prod b).2 = 0 All goals completed! 🐙 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)CoVector.indexEquiv (ComponentIdx.prod b).1 Finset.univ (if CoVector.indexEquiv.symm (CoVector.indexEquiv (ComponentIdx.prod b).1) = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (∂_ (CoVector.indexEquiv (ComponentIdx.prod b).1) f x))) (ComponentIdx.prod b).2 else 0) = 0 All goals completed! 🐙

The expansion of tensorDeriv in terms of the tensor basis vector.

lemma tensorDeriv_eq_sum_tensor_basis {f : SpaceTime d M} (hf : Differentiable f) (x : SpaceTime d) : tensorDeriv f x = b, ∂_ (CoVector.indexEquiv (ComponentIdx.prod b).1) (fun x => (Tensor.basis _).repr (toTensor (f x)) (ComponentIdx.prod b).2) x toTensor.symm (Tensor.basis _ b) := n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime dtensorDeriv f x = b, ∂_ (CoVector.indexEquiv (ComponentIdx.prod b).1) (fun x => ((basis c).repr (toTensor (f x))) (ComponentIdx.prod b).2) x toTensor.symm ((basis (Fin.append ![realLorentzTensor.Color.down] c)) b) n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime dtoTensor (tensorDeriv f x) = toTensor (∑ b, ∂_ (CoVector.indexEquiv (ComponentIdx.prod b).1) (fun x => ((basis c).repr (toTensor (f x))) (ComponentIdx.prod b).2) x toTensor.symm ((basis (Fin.append ![realLorentzTensor.Color.down] c)) b)) n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime d(basis (Fin.append ![realLorentzTensor.Color.down] c)).repr (toTensor (tensorDeriv f x)) = (basis (Fin.append ![realLorentzTensor.Color.down] c)).repr (toTensor (∑ b, ∂_ (CoVector.indexEquiv (ComponentIdx.prod b).1) (fun x => ((basis c).repr (toTensor (f x))) (ComponentIdx.prod b).2) x toTensor.symm ((basis (Fin.append ![realLorentzTensor.Color.down] c)) b))) n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space Mf:SpaceTime d Mhf:Differentiable fx:SpaceTime db:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)((basis (Fin.append ![realLorentzTensor.Color.down] c)).repr (toTensor (tensorDeriv f x))) b = ((basis (Fin.append ![realLorentzTensor.Color.down] c)).repr (toTensor (∑ b, ∂_ (CoVector.indexEquiv (ComponentIdx.prod b).1) (fun x => ((basis c).repr (toTensor (f x))) (ComponentIdx.prod b).2) x toTensor.symm ((basis (Fin.append ![realLorentzTensor.Color.down] c)) b)))) b All goals completed! 🐙

C.1. Derivatives of tensors for distributions

The derivative of a tensor, as a tensor for distributions.

n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf:(SpaceTime d)→d[] Mμ:Fin 1 Fin dx✝:μ Finset.univw:Finset Mb:OrthonormalBasis w Mhb1:b = Subtype.valh1: (y : M), CoVector.basis μ ⊗ₜ[] y = i, b i, y⟫_ CoVector.basis μ ⊗ₜ[] b iContinuous fun y => CoVector.basis μ ⊗ₜ[] y n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf:(SpaceTime d)→d[] Mμ:Fin 1 Fin dx✝:μ Finset.univw:Finset Mb:OrthonormalBasis w Mhb1:b = Subtype.valh1: (y : M), CoVector.basis μ ⊗ₜ[] y = i, b i, y⟫_ CoVector.basis μ ⊗ₜ[] b i| Continuous fun y => CoVector.basis μ ⊗ₜ[] y n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf:(SpaceTime d)→d[] Mμ:Fin 1 Fin dx✝:μ Finset.univw:Finset Mb:OrthonormalBasis w Mhb1:b = Subtype.valh1: (y : M), CoVector.basis μ ⊗ₜ[] y = i, b i, y⟫_ CoVector.basis μ ⊗ₜ[] b iy:M| CoVector.basis μ ⊗ₜ[] y; n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf:(SpaceTime d)→d[] Mμ:Fin 1 Fin dx✝:μ Finset.univw:Finset Mb:OrthonormalBasis w Mhb1:b = Subtype.valh1: (y : M), CoVector.basis μ ⊗ₜ[] y = i, b i, y⟫_ CoVector.basis μ ⊗ₜ[] b iy:M| i, b i, y⟫_ CoVector.basis μ ⊗ₜ[] b i All goals completed! 🐙 n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf:(SpaceTime d)→d[] Mμ:Fin 1 Fin dx✝:μ Finset.univContinuous ((distDeriv μ) f) All goals completed! 🐙 } map_add' f1 f2 := n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf1:(SpaceTime d)→d[] Mf2:(SpaceTime d)→d[] M{ toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) (f1 + f2)) ε, map_add' := , map_smul' := , cont := } = { toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f1) ε, map_add' := , map_smul' := , cont := } + { toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f2) ε, map_add' := , map_smul' := , cont := } n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf1:(SpaceTime d)→d[] Mf2:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, ){ toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) (f1 + f2)) ε, map_add' := , map_smul' := , cont := } ε = ({ toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f1) ε, map_add' := , map_smul' := , cont := } + { toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f2) ε, map_add' := , map_smul' := , cont := }) ε All goals completed! 🐙 map_smul' a f := n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Ma:f:(SpaceTime d)→d[] M{ toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) (a f)) ε, map_add' := , map_smul' := , cont := } = (RingHom.id ) a { toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f) ε, map_add' := , map_smul' := , cont := } n:d✝:M✝¹:Typeinst✝⁹:AddCommGroup M✝¹inst✝⁸:Module M✝¹inst✝⁷:TopologicalSpace M✝¹c:Fin n realLorentzTensor.ColorM✝:Typeinst✝⁶:NormedAddCommGroup M✝inst✝⁵:NormedSpace M✝inst✝⁴:(realLorentzTensor d✝).Tensorial c M✝inst✝³:T2Space M✝M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Ma:f:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, ){ toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) (a f)) ε, map_add' := , map_smul' := , cont := } ε = ((RingHom.id ) a { toFun := fun ε => μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f) ε, map_add' := , map_smul' := , cont := }) ε All goals completed! 🐙
lemma distTensorDeriv_apply {M d} [NormedAddCommGroup M] [InnerProductSpace M] [FiniteDimensional M] (f : (SpaceTime d) →d[] M) (ε : 𝓢(SpaceTime d, )) : distTensorDeriv f ε = μ, (Lorentz.CoVector.basis μ) ⊗ₜ distDeriv μ f ε := M:Typed:inst✝²:NormedAddCommGroup Minst✝¹:InnerProductSpace Minst✝:FiniteDimensional Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )(distTensorDeriv f) ε = μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f) ε All goals completed! 🐙n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] MΛ:(LorentzGroup d)ε:𝓢(SpaceTime d, ) ν, Λ CoVector.basis ν ⊗ₜ[] ((distDeriv ν) f) ((schwartzAction Λ⁻¹) ε) = (smulLinearMap Λ) (∑ μ, CoVector.basis μ ⊗ₜ[] ((distDeriv μ) f) ((schwartzAction Λ⁻¹) ε)) All goals completed! 🐙n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)(if CoVector.indexEquiv.symm (CoVector.indexEquiv (ComponentIdx.prod b).1) = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv (CoVector.indexEquiv (ComponentIdx.prod b).1)) f) ε))) (ComponentIdx.prod b).2 else 0) = ((basis c).repr (toTensor (((distDeriv (CoVector.indexEquiv (ComponentIdx.prod b).1)) f) ε))) (ComponentIdx.prod b).2n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c) b_1 Finset.univ, b_1 CoVector.indexEquiv (ComponentIdx.prod b).1 (if CoVector.indexEquiv.symm b_1 = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv b_1) f) ε))) (ComponentIdx.prod b).2 else 0) = 0n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)CoVector.indexEquiv (ComponentIdx.prod b).1 Finset.univ (if CoVector.indexEquiv.symm (CoVector.indexEquiv (ComponentIdx.prod b).1) = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv (CoVector.indexEquiv (ComponentIdx.prod b).1)) f) ε))) (ComponentIdx.prod b).2 else 0) = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)(if CoVector.indexEquiv.symm (CoVector.indexEquiv (ComponentIdx.prod b).1) = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv (CoVector.indexEquiv (ComponentIdx.prod b).1)) f) ε))) (ComponentIdx.prod b).2 else 0) = ((basis c).repr (toTensor (((distDeriv (CoVector.indexEquiv (ComponentIdx.prod b).1)) f) ε))) (ComponentIdx.prod b).2 All goals completed! 🐙 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c) b_1 Finset.univ, b_1 CoVector.indexEquiv (ComponentIdx.prod b).1 (if CoVector.indexEquiv.symm b_1 = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv b_1) f) ε))) (ComponentIdx.prod b).2 else 0) = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)b':Fin 1 Fin da✝:b' Finset.univhb:b' CoVector.indexEquiv (ComponentIdx.prod b).1(if CoVector.indexEquiv.symm b' = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv b') f) ε))) (ComponentIdx.prod b).2 else 0) = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)b':Fin 1 Fin da✝:b' Finset.univhb:b' CoVector.indexEquiv (ComponentIdx.prod b).1CoVector.indexEquiv.symm b' = (ComponentIdx.prod b).1 ((basis c).repr (toTensor (((distDeriv b') f) ε))) (ComponentIdx.prod b).2 = 0 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)b':Fin 1 Fin da✝:b' Finset.univhb:b' CoVector.indexEquiv (ComponentIdx.prod b).1hx:CoVector.indexEquiv.symm b' = (ComponentIdx.prod b).1((basis c).repr (toTensor (((distDeriv b') f) ε))) (ComponentIdx.prod b).2 = 0 All goals completed! 🐙 n:d:c:Fin n realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:InnerProductSpace Minst✝¹:FiniteDimensional Minst✝:(realLorentzTensor d).Tensorial c Mf:(SpaceTime d)→d[] Mε:𝓢(SpaceTime d, )b:ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)CoVector.indexEquiv (ComponentIdx.prod b).1 Finset.univ (if CoVector.indexEquiv.symm (CoVector.indexEquiv (ComponentIdx.prod b).1) = (ComponentIdx.prod b).1 then ((basis c).repr (toTensor (((distDeriv (CoVector.indexEquiv (ComponentIdx.prod b).1)) f) ε))) (ComponentIdx.prod b).2 else 0) = 0 All goals completed! 🐙