Documentation

Lean 4 Proof

theorem pigouvian_subsidy_decomposition {J ρ c : ℝ} :
    J * valueFunctionDeriv J ρ c =
    J * marginalK J ρ * perCapitaBenefit J ρ c +
    J * curvatureKReal J ρ * ((1 / ρ - 1) * J ^ (1 / ρ - 2) * c) := by
  simp only [valueFunctionDeriv]; ring

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:339

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file