Documentation

AlgebraicComplexity.Formulas

source
inductive AlgebraicComplexity.Formulas.Formula (α : Type u) (Idx : Type v) :
Type (max u v)
Instances For
    source
    def AlgebraicComplexity.Formulas.«termC[_]» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def AlgebraicComplexity.Formulas.«termV[_]» :
      Lean.ParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance AlgebraicComplexity.Formulas.zero {α : Type u} {Idx : Type v} [Ring α] :
        Zero (Formula α Idx)
        Equations
        source
        instance AlgebraicComplexity.Formulas.one {α : Type u} {Idx : Type v} [Ring α] :
        One (Formula α Idx)
        Equations
        source
        instance AlgebraicComplexity.Formulas.add {α : Type u} {Idx : Type v} :
        Add (Formula α Idx)
        Equations
        source
        instance AlgebraicComplexity.Formulas.neg {α : Type u} {Idx : Type v} :
        Neg (Formula α Idx)
        Equations
        source
        instance AlgebraicComplexity.Formulas.sub {α : Type u} {Idx : Type v} :
        Sub (Formula α Idx)
        Equations
        source
        instance AlgebraicComplexity.Formulas.mul {α : Type u} {Idx : Type v} :
        Mul (Formula α Idx)
        Equations
        source
        def AlgebraicComplexity.Formulas.inputSize {α : Type u} {Idx : Type v} [Fintype Idx] :
        Formula α Idx → ℕ
        Equations
        Instances For
          source
          def AlgebraicComplexity.Formulas.size {α : Type u} {Idx : Type v} (f : Formula α Idx) :
          ℕ
          Equations
          Instances For
            source
            def AlgebraicComplexity.Formulas.depth {α : Type u} {Idx : Type v} (f : Formula α Idx) :
            ℕ
            Equations
            Instances For
              source
              noncomputable def AlgebraicComplexity.Formulas.evalToPolynomial {α : Type u} {Idx : Type v} [CommRing α] (f : Formula α Idx) :
              MvPolynomial Idx α
              Equations
              Instances For
                source
                theorem AlgebraicComplexity.Formulas.size_zero_const_or_var {α : Type u} {Idx : Type v} (f : Formula α Idx) :
                size f = 0 → (∃ (x : Idx), f = Formula.CVar x) ∨ ∃ (c : α), f = C[c]
                source
                theorem AlgebraicComplexity.Formulas.size_highest_degree {α : Type u} {Idx : Type v} [CommRing α] [Nontrivial α] (f : Formula α Idx) :
                size f ≥ (evalToPolynomial f).totalDegree - 1
                source
                def AlgebraicComplexity.Formulas.coeFormula {α : Type u} {Idx₁ : Type u_1} {Idx₂ : Type u_2} [Coe Idx₁ Idx₂] (f : Formula α Idx₁) :
                Formula α Idx₂

                coerce_up f coerces a formula f in n variables to a formula in n + 1 variables.

                Equations
                Instances For
                  source
                  instance AlgebraicComplexity.Formulas.instCoeFormula {α : Type u} {Idx₁ : Type u_1} {Idx₂ : Type u_2} [Coe Idx₁ Idx₂] :
                  Coe (Formula α Idx₁) (Formula α Idx₂)

                  This is the Coe typeclass instance for the above coercion. T

                  Equations
                  source
                  theorem AlgebraicComplexity.Formulas.coeFormula_composes_rename {α : Type u} {Idx₁ : Type u_1} {Idx₂ : Type u_2} [CommRing α] [instCoe : Coe Idx₁ Idx₂] (f : Formula α Idx₁) (p : MvPolynomial Idx₁ α) (heval : evalToPolynomial f = p) :
                  evalToPolynomial (coeFormula f) = (MvPolynomial.rename Coe.coe) p
                  source
                  def AlgebraicComplexity.Formulas.FormulaComplexityUpperBound {α : Type u} {ID : Type u_1} [CommRing α] (p : MvPolynomial ID α) (size_bound : ℕ) :
                  Prop

                  The complexity of a polynomial p, denoted L p is the size of the smallest formula that evaluates to it

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def AlgebraicComplexity.Formulas.FormulaComplexityLowerBound {α : Type u} {ID : Type u_1} [CommRing α] (p : MvPolynomial ID α) (size_bound : ℕ) :
                    Prop
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem AlgebraicComplexity.Formulas.complexity_UB_monomial {α : Type u} {ID : Type u_1} [CommRing α] [Nontrivial α] (deg : ℕ) :
                      have my_monomial := fun (x : ID) => MvPolynomial.X x ^ deg; ∀ (x : ID), FormulaComplexityUpperBound (my_monomial x) (2 * deg + 1)