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 d⊢ manifoldDeriv 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 d⊢ Differentiable ℝ 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 d⊢ ContDiff ℝ 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) f⊢ ContDiff ℝ 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) f⊢ n + 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 f⊢ ContDiff ℝ (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 d⊢ IsSymmSndFDerivAt ℝ f xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:ContDiff ℝ 2 fx:SpaceTime d⊢ DifferentiableAt ℝ (fderiv ℝ f) xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:ContDiff ℝ 2 fx:SpaceTime d⊢ DifferentiableAt ℝ (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 d⊢ DifferentiableAt ℝ (fderiv ℝ f) xM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:ContDiff ℝ 2 fx:SpaceTime d⊢ DifferentiableAt ℝ (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 d⊢ IsSymmSndFDerivAt ℝ 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 d⊢ minSmoothness ℝ 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 d⊢ DifferentiableAt ℝ f ((Lorentz.Vector.actionCLM Λ) x)M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:Differentiable ℝ fΛ:↑(LorentzGroup d)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(Lorentz.Vector.actionCLM Λ)) x M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:Differentiable ℝ fΛ:↑(LorentzGroup d)x:SpaceTime d⊢ DifferentiableAt ℝ f ((Lorentz.Vector.actionCLM Λ) x)M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:Differentiable ℝ fΛ:↑(LorentzGroup d)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(Lorentz.Vector.actionCLM Λ)) x M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕμ:Fin 1 ⊕ Fin df:SpaceTime d → Mhf:Differentiable ℝ fΛ:↑(LorentzGroup d)x:SpaceTime d⊢ DifferentiableAt ℝ 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 d⊢ DifferentiableAt ℝ (⇑(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)) x⊢ Differentiable ℝ 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)) x⊢ Differentiable ℝ 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⊢ Differentiable ℝ 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⊢ Differentiable ℝ 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 d⊢ Lorentz.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 d⊢ Lorentz.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 d⊢ DifferentiableAt ℝ (fun t => t) ((toTimeAndSpace c) x).1d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mhf:Differentiable ℝ fx:SpaceTime d⊢ DifferentiableAt ℝ (fun t => ((toTimeAndSpace c) x).2) ((toTimeAndSpace c) x).1d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mhf:Differentiable ℝ fx:SpaceTime d⊢ DifferentiableAt ℝ ⇑(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 d⊢ DifferentiableAt ℝ (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 d⊢ DifferentiableAt ℝ (fun t => t) ((toTimeAndSpace c) x).1d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mhf:Differentiable ℝ fx:SpaceTime d⊢ DifferentiableAt ℝ (fun t => ((toTimeAndSpace c) x).2) ((toTimeAndSpace c) x).1d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mhf:Differentiable ℝ fx:SpaceTime d⊢ DifferentiableAt ℝ ⇑(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 d⊢ DifferentiableAt ℝ (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).1⊢ CoVector.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 d⊢ tensorDeriv 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 d⊢ toTensor (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 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 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.univ⊢ Continuous ⇑((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).1⊢ CoVector.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! 🐙