Documentation

Lean 4 Proof

theorem coupled_3d_instability {a_ρρ a_TT a_JJ : ℝ}
    (htrace : 0 < jacobian3DTrace a_ρρ a_TT a_JJ) :
    0 < a_ρρ + a_TT + a_JJ :=
  instability_from_trace htrace

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:215

Module Section

## Coupled (ρ, T, J) System (merged from CoupledSystem.lean)

In the same file