Documentation

Linglib.Studies.Luce1959

Luce (1959), Chapter 3: Applications to Utility Theory [Luc59] #

Choices among gambles: aρb is "outcome a if chance event ρ occurs, else b" (p. 78), and S(A,E) = (A × E × A) ∪ A collects gambles and pure alternatives. A decomposable preference structure ⟨A, E, P, Q⟩ (Definition 5) couples a choice function P over S(A,E) with an event choice function Q via Axiom 2: P(aρb, aσb) = P(a,b)·Q(ρ,σ) + P(b,a)·Q(σ,ρ).

Main results #

Formalization notes #

Luce's P and Q are families of probability measures on subsets of size ≤ 3 (Definition 5); here both are total ChoiceFns, which is where the diagonal bites: binary x x = 1, so Axiom 2 needs its a ≠ b guard (axiom2_unguarded_false) and Axiom 3 its two x-guards (complementation_unguarded_false) — for Luce those instances are degenerate singleton choices. Ratio scales enter as ChoiceFn.BinaryRatioScaleOn, local to the gamble set under discussion, because Chapter 3 mixes imperfect discrimination among gambles with perfect discrimination among pure alternatives (P(a,b) = 1), which a globally positive scale cannot represent.

Axiom 1 lives in the structure (axiom1P/axiom1Q, in ChoiceFn.HasChoiceAxiom's two-clause form) exactly as Definition 5 demands; only the §3.C additional axioms and Theorem 10's nondegeneracy enter as per-theorem hypotheses, as in the book. The three-class theorems are stated representative-wise — among any four events two are equi-likely (atMostThreeClasses); three pairwise non-equivalent events to one of which every event is equivalent (theorem12) — avoiding quotient machinery; a Setoid-packaged corollary is natural future work. The three-class regime forces perfect discrimination Q ∈ {0, 1} between extreme classes, which is exactly what HasChoiceAxiom's deletion clause (and no globally positive ratio scale) tolerates.

structure Luce1959.Gamble (A : Type u_3) (E : Type u_4) :
Type (max u_3 u_4)

A gamble aρb (p. 78): outcome win if the chance event event occurs, else lose.

  • win : A

    Outcome if the event occurs.

  • event : E

    The conditioning chance event.

  • lose : A

    Outcome if the event does not occur.

Instances For
    @[implicit_reducible]
    instance Luce1959.instDecidableEqGamble {A✝ : Type u_3} {E✝ : Type u_4} [DecidableEq A✝] [DecidableEq E✝] :
    DecidableEq (Gamble A✝ E✝)
    Equations
    def Luce1959.instDecidableEqGamble.decEq {A✝ : Type u_3} {E✝ : Type u_4} [DecidableEq A✝] [DecidableEq E✝] (x✝ x✝¹ : Gamble A✝ E✝) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]
      abbrev Luce1959.Alternative (A : Type u_3) (E : Type u_4) :
      Type (max (max u_4 u_3) u_3)

      Luce's total alternative set S(A,E) = (A × E × A) ∪ A (p. 78): gambles together with the pure alternatives.

      Equations
      Instances For
        structure Luce1959.DecomposablePreference (A : Type u_3) (E : Type u_4) [DecidableEq A] [DecidableEq E] :
        Type (max u_3 u_4)

        A decomposable preference structure ⟨A, E, P, Q⟩ (Definition 5, p. 78): choice over gambles and pure alternatives (P), choice over events by subjective likelihood (Q), coupled by Axiom 2: P(aρb, aσb) = P(a,b)·Q(ρ,σ) + P(b,a)·Q(σ,ρ).

        Deviations from Luce: P and Q are total ChoiceFns rather than families on ≤3-element subsets (Axiom 1 enters as the axiom1P/axiom1Q fields, in ChoiceFn.HasChoiceAxiom's two-clause form), and Axiom 2 carries an a ≠ b guard — at a = b it is unsatisfiable for a total P (axiom2_unguarded_false), and Luce's own uses all have P(a,b) ∉ {0, 1} or P(a,b) = 1 with a, b a genuine pair.

        • Choice over S(A,E).

        • Choice over events by subjective likelihood.

        • axiom2 (a b : A) : a b∀ (ρ σ : E), self.P.binary (Sum.inl { win := a, event := ρ, lose := b }) (Sum.inl { win := a, event := σ, lose := b }) = self.P.binary (Sum.inr a) (Sum.inr b) * self.Q.binary ρ σ + self.P.binary (Sum.inr b) (Sum.inr a) * self.Q.binary σ ρ

          Axiom 2 (p. 78), in Luce's full mixture form.

        • axiom1P : self.P.HasChoiceAxiom

          P satisfies Luce's Axiom 1, per Definition 5.

        • axiom1Q : self.Q.HasChoiceAxiom

          Q satisfies Luce's Axiom 1, per Definition 5.

        Instances For
          theorem Luce1959.axiom2_unguarded_false {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [Nontrivial E] [Inhabited A] (P : Core.ChoiceFn (Alternative A E)) (Q : Core.ChoiceFn E) (h : ∀ (a b : A) (ρ σ : E), P.binary (Sum.inl { win := a, event := ρ, lose := b }) (Sum.inl { win := a, event := σ, lose := b }) = P.binary (Sum.inr a) (Sum.inr b) * Q.binary ρ σ + P.binary (Sum.inr b) (Sum.inr a) * Q.binary σ ρ) :
          False

          Without its a ≠ b guard, Axiom 2 is unsatisfiable for a total choice function: at a = b it forces P(aρa, aσa) = Q(ρ,σ) + Q(σ,ρ) = 1 in both argument orders, contradicting binary complementarity. In Luce's system P(a, a) is the degenerate singleton choice.

          def Luce1959.DecomposablePreference.alt {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (a b : A) :

          Luce's P(a, b) for pure alternatives.

          Equations
          Instances For
            def Luce1959.DecomposablePreference.gam {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (g h : Gamble A E) :

            Luce's P(g, h) for gambles.

            Equations
            Instances For
              theorem Luce1959.DecomposablePreference.gam_of_alt_eq_one {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {a b : A} (hab : a b) (h1 : dp.alt a b = 1) (ρ σ : E) :
              dp.gam { win := a, event := ρ, lose := b } { win := a, event := σ, lose := b } = dp.Q.binary ρ σ

              The reduced decomposition under perfect discrimination, as used inside the proofs of Theorems 13–14 (p. 87): if P(a,b) = 1 then P(aρb, aσb) = Q(ρ, σ).

              Definition 6: the subjective likelihood order #

              def Luce1959.DecomposablePreference.EventPref {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (ρ σ : E) :

              Definition 6 (p. 79): ρ ≿ σ iff Q(ρ, σ) ≥ ½ρ is deemed at least as likely as σ.

              Equations
              Instances For
                def Luce1959.DecomposablePreference.EventIndiff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (ρ σ : E) :

                Subjective equi-likelihood ρ ∼ σ: the symmetric part of Definition 6's . On distinct events this is Q(ρ, σ) = ½ (eventIndiff_iff_eq_half); on the diagonal it holds since Q(ρ, ρ) = 1.

                Equations
                Instances For
                  theorem Luce1959.DecomposablePreference.eventIndiff_refl {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) (ρ : E) :
                  dp.EventIndiff ρ ρ
                  theorem Luce1959.DecomposablePreference.EventIndiff.symm {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (h : dp.EventIndiff ρ σ) :
                  dp.EventIndiff σ ρ
                  theorem Luce1959.DecomposablePreference.eventIndiff_iff_eq_half {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (hne : ρ σ) :
                  dp.EventIndiff ρ σ dp.Q.binary ρ σ = 1 / 2
                  theorem Luce1959.DecomposablePreference.ne_of_not_eventIndiff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (h : ¬dp.EventIndiff ρ σ) :
                  ρ σ
                  theorem Luce1959.DecomposablePreference.gt_half_or_of_not_eventIndiff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {ρ σ : E} (h : ¬dp.EventIndiff ρ σ) :
                  1 / 2 < dp.Q.binary ρ σ 1 / 2 < dp.Q.binary σ ρ

                  Totality of in strict form: a non-equi-likely pair is strictly ordered one way or the other.

                  def Luce1959.DecomposablePreference.Nondegenerate {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) :

                  The nondegeneracy hypothesis of Theorem 10 (p. 80): some genuine pair of alternatives is discriminated imperfectly and asymmetrically, P(a, b) ∉ {0, ½, 1}.

                  Equations
                  • dp.Nondegenerate = ∃ (a : A) (b : A), a b dp.alt a b 0 dp.alt a b 1 / 2 dp.alt a b 1
                  Instances For

                    The three-class theorems (§3.B.2) #

                    theorem Luce1959.DecomposablePreference.lemma5 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {a b : A} (hab : a b) (h0 : dp.alt a b 0) (hhalf : dp.alt a b 1 / 2) (h1 : dp.alt a b 1) {ρ σ τ : E} (hρσ : ρ σ) (hστ : σ τ) (hρτ : ρ τ) :
                    dp.alt a b * dp.alt b a * (2 * (dp.Q.binary ρ σ + dp.Q.binary σ τ + dp.Q.binary τ ρ) - 3) + (dp.alt a b - dp.alt b a) ^ 2 * (dp.Q.binary ρ σ * dp.Q.binary σ τ * dp.Q.binary τ ρ - dp.Q.binary ρ τ * dp.Q.binary τ σ * dp.Q.binary σ ρ) = 0

                    Lemma 5 (p. 80), in denominator-cleared form: Luce's identity (K+1){2[Q(ρ,σ)+Q(σ,τ)+Q(τ,ρ)] − 3} + K²[Q(ρ,σ)Q(σ,τ)Q(τ,ρ) − Q(ρ,τ)Q(τ,σ)Q(σ,ρ)] = 0, K = P(a,b)/P(b,a) − 1, multiplied through by P(b,a)². From Axiom 2 and Theorem 2 for the gamble triple {aρb, aσb, aτb}, whose pairwise discrimination is imperfect whenever P(a,b) ∉ {0, 1}.

                    theorem Luce1959.DecomposablePreference.eventPref_trans {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ σ τ : E} (h1 : dp.EventPref ρ σ) (h2 : dp.EventPref σ τ) :
                    dp.EventPref ρ τ

                    Lemma 6 (p. 80): is transitive (with gt_half_or_of_not_eventIndiff totality, a weak ordering of E).

                    theorem Luce1959.DecomposablePreference.eventIndiff_trans {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ σ τ : E} (h1 : dp.EventIndiff ρ σ) (h2 : dp.EventIndiff σ τ) :
                    dp.EventIndiff ρ τ

                    is transitive: with eventIndiff_refl and EventIndiff.symm, an equivalence relation (the content of Theorem 10's first clause).

                    theorem Luce1959.DecomposablePreference.lemma7 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ σ τ : E} (hρσ : ρ σ) (hστ : σ τ) (hρτ : ρ τ) (himp : dp.Q.ImperfectOn {ρ, σ, τ}) :
                    dp.EventIndiff ρ σ dp.EventIndiff σ τ dp.EventIndiff ρ τ

                    Lemma 7 (p. 81): three distinct events, pairwise imperfectly discriminated, cannot lie in three distinct -classes.

                    theorem Luce1959.DecomposablePreference.atMostThreeClasses {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) (ρ σ τ ω : E) :
                    dp.EventIndiff ρ σ dp.EventIndiff ρ τ dp.EventIndiff ρ ω dp.EventIndiff σ τ dp.EventIndiff σ ω dp.EventIndiff τ ω

                    Lemma 8 (p. 81) / the partition clause of Theorem 10 (p. 80): in a nondegenerate decomposable preference structure, partitions the events into at most three classes — among any four events, two are subjectively equi-likely.

                    theorem Luce1959.DecomposablePreference.theorem11 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} (hnd : dp.Nondegenerate) {ρ ρ' σ σ' : E} (h1 : dp.EventIndiff ρ ρ') (h2 : dp.EventIndiff σ σ') (hρσ : ρ σ) (hρ'σ' : ρ' σ') :
                    dp.Q.binary ρ σ = dp.Q.binary ρ' σ'

                    Theorem 11 (p. 82): Q is constant across -classes — if ρ ∼ ρ' and σ ∼ σ' then Q(ρ, σ) = Q(ρ', σ'). Both comparisons must be genuine pairs: at ρ' = σ' the total-ChoiceFn diagonal Q(ρ', ρ') = 1 breaks the unguarded claim, which Luce's P(x, x) = ½ convention (p. 5) hides.

                    theorem Luce1959.DecomposablePreference.theorem13 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {a b c d : A} {ρ σ : E} (hab : a b) (hcd : c d) (ha1 : dp.alt a b = 1) (hc1 : dp.alt c d = 1) (himp : dp.P.ImperfectOn {Sum.inl { win := a, event := ρ, lose := b }, Sum.inl { win := a, event := σ, lose := b }, Sum.inl { win := c, event := ρ, lose := d }, Sum.inl { win := c, event := σ, lose := d }}) :
                    dp.gam { win := a, event := ρ, lose := b } { win := c, event := ρ, lose := d } = dp.gam { win := a, event := σ, lose := b } { win := c, event := σ, lose := d }

                    Theorem 13 (p. 86): if P(a,b) = P(c,d) = 1 and "all pairwise discriminations in the set T = {aρb, aσb, cρd, cσd} are imperfect", then P(aρb, cρd) = P(aσb, cσd) — the step-function prediction of §3.D. The local ratio scale of Luce's proof is supplied by Theorem 3 (ChoiceFn.HasChoiceAxiom.binaryRatioScaleOn).

                    def Luce1959.DecomposablePreference.Complementation {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) :

                    Axiom 3 (p. 83): "P(aρb, x) = P(bρ̄a, x), where ρ̄ denotes the complement of ρ" — aρb and bρ̄a are the same prospect relabeled. The two guards exclude x ∈ {aρb, bρ̄a}: for Luce those instances are degenerate singleton choices, and over a total ChoiceFn the unguarded axiom is unsatisfiable (complementation_unguarded_false).

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Luce1959.DecomposablePreference.complementation_unguarded_false {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] [Nontrivial A] (dp : DecomposablePreference A E) (h : ∀ (a b : A) (ρ : E) (x : Alternative A E), dp.P.binary (Sum.inl { win := a, event := ρ, lose := b }) x = dp.P.binary (Sum.inl { win := b, event := ρ, lose := a }) x) :
                      False

                      Without its guards, Axiom 3 is unsatisfiable for a total choice function: x := bρ̄a forces P(aρb, bρ̄a) = 1, and symmetrically P(bρ̄a, aρb) = 1, contradicting binary complementarity.

                      def Luce1959.DecomposablePreference.NontrivialPreference {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] (dp : DecomposablePreference A E) :

                      Axiom 4 (p. 83): some pair of alternatives and some pair of events are discriminated away from ½. Distinctness is explicit: Luce's P(a*, b*) presupposes a genuine pair (P(a, a) = 1 ≠ ½ would satisfy the inequality degenerately and break the determinant step of Lemma 9).

                      Equations
                      • dp.NontrivialPreference = ((∃ (a : A) (b : A), a b dp.alt a b 1 / 2) ∃ (ρ : E) (σ : E), ρ σ dp.Q.binary ρ σ 1 / 2)
                      Instances For
                        theorem Luce1959.DecomposablePreference.q_compl_compl {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ρ σ : E) :
                        dp.Q.binary ρ σ = dp.Q.binary σ ρ

                        Lemma 9 (p. 84): under Axioms 3–4, Q(ρ, σ) = Q(σ̄, ρ̄).

                        theorem Luce1959.DecomposablePreference.v_mul_v_compl_const {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] {v : E} (hv : dp.Q.BinaryRatioScaleOn Set.univ v) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ρ σ : E) :
                        v ρ * v ρ = v σ * v σ

                        Under a global binary ratio scale for Q, Lemma 9 pins v(ρ)·v(ρ̄) to a constant — the source of the φ(ρ)φ(ρ̄) = constant clause of the §3.D.3 decomposition (p. 89).

                        def Luce1959.DecomposablePreference.Neutral {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) :

                        An event indifferent to its own complement: membership in Luce's class C(½) (Lemma 11, p. 85).

                        Equations
                        Instances For
                          def Luce1959.DecomposablePreference.Favorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) :

                          An event deemed more likely than its complement: Luce's class C(1).

                          Equations
                          Instances For
                            def Luce1959.DecomposablePreference.Unfavorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) :

                            An event deemed less likely than its complement: Luce's class C(0).

                            Equations
                            Instances For
                              theorem Luce1959.DecomposablePreference.unfavorable_or_neutral_or_favorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) (ρ : E) :
                              dp.Unfavorable ρ dp.Neutral ρ dp.Favorable ρ

                              Every event is unfavorable, neutral, or favorable.

                              theorem Luce1959.DecomposablePreference.neutral_compl_iff {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (ρ : E) :
                              dp.Neutral ρ dp.Neutral ρ

                              An event is neutral iff its complement is.

                              theorem Luce1959.DecomposablePreference.favorable_iff_unfavorable_compl {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (ρ : E) :
                              dp.Favorable ρ dp.Unfavorable ρ

                              An event is favorable iff its complement is unfavorable.

                              theorem Luce1959.DecomposablePreference.neutral_indifferent {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) {ρ σ : E} ( : dp.Neutral ρ) ( : dp.Neutral σ) (hρσ : ρ σ) :
                              dp.Q.binary ρ σ = 1 / 2

                              Two distinct neutral events are indifferent — the first clause of Lemma 10 (p. 84), "if ρ ∼ ρ̄ and σ ∼ σ̄, then ρ ∼ σ", via Theorem 11 and Lemma 9. Distinctness is required: Q(ρ, ρ) = 1.

                              theorem Luce1959.DecomposablePreference.favorable_gt_unfavorable {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] {v : E} (hv : dp.Q.BinaryRatioScaleOn Set.univ v) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) {ρ σ : E} ( : dp.Favorable ρ) ( : dp.Unfavorable σ) :
                              1 / 2 < dp.Q.binary ρ σ

                              Favorable events are preferred to unfavorable ones: the between-class ordering C(1) > C(0) of the three-class picture (§3.C.2, p. 85), under a global ratio scale for Q.

                              theorem Luce1959.DecomposablePreference.theorem14 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (ax3 : dp.Complementation) {a b c d : A} {ρ σ : E} {v : Alternative A E} (hab : a b) (hcd : c d) (hρσ : ρ σ) (hacbd : ¬(a = c b = d)) (ha1 : dp.alt a b = 1) (hd1 : dp.alt d c = 1) (hv : dp.P.BinaryRatioScaleOn {Sum.inl { win := a, event := ρ, lose := b }, Sum.inl { win := a, event := σ, lose := b }, Sum.inl { win := c, event := ρ, lose := d }, Sum.inl { win := c, event := σ, lose := d }, Sum.inl { win := d, event := ρ, lose := c }, Sum.inl { win := d, event := σ, lose := c }} v) :
                              v (Sum.inl { win := a, event := ρ, lose := b }) * v (Sum.inl { win := d, event := ρ, lose := c }) = v (Sum.inl { win := a, event := σ, lose := b }) * v (Sum.inl { win := d, event := σ, lose := c })

                              Theorem 14 (p. 89): with Axiom 3, P(a,b) = P(d,c) = 1, and a local ratio scale over the six gambles involved, the scale satisfies v(aρb)·v(dρ̄c) = v(aσb)·v(dσ̄c). Together with Theorem 13 this is what "suggests that v may be of the form v(aρb) = w(a,b)·φ(ρ)" (§3.D.3).

                              def Luce1959.DecomposablePreference.HasNeutralEvent {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] [BooleanAlgebra E] (dp : DecomposablePreference A E) :

                              Axiom 5 (p. 84): some event is subjectively as likely as its complement.

                              Equations
                              Instances For
                                theorem Luce1959.DecomposablePreference.neutral_of_indiff_neutral {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) {ρ σ : E} ( : dp.Neutral ρ) (h : dp.EventIndiff σ ρ) :
                                dp.Neutral σ

                                The second clause of Lemma 10 (p. 84): anything equi-likely with a neutral event is itself neutral — C(½) is exactly the neutral class.

                                theorem Luce1959.DecomposablePreference.atLeastThreeClasses {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ax5 : dp.HasNeutralEvent) :
                                ∃ (ε : E) (ρ : E), ¬dp.EventIndiff ε ρ ¬dp.EventIndiff ε ρ ¬dp.EventIndiff ρ ρ

                                Lemma 11 (p. 85): with Axioms 3–5 and nondegeneracy there are at least three classes — a neutral event, a non-neutral event, and its complement are pairwise non-equivalent.

                                theorem Luce1959.DecomposablePreference.theorem12 {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} [BooleanAlgebra E] [Nontrivial E] (hnd : dp.Nondegenerate) (ax3 : dp.Complementation) (ax4 : dp.NontrivialPreference) (ax5 : dp.HasNeutralEvent) :
                                ∃ (ρ₁ : E) (ρ₂ : E) (ρ₃ : E), (¬dp.EventIndiff ρ₁ ρ₂ ¬dp.EventIndiff ρ₁ ρ₃ ¬dp.EventIndiff ρ₂ ρ₃) ∀ (σ : E), dp.EventIndiff σ ρ₁ dp.EventIndiff σ ρ₂ dp.EventIndiff σ ρ₃

                                Theorem 12 (p. 84): given Axioms 3–5 and a nondegenerately discriminated pair of alternatives, partitions the events into exactly three classes: three pairwise non-equivalent events to one of which every event is equivalent.

                                theorem Luce1959.DecomposablePreference.gam_of_factored {A : Type u_1} {E : Type u_2} [DecidableEq A] [DecidableEq E] {dp : DecomposablePreference A E} {S : Set (Gamble A E)} {v : Alternative A E} {w : AA} {φ : E} (hv : dp.P.BinaryRatioScaleOn (Sum.inl '' S) v) ( : ∀ (τ : E), 0 < φ τ) (hfac : ∀ (x y : A) (τ : E), { win := x, event := τ, lose := y } Sv (Sum.inl { win := x, event := τ, lose := y }) = w x y * φ τ) {a b c d : A} {ρ : E} (h₁ : { win := a, event := ρ, lose := b } S) (h₂ : { win := c, event := ρ, lose := d } S) (hacbd : ¬(a = c b = d)) :
                                dp.gam { win := a, event := ρ, lose := b } { win := c, event := ρ, lose := d } = w a b / (w a b + w c d)

                                The observable content of the §3.D.3 suggested factoring v(aρb) = w(a,b)·φ(ρ) (pp. 89–90): between gambles on the same event the event weight cancels, so binary choice follows the Luce rule on the outcome weights alone — "the step function described in theorem 13 can have only one step intermediate between 0 and 1" (p. 90). Luce offers the factoring as a hypothesis consistent with Theorems 13–14, not a theorem; accordingly it enters here as a hypothesis.