basisVec_self

formal source

  11/-- Standard basis vector `e_μ`. -/
  12def basisVec (μ : Fin 4) : Fin 4 → ℝ := fun ν => if ν = μ then 1 else 0
  13
  14@[simp] lemma basisVec_self (μ : Fin 4) : basisVec μ μ = 1 := by simp [basisVec]
  15
  16@[simp] lemma basisVec_ne {μ ν : Fin 4} (h : ν ≠ μ) : basisVec μ ν = 0 := by
  17  simp [basisVec, h]
  18
  19/-- Coordinate ray `x + t e_μ`. -/
  20def coordRay (x : Fin 4 → ℝ) (μ : Fin 4) (t : ℝ) : Fin 4 → ℝ :=
  21  fun ν => x ν + t * basisVec μ ν
  22
  23@[simp] lemma coordRay_apply (x : Fin 4 → ℝ) (μ : Fin 4) (t : ℝ) (ν : Fin 4) :
  24    coordRay x μ t ν = x ν + t * basisVec μ ν := rfl
  25
  26@[simp] lemma coordRay_zero (x : Fin 4 → ℝ) (μ : Fin 4) : coordRay x μ 0 = x := by
  27  funext ν; simp [coordRay]
  28
  29@[simp] lemma coordRay_coordRay (x : Fin 4 → ℝ) (μ : Fin 4) (s t : ℝ) :
  30    coordRay (coordRay x μ s) μ t = coordRay x μ (s + t) := by
  31  funext ν; simp [coordRay]; ring
  32
  33/-- Directional derivative `∂_μ f(x)` via real derivative along the coordinate ray. -/
  34noncomputable def partialDeriv_v2 (f : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
  35    (x : Fin 4 → ℝ) : ℝ :=
  36  deriv (fun t => f (coordRay x μ t)) 0
  37
  38/-- The derivative of a constant function is zero. -/
  39lemma partialDeriv_v2_const {f : (Fin 4 → ℝ) → ℝ} {c : ℝ} (h : ∀ y, f y = c) (μ : Fin 4) (x : Fin 4 → ℝ) :
  40    partialDeriv_v2 f μ x = 0 := by
  41  unfold partialDeriv_v2
  42  have h_const : (fun t => f (coordRay x μ t)) = (fun _ => c) := by
  43    funext t
  44    rw [h]