pith. machine review for the scientific record. sign in
structure definition def or abbrev

TOVSystem

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  35structure TOVSystem where
  36  ε : ℝ → ℝ  -- energy density profile ε(r)
  37  P : ℝ → ℝ  -- pressure profile P(r)
  38  M : ℝ → ℝ  -- mass function M(r) = ∫₀ʳ 4πr'²ε(r')dr'
  39
  40/-- GR corrections to Newtonian hydrostatics:
  41    Factor 1: (ε + P) replaces ε — pressure gravitates in GR
  42    Factor 2: (M + 4πr³P) replaces M — pressure contributes to source
  43    Factor 3: (1 - 2M/r)⁻¹ — metric redshift factor -/

depends on (4)

Lean names referenced from this declaration's body.