Documentation

Lean 4 Proof

theorem euler_equilibrium_identity (J : ℕ) (q T : ℝ) (hT : 0 < T)
    (p : Fin J → ℝ) (eps : Fin J → ℝ) :
    -- nabla Phi(p*) = T * nabla S_q(p*) + mu * 1
    -- where p* is the q-exponential equilibrium
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:39

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file