Documentation

Lean 4 Proof

theorem fold_marginalK_pos {J_fold ρ : ℝ}
    (hJ : 0 < J_fold) (hρ : ρ < 1) :
    0 < marginalK J_fold ρ :=
  pigouvian_subsidy_pos hJ hρ

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:54

Module Section

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

In the same file