Derivative of Real Lorentz tensors #
noncomputable def
realLorentzTensor.mapToBasis
{d n m : ℕ}
{cm : Fin m → Color}
{cn : Fin n → Color}
(f : (realLorentzTensor d).Tensor cm → (realLorentzTensor d).Tensor cn)
:
(TensorSpecies.Tensor.ComponentIdx cm → ℝ) → TensorSpecies.Tensor.ComponentIdx cn → ℝ
The map between coordinates given a map ℝT(d, cm) → ℝT(d, cn).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
realLorentzTensor.derivative
{d n m : ℕ}
{cm : Fin m → Color}
{cn : Fin n → Color}
(f : (realLorentzTensor d).Tensor cm → (realLorentzTensor d).Tensor cn)
:
(realLorentzTensor d).Tensor cm →
(realLorentzTensor d).Tensor (Sum.elim (fun (i : Fin m) => (realLorentzTensor d).τ (cm i)) cn ∘ ⇑finSumFinEquiv.symm)
The derivative of a function f : ℝT(d, cm) → ℝT(d, cn), giving a function
ℝT(d, cm) → ℝT(d, (Sum.elim cm cn) ∘ finSumFinEquiv.symm).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The derivative of a function f : ℝT(d, cm) → ℝT(d, cn), giving a function
ℝT(d, cm) → ℝT(d, (Sum.elim cm cn) ∘ finSumFinEquiv.symm).
Equations
- realLorentzTensor.«term∂» = Lean.ParserDescr.node `realLorentzTensor.«term∂» 1024 (Lean.ParserDescr.symbol "∂")
Instances For
theorem
realLorentzTensor.derivative_repr
{d n m : ℕ}
{cm : Fin m → Color}
{cn : Fin n → Color}
(f : (realLorentzTensor d).Tensor cm → (realLorentzTensor d).Tensor cn)
(y : (realLorentzTensor d).Tensor cm)
(b :
(j : Fin (m + n)) →
Fin
((realLorentzTensor d).repDim
((Sum.elim (fun (i : Fin m) => (realLorentzTensor d).τ (cm i)) cn ∘ ⇑finSumFinEquiv.symm) j)))
(h1 : DifferentiableAt ℝ (mapToBasis f) (Finsupp.equivFunOnFinite ((TensorSpecies.Tensor.basis cm).repr y)))
:
((TensorSpecies.Tensor.basis
(Sum.elim (fun (i : Fin m) => (realLorentzTensor d).τ (cm i)) cn ∘ ⇑finSumFinEquiv.symm)).repr
(derivative f y))
b = (fderiv ℝ
(fun (y : TensorSpecies.Tensor.ComponentIdx cm → ℝ) =>
mapToBasis f y (TensorSpecies.Tensor.ComponentIdx.splitEquiv b).2)
⇑((TensorSpecies.Tensor.basis cm).repr y))
⇑(Finsupp.single (fun (i : Fin m) => Fin.cast ⋯ ((TensorSpecies.Tensor.ComponentIdx.splitEquiv b).1 i)) 1)