Documentation

Lean 4 Proof

theorem instability_from_trace {a_ρρ a_TT a_JJ : ℝ}
    (htrace : 0 < jacobian3DTrace a_ρρ a_TT a_JJ) :
    0 < a_ρρ + a_TT + a_JJ := by
  simp only [jacobian3DTrace] at htrace; exact htrace

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:95

Module Section

## Entry-Exit Core Definitions (merged from EntryExitDefs.lean)

In the same file