perfect_fluid

formal source

  47  symmetric := fun _ _ => rfl
  48
  49/-- A perfect fluid stress-energy: T_{mu nu} = (rho + p) u_mu u_nu + p g_{mu nu}. -/
  50noncomputable def perfect_fluid (rho p : ℝ) (u : Idx → ℝ)
  51    (met : MetricTensor) : StressEnergy where
  52  T := fun mu nu => (rho + p) * u mu * u nu + p * met.g mu nu
  53  symmetric := by
  54    intro mu nu
  55    simp [met.symmetric mu nu]
  56    ring
  57
  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