kronecker_symm

formal source

  61/-- Kronecker delta for indices. -/
  62def kronecker {n : ℕ} (μ ν : Fin n) : ℝ := if μ = ν then 1 else 0
  63
  64theorem kronecker_symm {n : ℕ} (μ ν : Fin n) :
  65  kronecker μ ν = kronecker ν μ := by
  66  by_cases h : μ = ν
  67  · simp [kronecker, h]
  68  · have h' : ν ≠ μ := by
  69      intro hνμ
  70      exact h hνμ.symm
  71    simp [kronecker, h, h']
  72
  73theorem kronecker_diag {n : ℕ} (μ : Fin n) :
  74  kronecker μ μ = 1 := by
  75  simp [kronecker]
  76
  77theorem kronecker_off_diag {n : ℕ} (μ ν : Fin n) (h : μ ≠ ν) :
  78  kronecker μ ν = 0 := by
  79  simp [kronecker, h]
  80
  81/-- Partial derivative of a scalar function using a directional derivative along the basis vector. -/
  82noncomputable def partialDeriv {M : Manifold} (f : Point M → ℝ) (μ : Fin M.dim) (x : Point M) : ℝ :=
  83  deriv (fun t => f (fun i => if i = μ then x i + t else x i)) 0
  84
  85
  86end Geometry
  87end Relativity
  88end IndisputableMonolith