Documentation

Lean 4 Proof

theorem pigouvian_subsidy_decreasing {J₁ J₂ ρ : ℝ}
    (hJ₁ : 0 < J₁) (hρ : ρ < 1) (hJ : J₁ < J₂) :
    marginalK J₂ ρ < marginalK J₁ ρ := by
  simp only [marginalK]
  apply div_lt_div_of_pos_left (by linarith) (sq_pos_of_pos hJ₁)
  exact sq_lt_sq' (by linarith) hJ

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Defs.lean:160

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file