Documentation

LeanMlir.Proofs.Foundation.GramQ

Gram-matrix identities by one kernel check #

The Lipschitz certificates bound ‖W‖₂ through Gram matrices G = W Wᵀ (and H = Gᵀ G for the Schatten-8 step), and each instance has to establish ∀ a b, G a b = ∑ j, W a j * W b j for concrete rational data. Over ℝ, entry by entry with simp/norm_num, that cost up to ~270 s per matrix. Here the data is ℚ, the ℝ matrices are DEFINED as its cast (castM), and gram_eq_of_check turns one kernel-evaluated gramCheck into the whole identity; abs_le_of_check does the same for an entrywise bound |A i j| ≤ c.

H = Gᵀ G is the same statement with W := fun a c => G c a.

source
def Proofs.castM {m n : ℕ} (A : Fin m → Fin n → ℚ) :
Fin m → Fin n → ℝ

A ℚ matrix read over ℝ.

Equations
Instances For
    source
    def Proofs.rowDotQ {m n : ℕ} (W : Fin m → Fin n → ℚ) (a b : Fin m) :
    ℚ

    ∑ j, W a j * W b j over ℚ, as a sum the kernel can evaluate.

    Equations
    Instances For
      source
      def Proofs.gramCheck {m n : ℕ} (G : Fin m → Fin m → ℚ) (W : Fin m → Fin n → ℚ) :
      Bool

      Every entry of G is the row inner product of W — the check decide +kernel runs.

      Equations
      Instances For
        source
        theorem Proofs.gram_eq_of_check {m n : ℕ} (G : Fin m → Fin m → ℚ) (W : Fin m → Fin n → ℚ) (h : gramCheck G W = true) (a b : Fin m) :
        castM G a b = ∑ j : Fin n, castM W a j * castM W b j

        ⭐ A passing gramCheck is the Gram identity over ℝ.

        source
        def Proofs.absLeCheck {m n : ℕ} (A : Fin m → Fin n → ℚ) (c : ℚ) :
        Bool

        Every entry of A is at most c in absolute value — the check decide +kernel runs.

        Equations
        Instances For
          source
          theorem Proofs.abs_le_of_check {m n : ℕ} (A : Fin m → Fin n → ℚ) (c : ℚ) (h : absLeCheck A c = true) (i : Fin m) (j : Fin n) :
          |castM A i j| ≤ ↑c

          ⭐ A passing absLeCheck bounds every entry over ℝ.