Documentation

Complexity.Computability.Circuit.Continuity

The modulus of continuity of circuit complexity #

Over a finite carrier U and a complete interpretation I, the modulus of continuity of circuit complexity, ω_{I,n,m}(r) (Cslib.Circuits.complexityModulus), is the largest change |C_I(f) - C_I(g)| in the complexity of two functions with n inputs and m outputs that differ on at most r inputs, that is, at Hamming distance at most r as functions of their inputs. It is a natural number, it is attained (Cslib.Circuits.exists_dist_complexity_eq_complexityModulus), it increases with r and vanishes at r = 0, and it is subadditive, ω(r + s) ≤ ω(r) + ω(s) (Cslib.Circuits.complexityModulus_add_le): a change on r + s inputs is a change on r inputs followed by a change on s inputs. In particular ω(r) ≤ r ω(1).

A function with one output is at the Hamming distance of its single value (Cslib.Circuits.hammingDist_single), so the modulus for one output measures changes of single-valued functions. For the De Morgan basis the modulus at the square root of the number of inputs is located in Complexity.Computability.Circuit.Boolean.Continuity.

Main definitions #

Main results #

References #

source
@[simp]
theorem Cslib.Circuits.hammingDist_single {U : Type u_1} [Fintype U] [DecidableEq U] {n : ℕ} (f g : (Fin n → U) → U) :
hammingDist (single f) (single g) = hammingDist f g

A function with one output is at the Hamming distance of its single value.

source
noncomputable def Cslib.Circuits.complexityModulus {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] (I : Interpretation σ U) [I.IsComplete] (n m r : ℕ) :
ℕ

The modulus of continuity ω_{I,n,m}(r) of circuit complexity: the largest change |C_I(f) - C_I(g)| in the complexity of two functions with n inputs and m outputs over a finite carrier U that differ on at most r inputs.

Instances For
    source
    theorem Cslib.Circuits.dist_complexity_le_complexityModulus {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m r : ℕ} {I : Interpretation σ U} [I.IsComplete] {f g : (Fin n → U) → Fin m → U} (h : hammingDist f g ≤ r) :
    (complexity I f).dist (complexity I g) ≤ complexityModulus I n m r

    Functions that differ on at most r inputs have complexities at most ω(r) apart.

    source
    theorem Cslib.Circuits.complexityModulus_le_iff {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m r : ℕ} {I : Interpretation σ U} [I.IsComplete] {k : ℕ} :
    complexityModulus I n m r ≤ k ↔ ∀ (f g : (Fin n → U) → Fin m → U), hammingDist f g ≤ r → (complexity I f).dist (complexity I g) ≤ k

    The modulus is the least bound on the change in complexity over changes on at most r inputs.

    source
    theorem Cslib.Circuits.exists_dist_complexity_eq_complexityModulus {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m r : ℕ} {I : Interpretation σ U} [I.IsComplete] [Nonempty U] :
    ∃ (f : (Fin n → U) → Fin m → U) (g : (Fin n → U) → Fin m → U), hammingDist f g ≤ r ∧ (complexity I f).dist (complexity I g) = complexityModulus I n m r

    The modulus is attained.

    source
    theorem Cslib.Circuits.complexityModulus_mono {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] :
    Monotone (complexityModulus I n m)

    The modulus increases with the number of changed inputs.

    source
    @[simp]
    theorem Cslib.Circuits.complexityModulus_zero {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m : ℕ} {I : Interpretation σ U} [I.IsComplete] :
    complexityModulus I n m 0 = 0

    Changing no input does not change the complexity.

    source
    theorem Cslib.Circuits.complexityModulus_add_le {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m r s : ℕ} {I : Interpretation σ U} [I.IsComplete] :
    complexityModulus I n m (r + s) ≤ complexityModulus I n m r + complexityModulus I n m s

    The modulus is subadditive: ω(r + s) ≤ ω(r) + ω(s).

    source
    theorem Cslib.Circuits.complexityModulus_le_mul {σ : Signature} {U : Type u_1} [Fintype U] [DecidableEq U] {n m r : ℕ} {I : Interpretation σ U} [I.IsComplete] :
    complexityModulus I n m r ≤ r * complexityModulus I n m 1

    The change in complexity is at most ω(1) per changed input.