minkowski_preserves_inner

formal source

 116    The proof uses the fact that η is position-independent and both V, W
 117    have vanishing derivatives (proved by `parallel_transport_flat`).
 118    The derivative of Σ (const * const * const) = 0. -/
 119theorem minkowski_preserves_inner (γ : SpacetimeCurve) :
 120    ParallelTransportPreservesInnerProduct minkowski_tensor γ := by
 121  intro V W h_diffV h_diffW hV hW lam
 122  have hV_const := parallel_transport_flat γ V hV
 123  have hW_const := parallel_transport_flat γ W hW
 124  let t0 : ℝ → ℝ := fun l => V l 0 * W l 0
 125  let t1 : ℝ → ℝ := fun l => V l 1 * W l 1
 126  let t2 : ℝ → ℝ := fun l => V l 2 * W l 2
 127  let t3 : ℝ → ℝ := fun l => V l 3 * W l 3
 128  have ht0_diff : DifferentiableAt ℝ t0 lam := by
 129    unfold t0
 130    exact (h_diffV 0 lam).mul (h_diffW 0 lam)
 131  have ht1_diff : DifferentiableAt ℝ t1 lam := by
 132    unfold t1
 133    exact (h_diffV 1 lam).mul (h_diffW 1 lam)
 134  have ht2_diff : DifferentiableAt ℝ t2 lam := by
 135    unfold t2
 136    exact (h_diffV 2 lam).mul (h_diffW 2 lam)
 137  have ht3_diff : DifferentiableAt ℝ t3 lam := by
 138    unfold t3
 139    exact (h_diffV 3 lam).mul (h_diffW 3 lam)
 140  have ht0_zero : deriv t0 lam = 0 := by
 141    unfold t0
 142    simpa [hV_const lam 0, hW_const lam 0] using
 143      (((h_diffV 0 lam).hasDerivAt).mul ((h_diffW 0 lam).hasDerivAt)).deriv
 144  have ht1_zero : deriv t1 lam = 0 := by
 145    unfold t1
 146    simpa [hV_const lam 1, hW_const lam 1] using
 147      (((h_diffV 1 lam).hasDerivAt).mul ((h_diffW 1 lam).hasDerivAt)).deriv
 148  have ht2_zero : deriv t2 lam = 0 := by
 149    unfold t2