Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.Reindex

Sensitivity separation: reindex #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Reindex.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.reindex {I J : Type} (e : I ≃ J) (f : (I → Bool) → Bool) :
(J → Bool) → Bool

Transport a Boolean function along an equivalence of its coordinate types.

Equations
Instances For
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_reindex {I J : Type} (e : I ≃ J) (x : J → Bool) (B : Finset I) :
    (fun (i : I) => flip x (Finset.map e.toEmbedding B) (e i)) = flip (fun (i : I) => x (e i)) B
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.flip_reindex_singleton {I J : Type} (e : I ≃ J) (x : J → Bool) (i : I) :
    (fun (a : I) => flip x {e i} (e a)) = flip (fun (a : I) => x (e a)) {i}
    source
    @[simp]
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.reindex_symm {I J : Type} (e : I ≃ J) (f : (I → Bool) → Bool) :
    reindex e.symm (reindex e f) = f
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivityAt_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) (x : J → Bool) :
    sensitivityAt (reindex e f) x = sensitivityAt f fun (i : I) => x (e i)
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) :
    sensitivity (reindex e f) = sensitivity f
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_le_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) (x : J → Bool) :
    (blockSensitivityAt f fun (i : I) => x (e i)) ≤ blockSensitivityAt (reindex e f) x
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) (x : J → Bool) :
    blockSensitivityAt (reindex e f) x = blockSensitivityAt f fun (i : I) => x (e i)
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivity_reindex {I J : Type} [Fintype I] [Fintype J] (e : I ≃ J) (f : (I → Bool) → Bool) :
    blockSensitivity (reindex e f) = blockSensitivity f