Derivative of Real Lorentz tensors

noncomputable def realLorentzTensor.mapToBasis {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C} {cn : Fin n → (realLorentzTensor d).C} (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.

noncomputable def realLorentzTensor.derivative {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C} {cn : Fin n → (realLorentzTensor d).C} (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.

def realLorentzTensor.«term∂» : Lean.ParserDescr

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 "∂")

theorem realLorentzTensor.derivative_repr {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C} {cn : Fin n → (realLorentzTensor d).C} (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)