Documentation

CompPoly.Univariate.NTT.FastMul

Fast Multiplication via NTT #

This file wires forward NTT, pointwise multiplication, and inverse NTT into a spec/implementation pipeline.

source
@[inline]
def CompPoly.CPolynomial.NTT.FastMul.pointwiseMul {R : Type u_1} [Field R] (D : Domain R) (a b : Array R) :
Array R

Pointwise multiplication in evaluation form.

Instances For
    source
    @[simp]
    theorem CompPoly.CPolynomial.NTT.FastMul.size_pointwiseMul {R : Type u_1} [Field R] (D : Domain R) (a b : Array R) :
    (pointwiseMul D a b).size = D.n
    source
    @[inline]
    def CompPoly.CPolynomial.NTT.FastMul.Raw.fastMulSpec {R : Type u_1} [Field R] [BEq R] (D : Domain R) (p q : Raw R) :
    Raw R

    Raw spec pipeline for NTT-based multiplication.

    This is the low-level array computation and deliberately does not trim the output.

    Instances For
      source
      @[inline]
      def CompPoly.CPolynomial.NTT.FastMul.Raw.fastMulImpl {R : Type u_1} [Field R] [BEq R] (D : Domain R) (p q : Raw R) :
      Raw R

      Raw implementation pipeline for NTT-based multiplication.

      Correctness as ordinary polynomial multiplication requires Domain.fits D p q; see fastMulImpl_trim_eq_mul. Without this precondition, this function only exposes the raw NTT pipeline result, which may include cyclic wraparound and has no product-correctness guarantee. The output is not trimmed; use FastMul.fastMulImpl for the canonical public API.

      Instances For
        source
        theorem CompPoly.CPolynomial.NTT.FastMul.Raw.fastMulImpl_correct {R : Type u_1} [Field R] [BEq R] (D : Domain R) (p q : Raw R) :
        fastMulImpl D p q = fastMulSpec D p q
        source
        theorem CompPoly.CPolynomial.NTT.FastMul.Raw.fastMulSpec_coeff {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : Raw R) (hfit : D.fits p q) (i : ℕ) :
        (fastMulSpec D p q).coeff i = (p * q).coeff i
        source
        theorem CompPoly.CPolynomial.NTT.FastMul.Raw.fastMulSpec_trim_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : Raw R) (hfit : D.fits p q) :
        (fastMulSpec D p q).trim = p * q
        source
        theorem CompPoly.CPolynomial.NTT.FastMul.Raw.fastMulImpl_trim_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : Raw R) (hfit : D.fits p q) :
        (fastMulImpl D p q).trim = p * q
        source
        @[inline]
        def CompPoly.CPolynomial.NTT.FastMul.fastMulSpec {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) :
        CPolynomial R

        Spec pipeline for NTT-based multiplication as a canonical polynomial.

        Instances For
          source
          @[inline]
          def CompPoly.CPolynomial.NTT.FastMul.fastMulImpl {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) :
          CPolynomial R

          Implementation pipeline for NTT-based multiplication as a canonical polynomial.

          Correctness as ordinary polynomial multiplication requires Domain.fits D p.val q.val; see fastMulImpl_eq_mul. Without this precondition, the raw NTT computation may include cyclic wraparound before canonicalization.

          Instances For
            source
            @[inline]
            def CompPoly.CPolynomial.NTT.FastMul.safeFastMul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) (_hfit : D.fits ↑p ↑q) :
            CPolynomial R

            Safe NTT-based multiplication wrapper.

            This computes with fastMulImpl, but requires the caller to provide the Domain.fits D p.val q.val proof at the call site.

            Instances For
              source
              theorem CompPoly.CPolynomial.NTT.FastMul.fastMulImpl_correct {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) :
              fastMulImpl D p q = fastMulSpec D p q
              source
              theorem CompPoly.CPolynomial.NTT.FastMul.fastMulSpec_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) (hfit : D.fits ↑p ↑q) :
              fastMulSpec D p q = p * q
              source
              theorem CompPoly.CPolynomial.NTT.FastMul.fastMulImpl_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) (hfit : D.fits ↑p ↑q) :
              fastMulImpl D p q = p * q
              source
              theorem CompPoly.CPolynomial.NTT.FastMul.safeFastMul_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (D : Domain R) (p q : CPolynomial R) (hfit : D.fits ↑p ↑q) :
              safeFastMul D p q hfit = p * q

              The safe wrapper is equivalent to ordinary canonical polynomial multiplication.

              There are no extra assumptions because the required Domain.fits D p.val q.val proof is already an argument of safeFastMul.

              source
              @[inline]
              def CompPoly.CPolynomial.NTT.FastMul.withFallback {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (FittingDomain R requiredLen)) (p q : CPolynomial R) :
              CPolynomial R

              NTT-backed multiplication with canonical multiplication as a fallback.

              The selector should return a domain fitting the required convolution length. When it does, this uses fastMulImpl; otherwise it falls back to canonical CPolynomial multiplication.

              Instances For
                source
                theorem CompPoly.CPolynomial.NTT.FastMul.withFallback_eq_mul {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (bestDomainForLength? : (requiredLen : ℕ) → Option (FittingDomain R requiredLen)) (p q : CPolynomial R) :
                withFallback bestDomainForLength? p q = p * q

                withFallback agrees with canonical polynomial multiplication.