Documentation

LeanCert.Engine.IntervalVector

Interval Vector Arithmetic #

This file provides vector and matrix operations for Dyadic intervals, enabling verified linear algebra computations.

Main definitions #

Main theorems #

source
@[reducible, inline]
abbrev LeanCert.Engine.IntervalVector :
Type

A vector of intervals representing bounded real vectors

Equations
Instances For

    Scalar Operations #

    source
    def LeanCert.Engine.IntervalVector.scalarMulInterval (w : ℚ) (I : Core.IntervalDyadic) (prec : ℤ := -53) :
    Core.IntervalDyadic

    Multiply an interval by a rational scalar. Uses the existing interval multiplication by converting the scalar to a singleton.

    Equations
    Instances For
      source
      theorem LeanCert.Engine.IntervalVector.mem_scalarMulInterval {w : ℚ} {x : ℝ} {I : Core.IntervalDyadic} (hx : x ∈ I) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) :
      ↑w * x ∈ scalarMulInterval w I prec

      Soundness of scalar-interval multiplication

      Dot Product #

      source
      def LeanCert.Engine.IntervalVector.dotProduct (weights : List ℚ) (inputs : IntervalVector) (prec : ℤ := -53) :
      Core.IntervalDyadic

      Dot product of rational weights with an interval vector. Returns an interval containing all possible dot products.

      Equations
      Instances For
        source
        def LeanCert.Engine.IntervalVector.realDotProduct (weights : List ℚ) (values : List ℝ) :
        ℝ

        Helper: real dot product of two lists

        Equations
        Instances For
          source
          theorem LeanCert.Engine.IntervalVector.mem_zero_singleton :
          0 ∈ Core.IntervalDyadic.singleton (Core.Dyadic.ofInt 0)

          Zero is in the zero singleton

          source
          theorem LeanCert.Engine.IntervalVector.mem_dotProduct_aux (weights : List ℚ) (xs : List ℝ) (Is : IntervalVector) (hlen : weights.length = List.length Is) (hxlen : xs.length = List.length Is) (hmem : ∀ (i : ℕ) (hi : i < List.length Is), xs[i] ∈ Is[i]) (prec : ℤ) (hprec : prec ≤ 0) :
          realDotProduct weights xs ∈ dotProduct weights Is prec

          Soundness of dot product for matching-length lists

          source
          theorem LeanCert.Engine.IntervalVector.mem_dotProduct {weights : List ℚ} {xs : List ℝ} {Is : IntervalVector} (hlen : weights.length = List.length Is) (hxlen : xs.length = List.length Is) (hmem : ∀ (i : ℕ) (hi : i < List.length Is), xs[i] ∈ Is[i]) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) :
          realDotProduct weights xs ∈ dotProduct weights Is prec

          Soundness of dot product: if each x_i ∈ I_i, then ∑ w_i * x_i ∈ dotProduct

          Vector Addition #

          source
          def LeanCert.Engine.IntervalVector.add (Is Js : IntervalVector) :
          IntervalVector

          Pointwise addition of two interval vectors

          Equations
          Instances For
            source
            theorem LeanCert.Engine.IntervalVector.mem_add_component {x y : ℝ} {I J : Core.IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) :
            x + y ∈ I.add J

            Soundness of vector addition (component-wise)

            source
            def LeanCert.Engine.IntervalVector.zero :
            Core.IntervalDyadic

            Zero interval (singleton at 0)

            Equations
            Instances For
              source
              theorem LeanCert.Engine.IntervalVector.mem_zero :
              0 ∈ zero

              Membership in zero interval

              Matrix-Vector Operations #

              source
              def LeanCert.Engine.IntervalVector.matVecMul (W : List (List ℚ)) (x : IntervalVector) (prec : ℤ := -53) :
              IntervalVector

              Matrix-vector multiplication: W · x where W is a matrix of rational weights and x is an interval vector. Each row of W is dotted with x.

              Equations
              Instances For
                source
                def LeanCert.Engine.IntervalVector.realMatVecMul (W : List (List ℚ)) (x : List ℝ) :
                List ℝ

                Real matrix-vector multiplication

                Equations
                Instances For
                  source
                  theorem LeanCert.Engine.IntervalVector.mem_matVecMul {W : List (List ℚ)} {xs : List ℝ} {Is : IntervalVector} (hWcols : ∀ row ∈ W, row.length = List.length Is) (hxlen : xs.length = List.length Is) (hmem : ∀ (i : ℕ) (hi : i < List.length Is), xs[i] ∈ Is[i]) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) (i : ℕ) (hi : i < W.length) :
                  (realMatVecMul W xs)[i] ∈ (matVecMul W Is prec)[i]

                  Soundness of matrix-vector multiplication

                  source
                  def LeanCert.Engine.IntervalVector.addBias (Is : IntervalVector) (bias : List ℚ) (prec : ℤ := -53) :
                  IntervalVector

                  Add a rational bias vector to an interval vector

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def LeanCert.Engine.IntervalVector.realAddBias (xs : List ℝ) (bias : List ℚ) :
                    List ℝ

                    Real vector plus bias

                    Equations
                    Instances For
                      source
                      theorem LeanCert.Engine.IntervalVector.mem_addBias {xs : List ℝ} {Is : IntervalVector} {bias : List ℚ} (hlen : xs.length = List.length Is) (hblen : bias.length = List.length Is) (hmem : ∀ (i : ℕ) (hi : i < List.length Is), xs[i] ∈ Is[i]) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) (i : ℕ) (hi : i < List.length Is) :
                      (realAddBias xs bias)[i] ∈ (Is.addBias bias prec)[i]

                      Soundness of bias addition