Documentation

MIPRE.Foundations.Repeat.Dom

Domination by a monomial in the parameters and the input size #

The time bounds of the repeated verifier (thm:parallel-repetition) have the shape c (W + 1)^m X^{e (K + 1)}: W a number dominating all the parameters at index n (the argument MIPRE.Repetition.arg), X = |d| + 1 the size of the input and K the input's degree. Dom W X K c m e v says v is below such a monomial. The costs of the programs are sums and products of quantities each of which is below W, below X, or a constant, and the combinators here — add, mul, pow, ofLeW, ofLeX, const — assemble the exponents, so that the final c, m, e are produced by the chain rather than computed by hand. The exponent of X is counted in units of K + 1, so that a bound X^{e (K + 1)} with e independent of K is what comes out, as the degree clause of the theorem needs.

source
def MIPRE.Repeat.Dom (W X K c m e v : ℕ) :
Prop

v ≤ c (W + 1)^m X^{e (K + 1)}.

Equations
Instances For
    source
    theorem MIPRE.Repeat.Dom.le {W X K c m e v : ℕ} (h : Dom W X K c m e v) :
    v ≤ c * (W + 1) ^ m * X ^ (e * (K + 1))
    source
    theorem MIPRE.Repeat.Dom.of_le {W X K c m e v v' : ℕ} (h : Dom W X K c m e v) (hv : v' ≤ v) :
    Dom W X K c m e v'
    source
    theorem MIPRE.Repeat.Dom.const {W X K : ℕ} (c : ℕ) :
    Dom W X K c 0 0 c
    source
    theorem MIPRE.Repeat.Dom.ofLeW {W X K v : ℕ} (h : v ≤ W) :
    Dom W X K 1 1 0 v
    source
    theorem MIPRE.Repeat.Dom.ofAffine {W X K a b v : ℕ} (h : v ≤ a * W + b) :
    Dom W X K (a + b) 1 0 v

    An affine function of W is dominated by (a + b)(W + 1).

    source
    theorem MIPRE.Repeat.Dom.ofAffineX {W X K : ℕ} (hX : 1 ≤ X) {a b v : ℕ} (h : v ≤ a * X + b) :
    Dom W X K (a + b) 0 1 v

    An affine function of X is dominated by (a + b) X^{K+1}.

    source
    theorem MIPRE.Repeat.Dom.ofLeX {W X K : ℕ} (hX : 1 ≤ X) {v : ℕ} (h : v ≤ X) :
    Dom W X K 1 0 1 v
    source
    theorem MIPRE.Repeat.Dom.mono {W X K : ℕ} (hX : 1 ≤ X) {c c' m m' e e' v : ℕ} (h : Dom W X K c m e v) (hc : c ≤ c') (hm : m ≤ m') (he : e ≤ e') :
    Dom W X K c' m' e' v
    source
    theorem MIPRE.Repeat.Dom.add {W X K : ℕ} (hX : 1 ≤ X) {c₁ c₂ m₁ m₂ e₁ e₂ v₁ v₂ : ℕ} (h₁ : Dom W X K c₁ m₁ e₁ v₁) (h₂ : Dom W X K c₂ m₂ e₂ v₂) :
    Dom W X K (c₁ + c₂) (max m₁ m₂) (max e₁ e₂) (v₁ + v₂)
    source
    theorem MIPRE.Repeat.Dom.mul {W X K c₁ c₂ m₁ m₂ e₁ e₂ v₁ v₂ : ℕ} (h₁ : Dom W X K c₁ m₁ e₁ v₁) (h₂ : Dom W X K c₂ m₂ e₂ v₂) :
    Dom W X K (c₁ * c₂) (m₁ + m₂) (e₁ + e₂) (v₁ * v₂)
    source
    theorem MIPRE.Repeat.Dom.pow {W X K c m e v : ℕ} (h : Dom W X K c m e v) (p : ℕ) :
    Dom W X K (c ^ p) (m * p) (e * p) (v ^ p)
    source
    theorem MIPRE.Repeat.Dom.powK {W X K : ℕ} (hX : 1 ≤ X) :
    Dom W X K 1 0 1 (X ^ K)

    X^K itself: one unit of the exponent.