Documentation

Lean 4 Proof

def socialWelfare (J ρ c κ : ℝ) : ℝ :=
  J * (valueFunction J ρ c - κ)

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:315

Module Section

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

In the same file