Documentation

Lean 4 Proof

theorem marginalK_strictAntiOn {ρ : ℝ} (hρ : ρ < 1) :
    StrictAntiOn (fun J => marginalK J ρ) (Set.Ioi 0) :=
  fun _ hJ₁ _ _ hJ₁₂ => pigouvian_subsidy_decreasing (Set.mem_Ioi.mp hJ₁) hρ hJ₁₂

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:40

Module Section

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

In the same file