Documentation

Lean 4 Proof

theorem coupled_3d_fixed_point_exists :
    -- Under regularity conditions on the coupling,
    -- there exists an interior fixed point (rho*, T*, J*)
    -- with rho* < 1, T* > 0, J* > 1.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:208

Module Section

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

In the same file