Documentation

Lean 4 Proof

theorem trace_negative {df_rho_drho df_T_dT : ℝ}
    (h1 : df_rho_drho < 0) (h2 : df_T_dT < 0) :
    jacobianTrace df_rho_drho df_T_dT < 0 := by
  simp only [jacobianTrace]; linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:49

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file