IsMetricCompatible

formal source

  53  Finset.univ.sum (fun σ => Γ x σ ρ ν * g_comp x μ σ)
  54
  55/-- A connection is metric-compatible iff ∇_ρ g_{μν} = 0 for all ρ, μ, ν. -/
  56def IsMetricCompatible (Γ : ConnectionCoeffs) (g : MetricTensor) : Prop :=
  57  ∀ x ρ μ ν, cov_deriv_metric Γ g x ρ μ ν = 0
  58
  59/-! ## §2 Christoffel Symbols Are Torsion-Free -/
  60
  61/-- `Curvature.christoffel` is torsion-free.
  62    This is already proved as `christoffel_symmetric`. -/
  63theorem levi_civita_torsion_free (g : MetricTensor) :
  64    IsTorsionFree (christoffel g) :=
  65  fun x ρ μ ν => christoffel_symmetric g x ρ μ ν
  66
  67/-! ## §3 Metric Compatibility of the Christoffel Connection
  68
  69The metric compatibility ∇_ρ g_{μν} = 0 for the Levi-Civita connection
  70follows from the algebraic structure of the Christoffel symbols.
  71
  72We prove it by showing that ∂_ρ g_{μν} = Γ^σ_{ρμ} g_{σν} + Γ^σ_{ρν} g_{μσ}
  73when Γ is the Christoffel connection.
  74
  75This is equivalent to the Koszul formula, which uniquely determines
  76the connection from the metric. -/
  77
  78/-- The Koszul identity: for the Christoffel connection,
  79    g_{σν} Γ^σ_{ρμ} + g_{μσ} Γ^σ_{ρν} = ∂_ρ g_{μν}.
  80
  81    This is the fundamental identity that encodes metric compatibility.
  82
  83    Proof: Expand Γ using Christoffel formula and contract with metric.
  84    The three permutations of ∂g cancel to give exactly ∂_ρ g_{μν}. -/
  85def KoszulIdentity (g : MetricTensor) (x : Fin 4 → ℝ) : Prop :=
  86  ∀ ρ μ ν,