MetricSmooth

formal source

 492  ∀ μ ν, secondDeriv f μ ν x = secondDeriv f ν μ x
 493
 494/-- A metric whose components have symmetric mixed partials everywhere. -/
 495def MetricSmooth (g : MetricTensor) (x : Fin 4 → ℝ) : Prop :=
 496  ∀ a b, MixedPartialsSymmetric
 497    (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then a else b)) x
 498
 499/-! ## Trace Vanishing from Mixed Partial Symmetry
 500
 501The derivative part of Σ_ρ R^ρ_ρμν is:
 502  Σ_ρ (∂_μ Γ^ρ_νρ - ∂_ν Γ^ρ_μρ)
 503
 504Using Γ^ρ_νρ = (1/2) g^{ρλ} (∂_ν g_{ρλ} + ∂_ρ g_{νλ} - ∂_λ g_{νρ})
 505and the trace identity Σ_ρ Γ^ρ_νρ = ∂_ν(ln√|det g|),
 506the derivative terms become ∂_μ∂_ν(ln√|det g|) - ∂_ν∂_μ(ln√|det g|) = 0
 507by symmetry of mixed partials. -/
 508
 509/-- The Riemann trace vanishes for metrics with symmetric mixed partials.
 510    Σ_ρ R^ρ_ρμν = 0 when ∂_μ∂_ν = ∂_ν∂_μ on metric components.
 511
 512    Proof structure:
 513    1. Quadratic Christoffel terms vanish: already proved as
 514       `christoffel_quadratic_trace_vanishes`
 515    2. Derivative terms: Σ_ρ (∂_μ Γ^ρ_νρ - ∂_ν Γ^ρ_μρ)
 516       The Christoffel contraction Σ_ρ Γ^ρ_αρ is a function of x only,
 517       so its mixed partials commute by the Schwarz hypothesis. -/
 518theorem riemann_trace_vanishes_of_smooth (g : MetricTensor) (x : Fin 4 → ℝ)
 519    (μ ν : Fin 4)
 520    (_h_smooth : MetricSmooth g x)
 521    (h_christoffel_trace_partials :
 522      Finset.univ.sum (fun ρ : Fin 4 => partialDeriv_v2 (fun y => christoffel g y ρ ν ρ) μ x) =
 523      Finset.univ.sum (fun ρ : Fin 4 => partialDeriv_v2 (fun y => christoffel g y ρ μ ρ) ν x)) :
 524    riemann_trace_vanishes_hypothesis g x μ ν := by
 525  unfold riemann_trace_vanishes_hypothesis riemann_trace riemann_tensor