efe_with_source

formal source

  58/-! ## The Einstein Field Equation with Source -/
  59
  60/-- The sourced EFE: G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}. -/
  61def efe_with_source (met : MetricTensor) (ginv : InverseMetric)
  62    (gamma : Idx → Idx → Idx → ℝ)
  63    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  64    (Lambda kappa : ℝ) (T : StressEnergy) : Prop :=
  65  ∀ mu nu : Idx,
  66    einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu =
  67    kappa * T.T mu nu
  68
  69/-- Vacuum EFE is a special case with T = 0. -/
  70theorem vacuum_is_special_case (met : MetricTensor) (ginv : InverseMetric)
  71    (gamma : Idx → Idx → Idx → ℝ)
  72    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  73    (Lambda : ℝ) :
  74    efe_with_source met ginv gamma dgamma Lambda 0 vacuum_stress_energy →
  75    vacuum_efe_coord met ginv gamma dgamma Lambda := by
  76  intro h mu nu
  77  have := h mu nu
  78  simp [vacuum_stress_energy, efe_with_source] at this
  79  exact this
  80
  81/-! ## Conservation from Bianchi + EFE -/
  82
  83/-- The contracted Bianchi identity: nabla^mu G_{mu nu} = 0.
  84    This is a GEOMETRIC identity -- it follows from the symmetries
  85    of the Riemann tensor, independent of any field equation.
  86
  87    In coordinates: sum_mu nabla^mu G_{mu nu} = 0 for each nu.
  88
  89    We state this as a property of the Einstein tensor. -/
  90def contracted_bianchi (ginv : InverseMetric)
  91    (gamma : Idx → Idx → Idx → ℝ)