Documentation

Mathlib.SetTheory.Surreal.Multiplication

Surreal multiplication #

In this file, we show that multiplication of surreal numbers is well-defined, and thus the surreal numbers form a linear ordered commutative ring.

An inductive argument proves the following three main theorems:

This is Theorem 8 in [Conway2001], or Theorem 3.8 in [SchleicherStoll]. P1 allows us to define multiplication as an operation on numeric pregames, P2 says that this is well-defined as an operation on the quotient by PGame.Equiv, namely the surreal numbers, and P3 is an axiom that needs to be satisfied for the surreals to be a OrderedRing.

We follow the proof in [SchleicherStoll], except that we use the well-foundedness of the hydra relation CutExpand on Multiset PGame instead of the argument based on a depth function in the paper.

In the argument, P3 is stated with four variables x₁, x₂, y₁, y₂ satisfying x₁ < x₂ and y₁ < y₂, and says that x₁ * y₂ + x₂ * x₁ < x₁ * y₁ + x₂ * y₂, which is equivalent to 0 < x₂ - x₁ → 0 < y₂ - y₁ → 0 < (x₂ - x₁) * (y₂ - y₁), i.e. @mul_pos PGame _ (x₂ - x₁) (y₂ - y₁). It has to be stated in this form and not in terms of mul_pos because we need to show P1, P2 and (a specialized form of) P3 simultaneously, and for example P1 x y will be deduced from P3 with variables taking values simpler than x or y (among other induction hypotheses), but if you subtract two pregames simpler than x or y, the result may no longer be simpler.

The specialized version of P3 is called P4, which takes only three arguments x₁, x₂, y and requires that y₂ = y or -y and that y₁ is a left option of y₂. After P1, P2 and P4 are shown, a further inductive argument (this time using the GameAdd relation) proves P3 in full.

Implementation strategy of the inductive argument: we

The whole proof features a clear separation into lemmas of different roles:

References #

The nontrivial part of P1 in [SchleicherStoll] says that the left options of x * y are less than the right options, and this is the general form of these statements.

Equations
Instances For

    The proposition P2, without numericity assumptions.

    Equations
    Instances For

      The proposition P3, without the x₁ < x₂ and y₁ < y₂ assumptions.

      Equations
      Instances For

        The proposition P4, without numericity assumptions. In the references, the second part of the conjunction is stated as ∀ j, P3 x₁ x₂ y (y.moveRight j), which is equivalent to our statement by P3_comm and P3_neg. We choose to state everything in terms of left options for uniform treatment.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The conjunction of P2 and P4.

          Equations
          Instances For

            Symmetry properties of P1, P2, P3, and P4 #

            theorem Surreal.Multiplication.P3.trans {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {x₃ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (h₁ : Surreal.Multiplication.P3 x₁ x₂ y₁ y₂) (h₂ : Surreal.Multiplication.P3 x₂ x₃ y₁ y₂) :
            Surreal.Multiplication.P3 x₁ x₃ y₁ y₂

            Explicit calculations necessary for the main proof #

            theorem Surreal.Multiplication.mulOption_lt_iff_P1 {x : SetTheory.PGame} {y : SetTheory.PGame} {i : x.LeftMoves} {j : x.LeftMoves} {k : y.LeftMoves} {l : (-y).LeftMoves} :
            x.mulOption y i k < -x.mulOption (-y) j l Surreal.Multiplication.P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l)
            theorem Surreal.Multiplication.mulOption_lt_mul_iff_P3 {x : SetTheory.PGame} {y : SetTheory.PGame} {i : x.LeftMoves} {j : y.LeftMoves} :
            x.mulOption y i j < x * y Surreal.Multiplication.P3 (x.moveLeft i) x (y.moveLeft j) y
            theorem Surreal.Multiplication.P1_of_eq {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {x₃ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} {y₃ : SetTheory.PGame} (he : x₁ x₃) (h₁ : Surreal.Multiplication.P2 x₁ x₃ y₁) (h₃ : Surreal.Multiplication.P2 x₁ x₃ y₃) (h3 : Surreal.Multiplication.P3 x₁ x₂ y₂ y₃) :
            Surreal.Multiplication.P1 x₁ x₂ x₃ y₁ y₂ y₃
            theorem Surreal.Multiplication.P1_of_lt {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {x₃ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} {y₃ : SetTheory.PGame} (h₁ : Surreal.Multiplication.P3 x₃ x₂ y₂ y₃) (h₂ : Surreal.Multiplication.P3 x₁ x₃ y₂ y₁) :
            Surreal.Multiplication.P1 x₁ x₂ x₃ y₁ y₂ y₃

            The type of lists of arguments for P1, P2, and P4.

            Instances For

              The multiset associated to a list of arguments.

              Equations
              Instances For

                A list of arguments is numeric if all the arguments are.

                Equations
                • a.Numeric = xa.toMultiset, x.Numeric
                Instances For
                  theorem Surreal.Multiplication.Args.numeric_P24 {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} :
                  (Surreal.Multiplication.Args.P24 x₁ x₂ y).Numeric x₁.Numeric x₂.Numeric y.Numeric

                  The relation specifying when a list of (pregame) arguments is considered simpler than another: ArgsRel a₁ a₂ is true if a₁, considered as a multiset, can be obtained from a₂ by repeatedly removing a pregame from a₂ and adding back one or two options of the pregame.

                  Equations
                  Instances For

                    The statement that we will show by induction using the well-founded relation ArgsRel.

                    Equations
                    Instances For

                      The property that all arguments are numeric is leftward-closed under ArgsRel.

                      A specialized induction hypothesis used to prove P1.

                      Equations
                      Instances For

                        Symmetry properties of IH1 #

                        Specialize ih to obtain specialized induction hypotheses for P1 #

                        theorem Surreal.Multiplication.P3_of_ih {x : SetTheory.PGame} {y : SetTheory.PGame} (hy : y.Numeric) (ihyx : Surreal.Multiplication.IH1 y x) (i : x.LeftMoves) (k : y.LeftMoves) (l : (-y).LeftMoves) :
                        Surreal.Multiplication.P3 (x.moveLeft i) x (y.moveLeft k) (-(-y).moveLeft l)
                        theorem Surreal.Multiplication.P24_of_ih {x : SetTheory.PGame} {y : SetTheory.PGame} (ihxy : Surreal.Multiplication.IH1 x y) (i : x.LeftMoves) (j : x.LeftMoves) :
                        Surreal.Multiplication.P24 (x.moveLeft i) (x.moveLeft j) y
                        theorem Surreal.Multiplication.mulOption_lt_of_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (hy : y.Numeric) (ihxy : Surreal.Multiplication.IH1 x y) (ihyx : Surreal.Multiplication.IH1 y x) (i : x.LeftMoves) (j : x.LeftMoves) (k : y.LeftMoves) (l : (-y).LeftMoves) (h : x.moveLeft i < x.moveLeft j) :
                        x.mulOption y i k < -x.mulOption (-y) j l
                        theorem Surreal.Multiplication.mulOption_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric) (ihxy : Surreal.Multiplication.IH1 x y) (ihyx : Surreal.Multiplication.IH1 y x) (i : x.LeftMoves) (j : x.LeftMoves) (k : y.LeftMoves) (l : (-y).LeftMoves) :
                        x.mulOption y i k < -x.mulOption (-y) j l

                        P1 follows from the induction hypothesis.

                        A specialized induction hypothesis used to prove P2 and P4.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          A specialized induction hypothesis used to prove P4.

                          Equations
                          Instances For

                            Specialize ih' to obtain specialized induction hypotheses for P2 and P4 #

                            theorem Surreal.Multiplication.mulOption_lt_mul_of_equiv {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hn : x₁.Numeric) (h : Surreal.Multiplication.IH24 x₁ x₂ y) (he : x₁ x₂) (i : x₁.LeftMoves) (j : y.LeftMoves) :
                            x₁.mulOption y i j < x₂ * y
                            theorem Surreal.Multiplication.mul_right_le_of_equiv {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (h₁ : x₁.Numeric) (h₂ : x₂.Numeric) (h₁₂ : Surreal.Multiplication.IH24 x₁ x₂ y) (h₂₁ : Surreal.Multiplication.IH24 x₂ x₁ y) (he : x₁ x₂) :
                            x₁ * y x₂ * y

                            P2 follows from specialized induction hypotheses (one half of the equality).

                            The statement that all left options of x * y of the first kind are less than itself.

                            Equations
                            Instances For

                              That the left options of x * y are less than itself and the right options are greater, which is part of the condition that x * y is numeric, is equivalent to the conjunction of various MulOptionsLTMul statements for x, y and their negations. We only show the forward direction.

                              A condition just enough to deduce P3, which will always be used with x' being a left option of x₂. When y₁ is a left option of y₂, it can be deduced from induction hypotheses IH24 x₁ x₂ y₂, IH4 x₁ x₂ y₂, and (x₂ * y₂).Numeric (ih3_of_ih); when y₁ is not necessarily an option of y₂, it follows from the induction hypothesis for P3 (with x₂ replaced by a left option x') after the main theorem (P124) is established, and is used to prove P3 in full (P3_of_lt_of_lt).

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem Surreal.Multiplication.ih3_of_ih {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (h24 : Surreal.Multiplication.IH24 x₁ x₂ y) (h4 : Surreal.Multiplication.IH4 x₁ x₂ y) (hl : Surreal.Multiplication.MulOptionsLTMul x₂ y) (i : x₂.LeftMoves) (j : y.LeftMoves) :
                                Surreal.Multiplication.IH3 x₁ (x₂.moveLeft i) x₂ (y.moveLeft j) y
                                theorem Surreal.Multiplication.P3_of_le_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (i : x₂.LeftMoves) (h : Surreal.Multiplication.IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hl : x₁ x₂.moveLeft i) :
                                Surreal.Multiplication.P3 x₁ x₂ y₁ y₂
                                theorem Surreal.Multiplication.P3_of_lt {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (h : ∀ (i : x₂.LeftMoves), Surreal.Multiplication.IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hs : ∀ (i : (-x₁).LeftMoves), Surreal.Multiplication.IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂) (hl : x₁ < x₂) :
                                Surreal.Multiplication.P3 x₁ x₂ y₁ y₂

                                P3 follows from IH3 (so P4 (with y₁ a left option of y₂) follows from the induction hypothesis).

                                The main chunk of Theorem 8 in [Conway2001] / Theorem 3.8 in [SchleicherStoll].

                                theorem SetTheory.PGame.Numeric.mul {x : SetTheory.PGame} {y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric) :
                                (x * y).Numeric
                                theorem SetTheory.PGame.P24 {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) :
                                theorem SetTheory.PGame.Equiv.mul_congr_left {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y : SetTheory.PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) (he : x₁ x₂) :
                                x₁ * y x₂ * y
                                theorem SetTheory.PGame.Equiv.mul_congr_right {x : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx : x.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (he : y₁ y₂) :
                                x * y₁ x * y₂
                                theorem SetTheory.PGame.Equiv.mul_congr {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ x₂) (hy : y₁ y₂) :
                                x₁ * y₁ x₂ * y₂
                                theorem SetTheory.PGame.P3_of_lt_of_lt {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₁ : SetTheory.PGame} {y₂ : SetTheory.PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ < x₂) (hy : y₁ < y₂) :
                                Surreal.Multiplication.P3 x₁ x₂ y₁ y₂

                                One additional inductive argument that supplies the last missing part of Theorem 8.

                                theorem SetTheory.PGame.Numeric.mul_pos {x₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) :
                                0 < x₁ * x₂