Documentation

Lean 4 Proof

def persistencePremium (J_high J_crit ρ c d_sq : ℝ) : ℝ :=
  criticalFrictionReal J_high ρ c d_sq - criticalFrictionReal J_crit ρ c d_sq

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:130

Module Section

Paper 3c, Section 3: First-Order Regime Shift

In the same file