Documentation

Lean 4 Proof

theorem sector_relaxation_rate_eq (e : NSectorEconomy N) (n : Fin N) :
    sectorRelaxRate e n =
    e.ℓ n * |logCesEigenvaluePerp (e.J n) (e.ρ n) (e.c n)| *
      max 0 (1 - e.T n / sectorCriticalFriction e n) := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:78

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file