Documentation

Init.Omega.LinearCombo

Linear combinations #

We use this data structure while processing hypotheses.

Internal representation of a linear combination of atoms, and a constant term.

  • const : Int

    Constant term.

  • coeffs : Coeffs

    Coefficients of the atoms.

Instances For
    theorem Lean.Omega.LinearCombo.ext {a b : LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) :
    a = b

    Check if a linear combination is an atom, i.e. the constant term is zero and there is exactly one nonzero coefficient, which is one.

    Equations
      Instances For

        Evaluate a linear combination ⟨r, [c_1, …, c_k]⟩ at values [v_1, …, v_k] to obtain r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0)))).

        Equations
          Instances For

            The i-th coordinate function.

            Equations
              Instances For
                theorem Lean.Omega.LinearCombo.coordinate_eval_2 {a0 a1 a2 : Int} {t : List Int} :
                (coordinate 2).eval (Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2
                theorem Lean.Omega.LinearCombo.coordinate_eval_3 {a0 a1 a2 a3 : Int} {t : List Int} :
                (coordinate 3).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3
                theorem Lean.Omega.LinearCombo.coordinate_eval_4 {a0 a1 a2 a3 a4 : Int} {t : List Int} :
                (coordinate 4).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4
                theorem Lean.Omega.LinearCombo.coordinate_eval_5 {a0 a1 a2 a3 a4 a5 : Int} {t : List Int} :
                (coordinate 5).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5
                theorem Lean.Omega.LinearCombo.coordinate_eval_6 {a0 a1 a2 a3 a4 a5 a6 : Int} {t : List Int} :
                (coordinate 6).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6
                theorem Lean.Omega.LinearCombo.coordinate_eval_7 {a0 a1 a2 a3 a4 a5 a6 a7 : Int} {t : List Int} :
                (coordinate 7).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7
                theorem Lean.Omega.LinearCombo.coordinate_eval_8 {a0 a1 a2 a3 a4 a5 a6 a7 a8 : Int} {t : List Int} :
                (coordinate 8).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8
                theorem Lean.Omega.LinearCombo.coordinate_eval_9 {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 : Int} {t : List Int} :
                (coordinate 9).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9

                Implementation of addition on LinearCombo.

                Equations
                  Instances For
                    @[simp]
                    theorem Lean.Omega.LinearCombo.add_const {l₁ l₂ : LinearCombo} :
                    (l₁ + l₂).const = l₁.const + l₂.const
                    @[simp]
                    theorem Lean.Omega.LinearCombo.add_coeffs {l₁ l₂ : LinearCombo} :
                    (l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs

                    Implementation of subtraction on LinearCombo.

                    Equations
                      Instances For
                        @[simp]
                        theorem Lean.Omega.LinearCombo.sub_const {l₁ l₂ : LinearCombo} :
                        (l₁ - l₂).const = l₁.const - l₂.const
                        @[simp]
                        theorem Lean.Omega.LinearCombo.sub_coeffs {l₁ l₂ : LinearCombo} :
                        (l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs

                        Implementation of negation on LinearCombo.

                        Equations
                          Instances For
                            theorem Lean.Omega.LinearCombo.sub_eq_add_neg (l₁ l₂ : LinearCombo) :
                            l₁ - l₂ = l₁ + -l₂

                            Implementation of scalar multiplication of a LinearCombo by an Int.

                            Equations
                              Instances For
                                @[simp]
                                theorem Lean.Omega.LinearCombo.smul_const {lc : LinearCombo} {i : Int} :
                                (i * lc).const = i * lc.const
                                @[simp]
                                @[simp]
                                theorem Lean.Omega.LinearCombo.add_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :
                                (l₁ + l₂).eval v = l₁.eval v + l₂.eval v
                                @[simp]
                                @[simp]
                                theorem Lean.Omega.LinearCombo.sub_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :
                                (l₁ - l₂).eval v = l₁.eval v - l₂.eval v
                                @[simp]
                                theorem Lean.Omega.LinearCombo.smul_eval (lc : LinearCombo) (i : Int) (v : Coeffs) :
                                (i * lc).eval v = i * lc.eval v
                                theorem Lean.Omega.LinearCombo.smul_eval_comm (lc : LinearCombo) (i : Int) (v : Coeffs) :
                                (i * lc).eval v = lc.eval v * i

                                Multiplication of two linear combinations. This is useful only if at least one of the linear combinations is constant, and otherwise should be considered as a junk value.

                                Equations
                                  Instances For
                                    theorem Lean.Omega.LinearCombo.mul_eval_of_const_left (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero) :
                                    (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
                                    theorem Lean.Omega.LinearCombo.mul_eval_of_const_right (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₂.coeffs.isZero) :
                                    (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
                                    theorem Lean.Omega.LinearCombo.mul_eval (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero l₂.coeffs.isZero) :
                                    (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v