Documentation

Lean 4 Proof

theorem pigouvian_subsidy_pos {J ρ : ℝ} (hJ : 0 < J) (hρ : ρ < 1) :
    0 < marginalK J ρ := by
  simp only [marginalK]
  exact div_pos (by linarith) (sq_pos_of_pos hJ)

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Defs.lean:153

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file