Documentation

Lean 4 Proof

theorem adjustmentTimescale_connection {eps sigma T Tstar : ℝ} :
    institutionalAdjustmentTime eps sigma (1 - T / Tstar) =
    adjustmentTimescale (eps / sigma) T Tstar := by
  simp only [institutionalAdjustmentTime, adjustmentTimescale]
  rw [div_div]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:108

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file