Documentation

Lean 4 Proof

theorem damping_cancellation_J_independent
    {sigma_prev delta beta_n : ℝ}
    (_hs : 0 < sigma_prev) (_hb : 0 < beta_n) :
    -- The welfare contribution depends on sigma_{n-1}, delta, beta_n
    -- but NOT on J_n or sigma_n (the own-level parameters)
    welfareContribution sigma_prev delta beta_n =
    sigma_prev * delta ^ 2 / beta_n := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:305

Module Section

## Welfare with Endogenous J (merged from EntryExitWelfare.lean)

In the same file