FundamentalTheoremExistence

formal source

 176
 177/-- The Fundamental Theorem of Pseudo-Riemannian Geometry (existence part):
 178    The Christoffel connection is torsion-free and metric-compatible. -/
 179structure FundamentalTheoremExistence (g : MetricTensor) : Prop where
 180  torsion_free : IsTorsionFree (christoffel g)
 181  metric_compatible : ∀ x, KoszulIdentity g x →
 182    ∀ ρ μ ν, cov_deriv_metric (christoffel g) g x ρ μ ν = 0
 183
 184/-- The Fundamental Theorem of Pseudo-Riemannian Geometry (uniqueness part):
 185    Any torsion-free, metric-compatible connection has the same lowered coefficients
 186    as the Christoffel connection. -/
 187structure FundamentalTheoremUniqueness (g : MetricTensor) : Prop where
 188  unique : ∀ (Γ : ConnectionCoeffs) (x : Fin 4 → ℝ),
 189    IsTorsionFree Γ →
 190    LoweredConnectionIdentity Γ g x →
 191    ∀ ρ μ ν, lowered_connection Γ g x ρ μ ν =
 192      (1/2 : ℝ) * (
 193        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x +
 194        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else μ)) ν x -
 195        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x)
 196
 197/-- The Fundamental Theorem holds for all metrics. -/
 198theorem fundamental_theorem_existence (g : MetricTensor) : FundamentalTheoremExistence g where
 199  torsion_free := levi_civita_torsion_free g
 200  metric_compatible := fun x h_k => metric_compatible_of_koszul g x h_k
 201
 202theorem fundamental_theorem_uniqueness (g : MetricTensor) : FundamentalTheoremUniqueness g where
 203  unique := fun Γ x h_tf h_id => connection_uniqueness_lowered Γ g x h_tf h_id
 204
 205/-- Combined certificate for the Fundamental Theorem of Pseudo-Riemannian Geometry. -/
 206structure LeviCivitaCertificate (g : MetricTensor) : Prop where
 207  existence : FundamentalTheoremExistence g
 208  uniqueness : FundamentalTheoremUniqueness g
 209