Finite Boolean dependency tables -- proof internals

theorem Complexity.BooleanDependency.uniformProbability_restrict_internal {coordinate : Type u_1} [Fintype coordinate] [DecidableEq coordinate] (coordinates : Finset coordinate) (event : (↥coordinates → Bool) → Prop) [DecidablePred event] : uniformProbability {input : coordinate → Bool | event (restrict coordinates input)} = uniformProbability (Finset.filter event Finset.univ)

theorem Complexity.BooleanDependency.extendByFalse_restrict_apply_internal {coordinate : Type u_1} [DecidableEq coordinate] (coordinates : Finset coordinate) (input : coordinate → Bool) (index : coordinate) (hindex : index ∈ coordinates) : extendByFalse coordinates (restrict coordinates input) index = input index

theorem Complexity.BooleanDependency.table_restrict_internal {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) (hdepends : DependsOn function ↑coordinates) (input : coordinate → Bool) : table coordinates function (restrict coordinates input) = function input

theorem Complexity.BooleanDependency.card_assignments_internal {coordinate : Type u_1} (coordinates : Finset coordinate) : Nat.card (↥coordinates → Bool) = 2 ^ coordinates.card

theorem Complexity.BooleanDependency.finite_range_of_dependsOn_internal {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) (hdepends : DependsOn function ↑coordinates) : (Set.range function).Finite

theorem Complexity.BooleanDependency.card_range_le_pow_card_of_dependsOn_internal {coordinate : Type u_1} {result : Type u_2} [DecidableEq coordinate] (coordinates : Finset coordinate) (function : (coordinate → Bool) → result) (hdepends : DependsOn function ↑coordinates) : Nat.card ↑(Set.range function) ≤ 2 ^ coordinates.card