Approximation lower bounds relative to supplied functions #
The approximation scheme starts with the supplied functions. Its existing union-of-exceptions proof counts each shared gate once. Any uniform target separation therefore bounds the minimum relative error cost.
theorem
Algebraic.Approximation.Scheme.relativeCostComplexity_lowerBound
{X : Type u_1}
{σ : Signature}
{U : Type u_3}
{A : Type u_4}
{n : ℕ}
[Fintype X]
[DecidableEq X]
{interpretation : Interpretation σ U}
{approximation : Interpretation σ A}
{decode : A → X → U}
{sources : X → Fin n → U}
{initial : Fin n → A}
(scheme : Scheme interpretation approximation decode sources initial)
[DecidableRel scheme.relation]
(target : X → U)
(lower : ℕ)
(separated : ∀ (value : A), lower ≤ (failures scheme.relation decode value target).card)
:
↑lower ≤ Circuit.relativeCostComplexity interpretation scheme.errorCost (fun (x : X) (x_1 : Fin 1) => target x) sources
If every approximate value fails on at least lower samples, computing
the target from the initialized sources costs at least lower local errors.
noncomputable def
Algebraic.Approximation.Scheme.ofLocalErrors
{X : Type u_1}
{U : Type u_2}
{σ : Signature}
{A : Type u_4}
{n : ℕ}
[Fintype X]
[DecidableEq X]
[DecidableEq U]
(interpretation : Interpretation σ U)
(approximation : Interpretation σ A)
(decode : A → X → U)
(sources : X → Fin n → U)
(initial : Fin n → A)
(errorCost : OperationCost σ)
(inputExact : ∀ (x : X) (i : Fin n), sources x i = decode (initial i) x)
(localErrors :
∀ (op : σ.Op) (arguments : Fin (σ.Arity op) → A),
{x : X |
(interpretation op fun (i : Fin (σ.Arity op)) => decode (arguments i) x) ≠ decode (approximation op arguments) x}.card ≤ errorCost op)
:
Scheme interpretation approximation decode sources initial
Construct the equality-based scheme directly from exact supplied representatives and a bound on the number of local disagreements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algebraic.Approximation.Scheme.relativeCostComplexity_lowerBound_of_localErrors
{X : Type u_1}
{U : Type u_2}
{σ : Signature}
{A : Type u_4}
{n : ℕ}
[Fintype X]
[DecidableEq X]
[DecidableEq U]
(interpretation : Interpretation σ U)
(approximation : Interpretation σ A)
(decode : A → X → U)
(sources : X → Fin n → U)
(initial : Fin n → A)
(errorCost : OperationCost σ)
(inputExact : ∀ (x : X) (i : Fin n), sources x i = decode (initial i) x)
(localErrors :
∀ (op : σ.Op) (arguments : Fin (σ.Arity op) → A),
{x : X |
(interpretation op fun (i : Fin (σ.Arity op)) => decode (arguments i) x) ≠ decode (approximation op arguments) x}.card ≤ errorCost op)
(target : X → U)
(lower : ℕ)
(separated : ∀ (value : A), lower ≤ {x : X | target x ≠ decode value x}.card)
:
↑lower ≤ Circuit.relativeCostComplexity interpretation errorCost (fun (x : X) (x_1 : Fin 1) => target x) sources
The equality-based approximation bound stated directly in terms of local disagreements and exact supplied representatives.