Superquadratic sensitivity separation: fixed coordinates

This file counts the functions α → β between finite types that agree with a given function v on a prescribed finset s of coordinates, via an explicit equivalence with the functions on the complement of s. The resulting exact count is used to compute the sizes of labeling events in which some labels are prescribed.

Main definitions

• fixedCoordinatesEquiv: functions agreeing with v on s are equivalent to functions on the coordinates outside s.

Main results

• card_fixedCoordinates: there are Fintype.card β ^ (Fintype.card α - s.card) functions α → β that agree with v on s.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/FixedCoordinates.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.QueryComplexity.SensitivitySeparation.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.

theorem Cslib.QueryComplexity.SensitivitySeparation.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)

The number of functions α → β agreeing with v on s is Fintype.card β ^ (Fintype.card α - s.card).