Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Defs

Sensitivity separation: model #

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

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

source
noncomputable def Complexity.BooleanAnalysis.Sensitivity.flip {I : Type} (x : I → Bool) (B : Finset I) :
I → Bool

Flip exactly the coordinates belonging to the specified block.

Equations
Instances For
    source
    noncomputable def Complexity.BooleanAnalysis.Sensitivity.sensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) :
    ℕ

    The ordinary number of sensitive individual input coordinates.

    Equations
    Instances For
      source
      noncomputable def Complexity.BooleanAnalysis.Sensitivity.sensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) :
      ℕ

      Maximum ordinary sensitivity over all Boolean inputs.

      Equations
      Instances For
        source
        noncomputable def Complexity.BooleanAnalysis.Sensitivity.blockSensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) :
        ℕ

        Maximum size of a family of disjoint nonempty sensitive blocks at an input. The empty family is allowed and contributes zero. Invalid families contribute zero.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Complexity.BooleanAnalysis.Sensitivity.blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) :
          ℕ

          Maximum block sensitivity over all Boolean inputs.

          Equations
          Instances For