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.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Lean.Omega.LinearCombo.ext {a : Lean.Omega.LinearCombo} {b : Lean.Omega.LinearCombo} (w₁ : a.const = b.const) (w₂ : a.coeffs = b.coeffs) :
    a = b

    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
    • lc.eval values = lc.const + lc.coeffs.dot values
    Instances For
      @[simp]
      theorem Lean.Omega.LinearCombo.eval_nil {lc : Lean.Omega.LinearCombo} :
      lc.eval [] = lc.const

      The i-th coordinate function.

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

        Implementation of addition on LinearCombo.

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

          Implementation of subtraction on LinearCombo.

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

            Implementation of negation on LinearCombo.

            Equations
            • lc.neg = { const := -lc.const, coeffs := -lc.coeffs }
            Instances For
              @[simp]
              @[simp]

              Implementation of scalar multiplication of a LinearCombo by an Int.

              Equations
              • lc.smul i = { const := i * lc.const, coeffs := lc.coeffs.smul i }
              Instances For
                @[simp]
                theorem Lean.Omega.LinearCombo.smul_const {lc : Lean.Omega.LinearCombo} {i : Int} :
                (i * lc).const = i * lc.const
                @[simp]
                theorem Lean.Omega.LinearCombo.smul_coeffs {lc : Lean.Omega.LinearCombo} {i : Int} :
                (i * lc).coeffs = i * lc.coeffs
                @[simp]
                theorem Lean.Omega.LinearCombo.add_eval (l₁ : Lean.Omega.LinearCombo) (l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs) :
                (l₁ + l₂).eval v = l₁.eval v + l₂.eval v
                @[simp]
                @[simp]
                theorem Lean.Omega.LinearCombo.sub_eval (l₁ : Lean.Omega.LinearCombo) (l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs) :
                (l₁ - l₂).eval v = l₁.eval v - l₂.eval v
                @[simp]
                theorem Lean.Omega.LinearCombo.smul_eval (lc : Lean.Omega.LinearCombo) (i : Int) (v : Lean.Omega.Coeffs) :
                (i * lc).eval v = i * lc.eval v
                theorem Lean.Omega.LinearCombo.smul_eval_comm (lc : Lean.Omega.LinearCombo) (i : Int) (v : Lean.Omega.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
                • l₁.mul l₂ = l₂.const * l₁ + l₁.const * l₂ - { const := l₁.const * l₂.const, coeffs := [] }
                Instances For
                  theorem Lean.Omega.LinearCombo.mul_eval_of_const_left (l₁ : Lean.Omega.LinearCombo) (l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.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₁ : Lean.Omega.LinearCombo) (l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs) (w : l₂.coeffs.isZero) :
                  (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
                  theorem Lean.Omega.LinearCombo.mul_eval (l₁ : Lean.Omega.LinearCombo) (l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs) (w : l₁.coeffs.isZero l₂.coeffs.isZero) :
                  (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v