Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.Iterates

Sensitivity separation: iterates #

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

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

source
@[reducible, inline]
abbrev Complexity.BooleanAnalysis.Sensitivity.Internal.IterateCoord (I : Type) :
ℕ → Type

Coordinates of an iterated block composition, starting with a singleton.

Equations
Instances For
    source
    @[instance_reducible]
    instance Complexity.BooleanAnalysis.Sensitivity.Internal.iterateCoordFintype {I : Type} [Fintype I] (m : ℕ) :
    Fintype (IterateCoord I m)
    Equations
    source
    def Complexity.BooleanAnalysis.Sensitivity.Internal.iterateCompose {I : Type} (f : (I → Bool) → Bool) (m : ℕ) :
    (IterateCoord I m → Bool) → Bool

    Repeated block composition of a Boolean function.

    Equations
    Instances For
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.iterateCompose_one {I : Type} (f : (I → Bool) → Bool) (x : IterateCoord I 1 → Bool) :
      iterateCompose f 1 x = f fun (i : I) => x (i, ())
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.iterateCompose_zero {I : Type} (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (m : ℕ) :
      (iterateCompose f m fun (x : IterateCoord I m) => false) = false
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.iterateCoord_card {I : Type} [Fintype I] (m : ℕ) :
      Fintype.card (IterateCoord I m) = Fintype.card I ^ m
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_iterateCompose_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) (m : ℕ) :
      sensitivity (iterateCompose f m) ≤ sensitivity f ^ m
      source
      theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_iterateCompose_zero {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (m : ℕ) :
      (blockSensitivityAt f fun (x : I) => false) ^ m ≤ blockSensitivityAt (iterateCompose f m) fun (x : IterateCoord I m) => false
      source
      noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.iterateFin {I : Type} [Fintype I] (f : (I → Bool) → Bool) (m : ℕ) :
      (Fin (Fintype.card I ^ m) → Bool) → Bool

      Reindex the iterated composition onto a finite ordinal.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.iterateFin_zero {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (m : ℕ) :
        (iterateFin f m fun (x : Fin (Fintype.card I ^ m)) => false) = false
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.sensitivity_iterateFin_le {I : Type} [Fintype I] (f : (I → Bool) → Bool) (m : ℕ) :
        sensitivity (iterateFin f m) ≤ sensitivity f ^ m
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.blockSensitivityAt_iterateFin_zero {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (m : ℕ) :
        (blockSensitivityAt f fun (x : I) => false) ^ m ≤ blockSensitivityAt (iterateFin f m) fun (x : Fin (Fintype.card I ^ m)) => false
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.nonconstant_of_blockSensitivityAt_pos {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) (h : 0 < blockSensitivityAt f x) :
        ∃ (y : I → Bool) (z : I → Bool), f y ≠ f z
        source
        theorem Complexity.BooleanAnalysis.Sensitivity.Internal.iterateFin_nonconstant {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (h : 0 < blockSensitivityAt f fun (x : I) => false) (m : ℕ) :
        ∃ (x : Fin (Fintype.card I ^ m) → Bool) (y : Fin (Fintype.card I ^ m) → Bool), iterateFin f m x ≠ iterateFin f m y