Sensitivity separation: recursive blocks

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

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

def Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) : Finset ((Fin k × Fin r) × I)

Lift a sensitive block to every column of the specified row.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift i B = Finset.map { toFun := fun (p : Fin r × I) => ((i, p.1), p.2), inj' := ⋯ } (Finset.univ.product B)

@[simp]

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.mem_rowLift {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) (p : (Fin k × Fin r) × I) : p ∈ rowLift i B ↔ p.1.1 = i ∧ p.2 ∈ B

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift_card {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) : (rowLift i B).card = r * B.card

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift_nonempty {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) (hr : 0 < r) (hB : B.Nonempty) : (rowLift i B).Nonempty

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift_disjoint_of_ne {k r : ℕ} {I : Type} (i j : Fin k) (B C : Finset I) (hij : i ≠ j) : Disjoint (rowLift i B) (rowLift j C)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift_disjoint {k r : ℕ} {I : Type} (i j : Fin k) (B C : Finset I) (hBC : Disjoint B C) : Disjoint (rowLift i B) (rowLift j C)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowLift_family_disjoint {k r : ℕ} {I K : Type} (blocks : K → Finset I) (hB : Pairwise fun (a b : K) => Disjoint (blocks a) (blocks b)) : Pairwise fun (a b : Fin k × K) => Disjoint (rowLift a.1 (blocks a.2)) (rowLift b.1 (blocks b.2))

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveChild_rowLift_same {k r : ℕ} {I : Type} (i : Fin k) (B : Finset I) (c : Fin r) : recursiveChild (flip (fun (x : (Fin k × Fin r) × I) => false) (rowLift i B)) i c = flip (fun (x : I) => false) B

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveChild_rowLift_other {k r : ℕ} {I : Type} (i j : Fin k) (B : Finset I) (c : Fin r) (hji : j ≠ i) : recursiveChild (flip (fun (x : (Fin k × Fin r) × I) => false) (rowLift i B)) j c = fun (x : I) => false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily_rowLift {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hzero : ∀ (q : Fin (h + 1)), (F q fun (x : I) => false) = false) (B : Finset I) (hB : ∀ (q : Fin (h + 1)), F q (flip (fun (x : I) => false) B) = true) (i : Fin k) (q : Fin h) : recursiveFamily T label F q (flip (fun (x : (Fin k × Fin r) × I) => false) (rowLift i B)) = true