Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.HammingBase

Sensitivity separation: hamming base #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/HammingBase.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.hammingDist_flip_self {I : Type} [Fintype I] (x : I → Bool) (i : I) :
hammingDist x (flip x {i}) = 1
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.hammingDist_le_flip_add_one {I : Type} [Fintype I] (x z : I → Bool) (i : I) :
hammingDist x z ≤ hammingDist (flip x {i}) z + 1
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.hammingDist_flip_le_add_one {I : Type} [Fintype I] (x z : I → Bool) (i : I) :
hammingDist (flip x {i}) z ≤ hammingDist x z + 1
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.hammingDist_flip_eq_add_one {I : Type} [Fintype I] (x z : I → Bool) (i : I) (hi : x i = z i) :
hammingDist (flip x {i}) z = hammingDist x z + 1
source
def Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) :
Bool

The union of equal-radius Hamming balls.

Equations
Instances For
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_eq_true {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) :
    ballPredicate centers R x = true ↔ ∃ (c : C), hammingDist x (centers c) ≤ R
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_nested {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) {R S : ℕ} (hRS : R ≤ S) (x : I → Bool) (h : ballPredicate centers R x = true) :
    ballPredicate centers S x = true
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_zero_flip {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) (i : I) (hx : ballPredicate centers R x = false) (hi : ballPredicate centers R (flip x {i}) = true) :
    ∃ (c : C), hammingDist x (centers c) = R + 1 ∧ x i ≠ centers c i
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.near_center_unique {I C : Type} [Fintype I] (centers : C → I → Bool) (R : ℕ) (hsep : ∀ (a b : C), a ≠ b → 2 * (R + 1) < hammingDist (centers a) (centers b)) (x : I → Bool) {a b : C} (ha : hammingDist x (centers a) ≤ R + 1) (hb : hammingDist x (centers b) ≤ R + 1) :
    a = b
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_sensitivityAt_zero_le {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) (R : ℕ) (hsep : ∀ (a b : C), a ≠ b → 2 * (R + 1) < hammingDist (centers a) (centers b)) (x : I → Bool) (hx : ballPredicate centers R x = false) :
    sensitivityAt (ballPredicate centers R) x ≤ R + 1
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_no_joint_zero {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) {R S : ℕ} (hRS : R < S) (x : I → Bool) (i : I) (hS : ballPredicate centers S x = false) (hR : ballPredicate centers R (flip x {i}) = true) :
    False
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_no_joint_one {I C : Type} [Fintype I] [Fintype C] (centers : C → I → Bool) {R S : ℕ} (hRS : R < S) (x : I → Bool) (i : I) (hR : ballPredicate centers R x = true) (hS : ballPredicate centers S (flip x {i}) = false) :
    False
    source
    def Complexity.BooleanAnalysis.Sensitivity.Internal.nearestDistance {I C : Type} [Fintype I] [Fintype C] [Nonempty C] (centers : C → I → Bool) (x : I → Bool) :
    ℕ

    Minimum distance to the finite nonempty family of centers.

    Equations
    Instances For
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ballPredicate_eq_nearestDistance {I C : Type} [Fintype I] [Fintype C] [Nonempty C] (centers : C → I → Bool) (R : ℕ) (x : I → Bool) :
      ballPredicate centers R x = decide (nearestDistance centers x ≤ R)
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.nearestDistance_le_flip_add_one {I C : Type} [Fintype I] [Fintype C] [Nonempty C] (centers : C → I → Bool) (x : I → Bool) (i : I) :
      nearestDistance centers x ≤ nearestDistance centers (flip x {i}) + 1