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

IsMaximumMass

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)

  70def IsMaximumMass (sol : TOVSolution) (P_c_max M_max : ℝ) : Prop :=

proof body

Definition body.

  71  sol.M_of_Pc P_c_max = M_max ∧
  72  -- At P_c_max, the mass has a local maximum:
  73  ∀ P_c : ℝ, P_c ≠ P_c_max → sol.M_of_Pc P_c ≤ M_max
  74
  75/-- **STABILITY CRITERION**: The TOV stability condition for a NS.
  76    Configuration is stable iff dM/dρ_c > 0 (mass increases with central density).
  77    Above M_max, this condition fails. -/

depends on (11)

Lean names referenced from this declaration's body.