Reference · Logic

rainbow.math.logic.maximum-expected-utility

Logic src/rainbow/math/logic/maximum_expected_utility.clj11 definitions, 7 theorems

AHoF D17: finite exact-rational maximum expected utility.

ahof-d17/action-space

ahof-d17/action-space :
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

ahof-d17/outcome-space

DefinitionSource, line 71

ahof-d17/outcome-space :
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

ahof-d17/accept

DefinitionSource, line 163

ahof-d17/accept :
  → ℕ

ℕ = data/Nat

ahof-d17/renegotiate

DefinitionSource

ahof-d17/renegotiate :
  → ℕ

ℕ = data/Nat

ahof-d17/decline

DefinitionSource

ahof-d17/decline :
  → ℕ

ℕ = data/Nat

ahof-d17/probability-mass

DefinitionSource, line 84

ahof-d17/probability-mass :
  (x₁ : ℕ)
  → ℚ≥0

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

ahof-d17/utility

DefinitionSource, line 90

ahof-d17/utility :
  (x₁ x₂ : ℕ)
  → ℚ≥0

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

ahof-d17/expected-utility

DefinitionSource, line 113

ahof-d17/expected-utility :
  (x₁ : ℕ)
  → ℚ≥0

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

ahof-d17/finite-expected-utility

DefinitionSource, line 122

ahof-d17/finite-expected-utility :
  (x₁ : ℕ)
  → ℚ≥0

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

ahof-d17/total-mass

DefinitionSource, line 137

ahof-d17/total-mass :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

ahof-d17/selected-action

DefinitionSource, line 145

ahof-d17/selected-action :
  → ℕ

ℕ = data/Nat

ahof-d17/accept-is-action

TheoremWorked exampleNo axiomsSource, line 163

ahof-d17/accept-is-action :
  → audit-ex/accept ∈ ahof-d40/candidates

∈ = finset-data/to-set: membership in a finite set

ahof-d17/probabilities-normalized

TheoremWorked exampleNo axiomsSource, line 201

ahof-d17/probabilities-normalized :
  → ahof-d17/total-mass = 1

1 = nnrat/one= = nnrat/equivalent: equality of rational values

ahof-d17/expected-utility-is-finite-expectation

TheoremWorked exampleNo axiomsSource, line 219

ahof-d17/expected-utility-is-finite-expectation :
  → proposition/conjunction (ahof-d17/expected-utility audit-ex/accept = ahof-d17/finite-expected-utility audit-ex/accept) (conjunction)
  where conjunction := proposition/conjunction (ahof-d17/expected-utility ahof-d17/renegotiate = ahof-d17/finite-expected-utility ahof-d17/renegotiate) (ahof-d17/expected-utility ahof-d17/decline = ahof-d17/finite-expected-utility ahof-d17/decline)

= = nnrat/equivalent: equality of rational values

ahof-d17/selected-is-renegotiate

TheoremWorked exampleNo axiomsSource, line 239

ahof-d17/selected-is-renegotiate :
  → ahof-d17/selected-action = ahof-d17/renegotiate

= = equality/Eq

ahof-d17/selected-is-member

TheoremWorked exampleNo axiomsSource, line 251

ahof-d17/selected-is-member :
  → ahof-d17/selected-action ∈ ahof-d40/candidates

∈ = finset-data/to-set: membership in a finite set

ahof-d17/selected-dominates

TheoremFor all inputsNo axiomsSource, line 266

ahof-d17/selected-dominates :
  (candidate : ℕ)
  (member : candidate ∈ ahof-d40/candidates)
  → ahof-d17/expected-utility candidate ≤ ahof-d17/expected-utility ahof-d17/selected-action

ℕ = data/Nat∈ = finset-data/to-set: membership in a finite set≤ = nnrat/at-most

ahof-d17/maximum-expected-utility

TheoremWorked exampleNo axiomsSource, line 299

ahof-d17/maximum-expected-utility :
  → proposition/conjunction (ahof-d17/total-mass = 1) (conjunction)
  where conjunction := proposition/conjunction (ahof-d17/selected-action = ahof-d17/renegotiate) (proposition/conjunction (ahof-d17/selected-action ∈ ahof-d40/candidates) (∀ (candidate : ℕ), ∀ (member : candidate ∈ ahof-d40/candidates), ahof-d17/expected-utility candidate ≤ ahof-d17/expected-utility ahof-d17/selected-action))

1 = nnrat/one= = equality/Eqℕ = data/Nat∈ = finset-data/to-set: membership in a finite set≤ = nnrat/at-most