Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.InitialPredicates

Sensitivity separation: initial predicates #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/InitialPredicates.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.blockCenter {M L : ℕ} (j : Fin M) :
Fin M × Fin L → Bool

The Boolean input supported on one row of the base coordinate product.

Equations
Instances For
    source
    def Complexity.BooleanAnalysis.Sensitivity.Internal.baseBlock {M L : ℕ} (j : Fin M) :
    Finset (Fin M × Fin L)

    The coordinates in one row of the base coordinate product.

    Equations
    Instances For
      source
      @[simp]
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.mem_baseBlock {M L : ℕ} (j : Fin M) (p : Fin M × Fin L) :
      p ∈ baseBlock j ↔ p.1 = j
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.baseBlock_card {M L : ℕ} (j : Fin M) :
      (baseBlock j).card = L
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.baseBlock_nonempty {M L : ℕ} (hL : 0 < L) (j : Fin M) :
      (baseBlock j).Nonempty
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.baseBlock_disjoint {M L : ℕ} :
      Pairwise fun (i j : Fin M) => Disjoint (baseBlock i) (baseBlock j)
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_zero_baseBlock {M L : ℕ} (j : Fin M) :
      flip (fun (x : Fin M × Fin L) => false) (baseBlock j) = blockCenter j
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.hammingDist_zero_blockCenter {M L : ℕ} (j : Fin M) :
      hammingDist (fun (x : Fin M × Fin L) => false) (blockCenter j) = L
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.hammingDist_blockCenter {M L : ℕ} (i j : Fin M) (hij : i ≠ j) :
      hammingDist (blockCenter i) (blockCenter j) = 2 * L
      source
      def Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily (d M : ℕ) :
      Fin (d + 1) → (Fin M × Fin (d + 2) → Bool) → Bool

      Nested unions of Hamming balls around the disjoint row centers.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily_nested (d M : ℕ) :
        NestedFamily (initialFamily d M)
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily_zero (d M : ℕ) (q : Fin (d + 1)) :
        (initialFamily d M q fun (x : Fin M × Fin (d + 2)) => false) = false
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily_baseBlock (d M : ℕ) (q : Fin (d + 1)) (j : Fin M) :
        initialFamily d M q (flip (fun (x : Fin M × Fin (d + 2)) => false) (baseBlock j)) = true
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily_side_zero (d M : ℕ) :
        sideSensitivity (initialFamily d M) false ≤ d + 2
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily_side_one (d M : ℕ) :
        sideSensitivity (initialFamily d M) true ≤ (d + 2) * M
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.initialFamily_joint (d M : ℕ) (b : Bool) :
        jointSensitivity (initialFamily d M) b = 0
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.nearestDistance_blockCenter_zero (M L : ℕ) [NeZero M] :
        (nearestDistance blockCenter fun (x : Fin M × Fin L) => false) = L