Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.Tower

Sensitivity separation: tower #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Tower.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.TowerCoordinates (k r : ℕ) (I : Type) :
ℕ → Type

Coordinate type after the specified number of recursive construction levels.

Equations
Instances For
    source
    @[instance_reducible]
    instance Complexity.BooleanAnalysis.Sensitivity.Internal.towerCoordinatesFintype (k r : ℕ) (I : Type) [Fintype I] (n : ℕ) :
    Fintype (TowerCoordinates k r I n)
    Equations
    source
    def Complexity.BooleanAnalysis.Sensitivity.Internal.TowerBlockIndex (k : ℕ) (K : Type) :
    ℕ → Type

    Index type for the disjoint sensitive blocks after each recursive level.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Complexity.BooleanAnalysis.Sensitivity.Internal.towerBlockIndexFintype (k : ℕ) (K : Type) [Fintype K] (n : ℕ) :
      Fintype (TowerBlockIndex k K n)
      Equations
      source
      def Complexity.BooleanAnalysis.Sensitivity.Internal.towerFamily {k r : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (n h : ℕ) :
      Fin h → (TowerCoordinates k r I n → Bool) → Bool

      Iterate the tournament construction, adding a predicate index at each preceding level.

      Equations
      Instances For
        source
        def Complexity.BooleanAnalysis.Sensitivity.Internal.towerBlocks {k r : ℕ} {I K : Type} (blocks : K → Finset I) (n : ℕ) :
        TowerBlockIndex k K n → Finset (TowerCoordinates k r I n)

        Lift the base sensitive blocks through the recursive row products.

        Equations
        Instances For
          source
          def Complexity.BooleanAnalysis.Sensitivity.Internal.baseExtension {I : Type} (D : ℕ) (F : Fin D → (I → Bool) → Bool) (h : ℕ) (q : Fin h) (x : I → Bool) :
          Bool

          Extend a prescribed initial family to unused index counts without adding assumptions.

          Equations
          Instances For
            source
            @[simp]
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.baseExtension_same {I : Type} (D : ℕ) (F : Fin D → (I → Bool) → Bool) :
            baseExtension D F D = F
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.tower_coordinates_card {k r : ℕ} {I : Type} [Fintype I] (n : ℕ) :
            Fintype.card (TowerCoordinates k r I n) = (k * r) ^ n * Fintype.card I
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.tower_block_index_card {k : ℕ} {K : Type} [Fintype K] (n : ℕ) :
            Fintype.card (TowerBlockIndex k K n) = k ^ n * Fintype.card K
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerBlocks_card {k r : ℕ} {I K : Type} (blocks : K → Finset I) (L : ℕ) (hL : ∀ (b : K), (blocks b).card = L) (n : ℕ) (b : TowerBlockIndex k K n) :
            (towerBlocks blocks n b).card = r ^ n * L
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerBlocks_nonempty {k r : ℕ} {I K : Type} (blocks : K → Finset I) (hr : 0 < r) (hne : ∀ (b : K), (blocks b).Nonempty) (n : ℕ) (b : TowerBlockIndex k K n) :
            (towerBlocks blocks n b).Nonempty
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerBlocks_pairwise {k r : ℕ} {I K : Type} (blocks : K → Finset I) (hd : Pairwise fun (a b : K) => Disjoint (blocks a) (blocks b)) (n : ℕ) :
            Pairwise fun (a b : TowerBlockIndex k K n) => Disjoint (towerBlocks blocks n a) (towerBlocks blocks n b)
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerFamily_nested {k r : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (n h : ℕ) (hbase : NestedFamily (base (h + n))) :
            NestedFamily (towerFamily T label base n h)
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerFamily_zero {k r : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (hr : 0 < r) (n h : ℕ) (hbase : ∀ (q : Fin (h + n)), (base (h + n) q fun (x : I) => false) = false) (q : Fin h) :
            (towerFamily T label base n h q fun (x : TowerCoordinates k r I n) => false) = false
            source
            theorem Complexity.BooleanAnalysis.Sensitivity.Internal.towerFamily_blocks {k r : ℕ} {I K : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (base : (h : ℕ) → Fin h → (I → Bool) → Bool) (blocks : K → Finset I) (hr : 0 < r) (n h : ℕ) (hzero : ∀ (q : Fin (h + n)), (base (h + n) q fun (x : I) => false) = false) (hblocks : ∀ (b : K) (q : Fin (h + n)), base (h + n) q (flip (fun (x : I) => false) (blocks b)) = true) (b : TowerBlockIndex k K n) (q : Fin h) :
            towerFamily T label base n h q (flip (fun (x : TowerCoordinates k r I n) => false) (towerBlocks blocks n b)) = true