pith. machine review for the scientific record. sign in
structure definition def or abbrev

VCGCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 311structure VCGCert where
 312  dsic_zero : ∀ (v₀ b₁ b₀' : ℝ), utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁
 313  dsic_one : ∀ (v₁ b₀ b₁' : ℝ), utility₁ v₁ b₀ b₁' ≤ utility₁ v₁ b₀ v₁
 314  truthful_is_nash :
 315    ∀ (v₀ v₁ : ℝ),
 316      (∀ b₀' : ℝ, utility₀ v₀ b₀' v₁ ≤ utility₀ v₀ v₀ v₁) ∧
 317      (∀ b₁' : ℝ, utility₁ v₁ v₀ b₁' ≤ utility₁ v₁ v₀ v₁)
 318  pivot_identity :
 319    ∀ (v₀ v₁ : ℝ),
 320      (v₀ ≥ v₁ → payment₀ v₀ v₁ = v₁) ∧
 321      (v₀ < v₁ → payment₁ v₀ v₁ = v₀)
 322  sigma_conservation :
 323    ∀ (v₀ v₁ : ℝ),
 324      utility₀ v₀ v₀ v₁ + utility₁ v₁ v₀ v₁ +
 325          (payment₀ v₀ v₁ + payment₁ v₀ v₁) = max v₀ v₁
 326  payment_eq_sigma_cost :
 327    ∀ (v₀ v₁ : ℝ),
 328      (v₀ ≥ v₁ → payment₀ v₀ v₁ = sigma_cost_to_agent_0 v₁) ∧
 329      (v₀ < v₁ → payment₁ v₀ v₁ = sigma_cost_to_agent_1 v₀)
 330  welfare_optimal :
 331    ∀ (v₀ v₁ : ℝ),
 332      (winner v₀ v₁ = 0 ∧ v₀ ≥ v₁) ∨ (winner v₀ v₁ = 1 ∧ v₀ < v₁)
 333
 334/-- The master certificate is inhabited. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.