Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.FixedCoordinates

Sensitivity separation: fixed coordinates #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/FixedCoordinates.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.fixedCoordinatesEquiv {α β : Type} [DecidableEq α] (s : Finset α) (v : α → β) :
{ f : α → β // ∀ i ∈ s, f i = v i } ≃ ({ i : α // i ∉ s } → β)

Functions with prescribed coordinates are equivalent to functions on the remaining coordinates.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.card_fixedCoordinates {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] (s : Finset α) (v : α → β) [DecidablePred fun (f : α → β) => ∀ i ∈ s, f i = v i] :
    {f : α → β | ∀ i ∈ s, f i = v i}.card = Fintype.card β ^ (Fintype.card α - s.card)