85theorem parallel_transport_flat (γ : SpacetimeCurve) 86 (V : ℝ → (Fin 4 → ℝ)) 87 (h_pt : ParallelTransported minkowski_tensor γ V) : 88 ∀ lam μ, deriv (fun l => V l μ) lam = 0 := by
proof body
Term-mode proof.
89 intro lam μ 90 have h := h_pt lam μ 91 simp only [minkowski_christoffel_zero_proper, zero_mul, Finset.sum_const_zero, add_zero] at h 92 exact h 93 94/-- Parallel transport preserves the metric inner product. 95 If V, W are parallel-transported along γ, then g(V,W) is constant. 96 97 g_{μν} V^μ W^ν = const along γ 98 99 This is a consequence of metric compatibility ∇g = 0. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.