Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.Or

Sensitivity separation: or #

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

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

source
def Complexity.BooleanAnalysis.Sensitivity.Internal.orBits {K : Type} [Fintype K] (x : K → Bool) :
Bool

Disjunction of a finite family of Boolean values.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.orBits_eq_true {K : Type} [Fintype K] (x : K → Bool) :
    orBits x = true ↔ ∃ (k : K), x k = true
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.orBits_eq_false {K : Type} [Fintype K] (x : K → Bool) :
    orBits x = false ↔ ∀ (k : K), x k = false
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.orBits_zero {K : Type} [Fintype K] :
    (orBits fun (x : K) => false) = false
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.orBits_flip_of_witness {K : Type} [Fintype K] (x : K → Bool) {i j : K} (hji : j ≠ i) (hj : x j = true) :
    orBits (flip x {i}) = orBits x
    source
    def Complexity.BooleanAnalysis.Sensitivity.Internal.orCopies {I K : Type} [Fintype K] (f : (I → Bool) → Bool) :
    (K × I → Bool) → Bool

    Disjunction of independent copies of a Boolean function.

    Equations
    Instances For
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.orCopies_zero {I K : Type} [Fintype K] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) :
      (orCopies f fun (x : K × I) => false) = false
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_orCopies_le {I K : Type} [Fintype K] [Fintype I] (f : (I → Bool) → Bool) (S₀ S₁ : ℕ) (h₀ : ∀ (x : I → Bool), f x = false → sensitivityAt f x ≤ S₀) (h₁ : ∀ (x : I → Bool), f x = true → sensitivityAt f x ≤ S₁) :
      sensitivity (orCopies f) ≤ max (Fintype.card K * S₀) S₁
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.card_le_blockSensitivityAt_orBits_zero {K : Type} [Fintype K] :
      Fintype.card K ≤ blockSensitivityAt orBits fun (x : K) => false
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_orCopies_zero {I K : Type} [Fintype K] [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) :
      (Fintype.card K * blockSensitivityAt f fun (x : I) => false) ≤ blockSensitivityAt (orCopies f) fun (x : K × I) => false