diff --git a/Complexity/Computability/DecisionTree/Certificate.lean b/Complexity/Computability/DecisionTree/Certificate.lean index 351e980e97..a54f4c028c 100644 --- a/Complexity/Computability/DecisionTree/Certificate.lean +++ b/Complexity/Computability/DecisionTree/Certificate.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.DecisionTree.Sensitivity +public import Complexity.Computability.QueryComplexity.OneSided /-! # Decision trees from certificates @@ -21,11 +22,6 @@ value `b` (`complexity_le_certificateComplexityFor_mul`) [BlumImpagliazzo1987], [Jukna, Section 14.2][Jukna2012]. In particular, decision tree complexity is at most the square of certificate complexity. -## Main definitions - -* `Cslib.QueryComplexity.certificateComplexityFor`: the certificate complexity `C_b(f)` of the - inputs where `f` has value `b`. - ## Main results * `Cslib.DecisionTree.complexity_le_card_add`: querying a set of variables and continuing with @@ -97,19 +93,6 @@ end DecisionTree namespace QueryComplexity -/-- `C_b(f)`: the largest certificate complexity of `f` at an input where it has value `b`. -/ -def certificateComplexityFor (f : BooleanFunction n) (b : Bool) : ℕ := - (univ.filter fun x => f x = b).sup (certificateComplexityAt f) - -theorem certificateComplexityAt_le_certificateComplexityFor {f : BooleanFunction n} - {x : BitString n} {b : Bool} (h : f x = b) : - certificateComplexityAt f x ≤ certificateComplexityFor f b := - le_sup (f := certificateComplexityAt f) (mem_filter.2 ⟨mem_univ x, h⟩) - -theorem certificateComplexityFor_le_certificateComplexity (f : BooleanFunction n) (b : Bool) : - certificateComplexityFor f b ≤ certificateComplexity f := - sup_mono (filter_subset _ _) - /-- Restricting by answers on `S` does not lengthen certificates: every certificate for the function restricted by `a` at `z` is at most as long as a certificate of `f` at the filled input, minus its variables in `S`. -/ diff --git a/Complexity/Computability/DecisionTree/Parity.lean b/Complexity/Computability/DecisionTree/Parity.lean index 1a193af61b..5b5b0b98e5 100644 --- a/Complexity/Computability/DecisionTree/Parity.lean +++ b/Complexity/Computability/DecisionTree/Parity.lean @@ -7,24 +7,22 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Foundations.Data.BitString.PartialAssignment -public import Complexity.Foundations.Data.BitString.Parity public import Complexity.Computability.DecisionTree.Sensitivity +public import Complexity.Computability.QueryComplexity.Threshold +public import Complexity.Foundations.Data.BitString.PartialAssignment /-! # Decision trees for parity Flipping any bit flips the parity, so parity is sensitive to every bit at every input -(`sensitivityAt_parity`). Its sensitivity, block sensitivity, certificate complexity and decision -tree complexity therefore all equal the number of bits [Jukna, Chapter 14][Jukna2012]. +(`BitString.sensitivityAt_parity`), and every decision tree for it queries all of its bits in the +worst case (`DecisionTree.complexity_parity`) [Jukna, Chapter 14][Jukna2012]. More generally, +restricted parity queries every free bit (`DecisionTree.card_free_le_complexity_parity_fill`). ## Main results * `Cslib.DecisionTree.complexity_parity`: the decision tree complexity of the parity of `n` bits is `n`. -* `Cslib.BitString.sensitivity_parity`, `Cslib.QueryComplexity.blockSensitivity_parity`, - `Cslib.QueryComplexity.certificateComplexity_parity`: so are its sensitivity, block sensitivity - and certificate complexity. * `Cslib.DecisionTree.card_free_le_complexity_parity_fill`: restricted parity still needs to query every free bit. @@ -41,38 +39,6 @@ open Finset BitString QueryComplexity variable {n : ℕ} -namespace BitString - -/-- Parity is sensitive to every bit at every input. -/ -theorem sensitivityAt_parity (x : BitString n) : sensitivityAt (parity n) x = n := by - have : (univ.filter fun i => parity n (Function.update x i !x i) ≠ parity n x) = univ := by - refine eq_univ_of_forall fun i => mem_filter.2 ⟨mem_univ i, ?_⟩ - rw [parity, parityOn_update_not (mem_univ i)] - cases parityOn univ x <;> decide - change #(univ.filter fun i => parity n (Function.update x i !x i) ≠ parity n x) = n - rw [this, card_univ, Fintype.card_fin] - -/-- The sensitivity of parity is its number of coordinates. -/ -theorem sensitivity_parity : sensitivity (parity n) = n := - le_antisymm (sensitivity_le_card _) ((sensitivityAt_parity (fun _ => false)).symm.trans_le - (sensitivityAt_le_sensitivity _ _)) - -end BitString - -namespace QueryComplexity - -/-- The block sensitivity of parity is its number of coordinates. -/ -theorem blockSensitivity_parity : blockSensitivity (parity n) = n := - le_antisymm (blockSensitivity_le_card _) - (sensitivity_parity.symm.trans_le (sensitivity_le_blockSensitivity _)) - -/-- The certificate complexity of parity is its number of coordinates. -/ -theorem certificateComplexity_parity : certificateComplexity (parity n) = n := - le_antisymm (certificateComplexity_le_card _) - (blockSensitivity_parity.symm.trans_le (blockSensitivity_le_certificateComplexity _)) - -end QueryComplexity - namespace DecisionTree /-- Every decision tree for the parity of `n` bits queries all of them in the worst case. -/ diff --git a/Complexity/Computability/QueryComplexity/Monotone.lean b/Complexity/Computability/QueryComplexity/Monotone.lean index 96e4097b42..12f23389b4 100644 --- a/Complexity/Computability/QueryComplexity/Monotone.lean +++ b/Complexity/Computability/QueryComplexity/Monotone.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.DecisionTree.Certificate public import Complexity.Computability.QueryComplexity.OneSided public import Complexity.Foundations.Data.BitString.Weight diff --git a/Complexity/Computability/QueryComplexity/OneSided.lean b/Complexity/Computability/QueryComplexity/OneSided.lean index 4f65221057..fe04bd4830 100644 --- a/Complexity/Computability/QueryComplexity/OneSided.lean +++ b/Complexity/Computability/QueryComplexity/OneSided.lean @@ -7,26 +7,29 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.DecisionTree.Restrict -public import Complexity.Computability.QueryComplexity.Relations +public import Cslib.Computability.QueryComplexity.Measures /-! -# One-sided measures and negation +# One-sided query complexity measures and negation For a value `b`, the one-sided measures `s_b(f)`, `bs_b(f)` and `C_b(f)` are the largest -sensitivity, block sensitivity and certificate complexity of `f` at an input of value `b`. +sensitivity, block sensitivity and certificate complexity of `f` at an input of value `b` +(`BitString.sensitivityFor`, `QueryComplexity.blockSensitivityFor`, +`QueryComplexity.certificateComplexityFor`) [BuhrmanDeWolf2002]. + Negation keeps sensitive coordinates, sensitive blocks and certificates, so it preserves `s`, `bs` and `C` and exchanges the two values of the one-sided measures (`BitString.sensitivityFor_not`, `QueryComplexity.blockSensitivityFor_not`, `QueryComplexity.certificateComplexityFor_not`). -With `D(¬f) = D(f)` this turns the bound `D(f) ≤ bs₀(f) C₁(f)`, a one-sided form of the bound -`D(f) ≤ C₁(f) bs(f)` of [BealsBuhrmanCleveMoscaDeWolf2001], into its dual `D(f) ≤ bs₁(f) C₀(f)` -(`DecisionTree.complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor`), hence -`D(f) ≤ min(C₀(f), C₁(f)) bs(f)`. With the one-sided form `C_b(f) ≤ s_{¬b}(f) bs_b(f)` of Nisan's -bound [Nisan1991] -(`QueryComplexity.certificateComplexityFor_le_sensitivityFor_mul_blockSensitivityFor`) it gives -`D(f) ≤ bs_{¬b}(f) s_{¬b}(f) bs_b(f)`, in particular `D(f) ≤ bs₀(f) bs₁(f) s(f)`. +## Main definitions + +* `Cslib.BitString.sensitivityFor`: the sensitivity `s_b(f)` of the inputs where `f` has value + `b`. +* `Cslib.QueryComplexity.blockSensitivityFor`: the block sensitivity `bs_b(f)` of the inputs + where `f` has value `b`. +* `Cslib.QueryComplexity.certificateComplexityFor`: the certificate complexity `C_b(f)` of the + inputs where `f` has value `b`. ## Main results @@ -35,20 +38,9 @@ bound [Nisan1991] * `Cslib.BitString.sensitivityFor_not`, `Cslib.QueryComplexity.blockSensitivityFor_not`, `Cslib.QueryComplexity.certificateComplexityFor_not`: negation exchanges the two values of the one-sided measures. -* `Cslib.DecisionTree.complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor`: - `D(f) ≤ bs_{¬b}(f) C_b(f)`. -* `Cslib.DecisionTree.complexity_le_min_certificateComplexityFor_mul_blockSensitivity`: - `D(f) ≤ min(C₀(f), C₁(f)) bs(f)`. -* `Cslib.DecisionTree.complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor`: - `D(f) ≤ bs_{¬b}(f) s_{¬b}(f) bs_b(f)`. -* `Cslib.DecisionTree.complexity_le_blockSensitivityFor_mul_blockSensitivityFor_mul_sensitivity`: - `D(f) ≤ bs₀(f) bs₁(f) s(f)`. ## References -* [N. Nisan, *CREW PRAMs and decision trees*][Nisan1991] -* [R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, *Quantum lower bounds by - polynomials*][BealsBuhrmanCleveMoscaDeWolf2001] * [H. Buhrman, R. de Wolf, *Complexity measures and decision tree complexity: a survey*][BuhrmanDeWolf2002] -/ @@ -69,6 +61,20 @@ private theorem filter_not_eq (f : BooleanFunction n) (b : Bool) : namespace BitString +/-- `s_b(f)`: the largest sensitivity of `f` at an input where it has value `b`. -/ +def sensitivityFor (f : BooleanFunction n) (b : Bool) : ℕ := + (univ.filter fun x => f x = b).sup (sensitivityAt f) + +/-- The sensitivity at an input of value `b` is at most `s_b(f)`. -/ +theorem sensitivityAt_le_sensitivityFor {f : BooleanFunction n} {x : BitString n} + {b : Bool} (h : f x = b) : sensitivityAt f x ≤ sensitivityFor f b := + le_sup (f := sensitivityAt f) (mem_filter.2 ⟨mem_univ x, h⟩) + +/-- `s_b(f) ≤ s(f)`. -/ +theorem sensitivityFor_le_sensitivity (f : BooleanFunction n) (b : Bool) : + sensitivityFor f b ≤ sensitivity f := + sup_mono (filter_subset _ _) + /-- Negating a function keeps its sensitive coordinates. -/ @[simp] theorem isSensitiveCoord_not {f : BooleanFunction n} {x : BitString n} {i : Fin n} : @@ -101,6 +107,34 @@ namespace QueryComplexity variable {f : BooleanFunction n} {x : BitString n} +/-- `bs_b(f)`: the largest block sensitivity of `f` at an input where it has value `b`. -/ +def blockSensitivityFor (f : BooleanFunction n) (b : Bool) : ℕ := + (univ.filter fun x => f x = b).sup (blockSensitivityAt f) + +/-- The block sensitivity at an input of value `b` is at most `bs_b(f)`. -/ +theorem blockSensitivityAt_le_blockSensitivityFor {b : Bool} (h : f x = b) : + blockSensitivityAt f x ≤ blockSensitivityFor f b := + le_sup (f := blockSensitivityAt f) (mem_filter.2 ⟨mem_univ x, h⟩) + +/-- `bs_b(f) ≤ bs(f)`. -/ +theorem blockSensitivityFor_le_blockSensitivity (f : BooleanFunction n) (b : Bool) : + blockSensitivityFor f b ≤ blockSensitivity f := + sup_mono (filter_subset _ _) + +/-- `C_b(f)`: the largest certificate complexity of `f` at an input where it has value `b`. -/ +def certificateComplexityFor (f : BooleanFunction n) (b : Bool) : ℕ := + (univ.filter fun x => f x = b).sup (certificateComplexityAt f) + +/-- The certificate complexity at an input of value `b` is at most `C_b(f)`. -/ +theorem certificateComplexityAt_le_certificateComplexityFor {b : Bool} (h : f x = b) : + certificateComplexityAt f x ≤ certificateComplexityFor f b := + le_sup (f := certificateComplexityAt f) (mem_filter.2 ⟨mem_univ x, h⟩) + +/-- `C_b(f) ≤ C(f)`. -/ +theorem certificateComplexityFor_le_certificateComplexity (f : BooleanFunction n) (b : Bool) : + certificateComplexityFor f b ≤ certificateComplexity f := + sup_mono (filter_subset _ _) + /-- Negating a function keeps its sensitive blocks. -/ @[simp] theorem isSensitiveBlock_not {B : Block n} : @@ -152,58 +186,4 @@ theorem certificateComplexityFor_not (f : BooleanFunction n) (b : Bool) : end QueryComplexity -namespace DecisionTree - -open QueryComplexity - -/-- **Decision tree complexity from one-sided measures**: `D(f) ≤ bs_{¬b}(f) C_b(f)` for either -value `b`. For `b = 1` this is `D(f) ≤ bs₀(f) C₁(f)`, a one-sided form of the bound of Beals, -Buhrman, Cleve, Mosca and de Wolf [BealsBuhrmanCleveMoscaDeWolf2001]; negating the function gives -the dual `D(f) ≤ bs₁(f) C₀(f)`. -/ -theorem complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor - (f : BooleanFunction n) (b : Bool) : - complexity f ≤ blockSensitivityFor f (!b) * certificateComplexityFor f b := by - cases b with - | false => - have := complexity_le_blockSensitivityFor_mul_certificateComplexityFor (fun y => !f y) - rwa [complexity_not, blockSensitivityFor_not, certificateComplexityFor_not] at this - | true => exact complexity_le_blockSensitivityFor_mul_certificateComplexityFor f - -/-- `D(f) ≤ C_b(f) bs(f)` for either value `b` [BealsBuhrmanCleveMoscaDeWolf2001]. -/ -theorem complexity_le_certificateComplexityFor_mul_blockSensitivity (f : BooleanFunction n) - (b : Bool) : complexity f ≤ certificateComplexityFor f b * blockSensitivity f := - (complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor f b).trans (by - rw [mul_comm] - exact Nat.mul_le_mul_left _ (blockSensitivityFor_le_blockSensitivity f _)) - -/-- `D(f) ≤ min(C₀(f), C₁(f)) bs(f)`. -/ -theorem complexity_le_min_certificateComplexityFor_mul_blockSensitivity (f : BooleanFunction n) : - complexity f ≤ - min (certificateComplexityFor f false) (certificateComplexityFor f true) * - blockSensitivity f := by - rcases min_choice (certificateComplexityFor f false) (certificateComplexityFor f true) with h | h - all_goals - rw [h] - exact complexity_le_certificateComplexityFor_mul_blockSensitivity f _ - -/-- `D(f) ≤ bs_{¬b}(f) s_{¬b}(f) bs_b(f)`, from `D(f) ≤ bs_{¬b}(f) C_b(f)` and the one-sided Nisan -bound. -/ -theorem complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor - (f : BooleanFunction n) (b : Bool) : - complexity f ≤ blockSensitivityFor f (!b) * sensitivityFor f (!b) * blockSensitivityFor f b := - (complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor f b).trans - ((Nat.mul_le_mul_left _ - (certificateComplexityFor_le_sensitivityFor_mul_blockSensitivityFor f b)).trans_eq - (Nat.mul_assoc _ _ _).symm) - -/-- `D(f) ≤ bs₀(f) bs₁(f) s(f)`. -/ -theorem complexity_le_blockSensitivityFor_mul_blockSensitivityFor_mul_sensitivity - (f : BooleanFunction n) : - complexity f ≤ blockSensitivityFor f false * blockSensitivityFor f true * sensitivity f := - (complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor f true).trans (by - rw [Nat.mul_right_comm] - exact Nat.mul_le_mul_left _ (sensitivityFor_le_sensitivity f _)) - -end DecisionTree - end Cslib diff --git a/Complexity/Computability/QueryComplexity/Relations.lean b/Complexity/Computability/QueryComplexity/Relations.lean index ddc520276d..c1aa21fcce 100644 --- a/Complexity/Computability/QueryComplexity/Relations.lean +++ b/Complexity/Computability/QueryComplexity/Relations.lean @@ -8,6 +8,8 @@ module -- upstream: candidate public import Complexity.Computability.DecisionTree.Certificate +public import Complexity.Computability.DecisionTree.Restrict +public import Complexity.Computability.QueryComplexity.OneSided /-! # Relations between block sensitivity, certificate and decision tree complexity @@ -35,17 +37,14 @@ of `f` at an input of value `b`. certificate on which it differs from the input of value `1`, so its block sensitivity has dropped. -With `C(f) ≤ s(f) bs(f) ≤ bs(f)²` this gives `D(f) ≤ s(f) bs(f)² ≤ bs(f)³` +With `D(¬f) = D(f)` this turns `D(f) ≤ bs₀(f) C₁(f)` into its dual `D(f) ≤ bs₁(f) C₀(f)` +(`DecisionTree.complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor`), hence +`D(f) ≤ min(C₀(f), C₁(f)) bs(f)`, and with the one-sided Nisan bound it gives +`D(f) ≤ bs_{¬b}(f) s_{¬b}(f) bs_b(f)`, in particular `D(f) ≤ bs₀(f) bs₁(f) s(f)`. +With `C(f) ≤ s(f) bs(f) ≤ bs(f)²` it gives `D(f) ≤ s(f) bs(f)² ≤ bs(f)³` (`DecisionTree.complexity_le_sensitivity_mul_blockSensitivity_sq`, `DecisionTree.complexity_le_blockSensitivity_pow_three`; [BuhrmanDeWolf2002], Corollary 1). -## Main definitions - -* `Cslib.BitString.sensitivityFor`: the sensitivity `s_b(f)` of the inputs where `f` has value - `b`. -* `Cslib.QueryComplexity.blockSensitivityFor`: the block sensitivity `bs_b(f)` of the inputs - where `f` has value `b`. - ## Main results * `Cslib.QueryComplexity.certificateComplexityAt_le_sensitivityFor_mul_blockSensitivityAt`: @@ -59,6 +58,14 @@ With `C(f) ≤ s(f) bs(f) ≤ bs(f)²` this gives `D(f) ≤ s(f) bs(f)² ≤ bs( * `Cslib.QueryComplexity.certificateComplexity_le_blockSensitivity_sq`: `C(f) ≤ bs(f)²`. * `Cslib.DecisionTree.complexity_le_blockSensitivityFor_mul_certificateComplexityFor`: `D(f) ≤ bs₀(f) C₁(f)`. +* `Cslib.DecisionTree.complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor`: + `D(f) ≤ bs_{¬b}(f) C_b(f)`. +* `Cslib.DecisionTree.complexity_le_min_certificateComplexityFor_mul_blockSensitivity`: + `D(f) ≤ min(C₀(f), C₁(f)) bs(f)`. +* `Cslib.DecisionTree.complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor`: + `D(f) ≤ bs_{¬b}(f) s_{¬b}(f) bs_b(f)`. +* `Cslib.DecisionTree.complexity_le_blockSensitivityFor_mul_blockSensitivityFor_mul_sensitivity`: + `D(f) ≤ bs₀(f) bs₁(f) s(f)`. * `Cslib.DecisionTree.complexity_le_certificateComplexity_mul_blockSensitivity`: `D(f) ≤ C(f) bs(f)`. * `Cslib.DecisionTree.complexity_le_sensitivity_mul_blockSensitivity_sq`: `D(f) ≤ s(f) bs(f)²`. @@ -90,22 +97,6 @@ private theorem BitString.flipBlock_filter_ne (x y : BitString n) : flipBlock · rw [flipBlock_apply_of_mem (by simpa using h)] cases hx : x i <;> cases hy : y i <;> simp_all -/-! ### One-sided sensitivity -/ - -/-- `s_b(f)`: the largest sensitivity of `f` at an input where it has value `b`. -/ -def BitString.sensitivityFor (f : BooleanFunction n) (b : Bool) : ℕ := - (univ.filter fun x => f x = b).sup (sensitivityAt f) - -/-- The sensitivity at an input of value `b` is at most `s_b(f)`. -/ -theorem BitString.sensitivityAt_le_sensitivityFor {f : BooleanFunction n} {x : BitString n} - {b : Bool} (h : f x = b) : sensitivityAt f x ≤ sensitivityFor f b := - le_sup (f := sensitivityAt f) (mem_filter.2 ⟨mem_univ x, h⟩) - -/-- `s_b(f) ≤ s(f)`. -/ -theorem BitString.sensitivityFor_le_sensitivity (f : BooleanFunction n) (b : Bool) : - sensitivityFor f b ≤ sensitivity f := - sup_mono (filter_subset _ _) - namespace QueryComplexity variable {f : BooleanFunction n} {x : BitString n} @@ -210,20 +201,6 @@ theorem certificateComplexity_le_blockSensitivity_sq (f : BooleanFunction n) : rw [sq] exact Nat.mul_le_mul_right _ (sensitivity_le_blockSensitivity f)) -/-! ### Block sensitivity for a value -/ - -/-- `bs_b(f)`: the largest block sensitivity of `f` at an input where it has value `b`. -/ -def blockSensitivityFor (f : BooleanFunction n) (b : Bool) : ℕ := - (univ.filter fun x => f x = b).sup (blockSensitivityAt f) - -theorem blockSensitivityAt_le_blockSensitivityFor {b : Bool} (h : f x = b) : - blockSensitivityAt f x ≤ blockSensitivityFor f b := - le_sup (f := blockSensitivityAt f) (mem_filter.2 ⟨mem_univ x, h⟩) - -theorem blockSensitivityFor_le_blockSensitivity (f : BooleanFunction n) (b : Bool) : - blockSensitivityFor f b ≤ blockSensitivity f := - sup_mono (filter_subset _ _) - /-- **One-sided Nisan bound**: `C_b(f) ≤ s_{¬b}(f) bs_b(f)`. -/ theorem certificateComplexityFor_le_sensitivityFor_mul_blockSensitivityFor (f : BooleanFunction n) (b : Bool) : @@ -364,6 +341,54 @@ theorem complexity_le_blockSensitivityFor_mul_certificateComplexityFor (f : Bool rw [hScard, Nat.succ_mul, add_comm] exact Nat.add_le_add_left (certificateComplexityAt_le_certificateComplexityFor hw) _ +/-- **Decision tree complexity from one-sided measures**: `D(f) ≤ bs_{¬b}(f) C_b(f)` for either +value `b`. For `b = 1` this is `D(f) ≤ bs₀(f) C₁(f)`, a one-sided form of the bound of Beals, +Buhrman, Cleve, Mosca and de Wolf [BealsBuhrmanCleveMoscaDeWolf2001]; negating the function gives +the dual `D(f) ≤ bs₁(f) C₀(f)`. -/ +theorem complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor + (f : BooleanFunction n) (b : Bool) : + complexity f ≤ blockSensitivityFor f (!b) * certificateComplexityFor f b := by + cases b with + | false => + have := complexity_le_blockSensitivityFor_mul_certificateComplexityFor (fun y => !f y) + rwa [complexity_not, blockSensitivityFor_not, certificateComplexityFor_not] at this + | true => exact complexity_le_blockSensitivityFor_mul_certificateComplexityFor f + +/-- `D(f) ≤ C_b(f) bs(f)` for either value `b` [BealsBuhrmanCleveMoscaDeWolf2001]. -/ +theorem complexity_le_certificateComplexityFor_mul_blockSensitivity (f : BooleanFunction n) + (b : Bool) : complexity f ≤ certificateComplexityFor f b * blockSensitivity f := + (complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor f b).trans (by + rw [mul_comm] + exact Nat.mul_le_mul_left _ (blockSensitivityFor_le_blockSensitivity f _)) + +/-- `D(f) ≤ min(C₀(f), C₁(f)) bs(f)`. -/ +theorem complexity_le_min_certificateComplexityFor_mul_blockSensitivity (f : BooleanFunction n) : + complexity f ≤ + min (certificateComplexityFor f false) (certificateComplexityFor f true) * + blockSensitivity f := by + rcases min_choice (certificateComplexityFor f false) (certificateComplexityFor f true) with h | h + all_goals + rw [h] + exact complexity_le_certificateComplexityFor_mul_blockSensitivity f _ + +/-- `D(f) ≤ bs_{¬b}(f) s_{¬b}(f) bs_b(f)`, from `D(f) ≤ bs_{¬b}(f) C_b(f)` and the one-sided Nisan +bound. -/ +theorem complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor + (f : BooleanFunction n) (b : Bool) : + complexity f ≤ blockSensitivityFor f (!b) * sensitivityFor f (!b) * blockSensitivityFor f b := + (complexity_le_blockSensitivityFor_not_mul_certificateComplexityFor f b).trans + ((Nat.mul_le_mul_left _ + (certificateComplexityFor_le_sensitivityFor_mul_blockSensitivityFor f b)).trans_eq + (Nat.mul_assoc _ _ _).symm) + +/-- `D(f) ≤ bs₀(f) bs₁(f) s(f)`. -/ +theorem complexity_le_blockSensitivityFor_mul_blockSensitivityFor_mul_sensitivity + (f : BooleanFunction n) : + complexity f ≤ blockSensitivityFor f false * blockSensitivityFor f true * sensitivity f := + (complexity_le_blockSensitivityFor_mul_sensitivityFor_mul_blockSensitivityFor f true).trans (by + rw [Nat.mul_right_comm] + exact Nat.mul_le_mul_left _ (sensitivityFor_le_sensitivity f _)) + /-- `D(f) ≤ C(f) bs(f)` [BealsBuhrmanCleveMoscaDeWolf2001]. -/ theorem complexity_le_certificateComplexity_mul_blockSensitivity (f : BooleanFunction n) : complexity f ≤ certificateComplexity f * blockSensitivity f := diff --git a/Complexity/Computability/QueryComplexity/Threshold.lean b/Complexity/Computability/QueryComplexity/Threshold.lean index b58236993b..289d0f41bb 100644 --- a/Complexity/Computability/QueryComplexity/Threshold.lean +++ b/Complexity/Computability/QueryComplexity/Threshold.lean @@ -7,11 +7,12 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.DecisionTree.Certificate +public import Complexity.Computability.QueryComplexity.OneSided +public import Complexity.Foundations.Data.BitString.Parity public import Complexity.Foundations.Data.BitString.Weight /-! -# Query complexity measures of threshold functions +# Query complexity measures of threshold functions and parity The threshold function `Th^n_j` says that at least `j` of `n` bits are true. A coordinate `i` is sensitive for it at `x` exactly when `x` has weight `j` and `x i` is true, or (for `j ≥ 1`) weight @@ -24,7 +25,9 @@ measures agree: for `1 ≤ j ≤ n`, In particular majority has sensitivity `⌊n/2⌋ + 1` for `n ≥ 1`. The disjunction `OR_n = Th^n_1` is sensitive to every bit at the all-false input, so `bs(OR_n) = n`. A single true bit certifies its value `1`, while certifying the value `0` takes all `n` bits. -The measures are those of [BuhrmanDeWolf2002]. +Flipping any bit flips the parity, so parity is sensitive to every bit at every input +(`BitString.sensitivityAt_parity`), and its sensitivity, block sensitivity and certificate +complexity all equal `n`. The measures are those of [BuhrmanDeWolf2002]. ## Main results @@ -38,6 +41,8 @@ The measures are those of [BuhrmanDeWolf2002]. * `Cslib.QueryComplexity.certificateComplexityFor_threshold_one_right_true`, `Cslib.QueryComplexity.certificateComplexityFor_threshold_one_right_false`: `C₁(OR_n) = 1` for `n ≥ 1`, and `C₀(OR_n) = n`. +* `Cslib.BitString.sensitivity_parity`, `Cslib.QueryComplexity.blockSensitivity_parity`, + `Cslib.QueryComplexity.certificateComplexity_parity`: `s`, `bs` and `C` of `parity n` are `n`. ## References @@ -231,4 +236,38 @@ theorem certificateComplexityFor_threshold_one_right_false : end QueryComplexity +/-! ### Parity -/ + +namespace BitString + +/-- Parity is sensitive to every bit at every input. -/ +theorem sensitivityAt_parity (x : BitString n) : sensitivityAt (parity n) x = n := by + have : (univ.filter fun i => parity n (Function.update x i !x i) ≠ parity n x) = univ := by + refine eq_univ_of_forall fun i => mem_filter.2 ⟨mem_univ i, ?_⟩ + rw [parity, parityOn_update_not (mem_univ i)] + cases parityOn univ x <;> decide + change #(univ.filter fun i => parity n (Function.update x i !x i) ≠ parity n x) = n + rw [this, card_univ, Fintype.card_fin] + +/-- The sensitivity of parity is its number of coordinates. -/ +theorem sensitivity_parity : sensitivity (parity n) = n := + le_antisymm (sensitivity_le_card _) ((sensitivityAt_parity (fun _ => false)).symm.trans_le + (sensitivityAt_le_sensitivity _ _)) + +end BitString + +namespace QueryComplexity + +/-- The block sensitivity of parity is its number of coordinates. -/ +theorem blockSensitivity_parity : blockSensitivity (parity n) = n := + le_antisymm (blockSensitivity_le_card _) + (sensitivity_parity.symm.trans_le (sensitivity_le_blockSensitivity _)) + +/-- The certificate complexity of parity is its number of coordinates. -/ +theorem certificateComplexity_parity : certificateComplexity (parity n) = n := + le_antisymm (certificateComplexity_le_card _) + (blockSensitivity_parity.symm.trans_le (blockSensitivity_le_certificateComplexity _)) + +end QueryComplexity + end Cslib diff --git a/ComplexityTests/QueryComplexity/Sensitivity.lean b/ComplexityTests/QueryComplexity/Sensitivity.lean index 6e96201b58..705ba030f5 100644 --- a/ComplexityTests/QueryComplexity/Sensitivity.lean +++ b/ComplexityTests/QueryComplexity/Sensitivity.lean @@ -47,6 +47,10 @@ example {n : ℕ} : sensitivityAt (threshold n 1) (fun _ => false) = n ∧ blockSensitivity (threshold n 1) = n := ⟨sensitivityAt_threshold_one_right, blockSensitivity_threshold_one_right⟩ +example {n : ℕ} : sensitivity (parity n) = n ∧ blockSensitivity (parity n) = n ∧ + certificateComplexity (parity n) = n := + ⟨sensitivity_parity, blockSensitivity_parity, certificateComplexity_parity⟩ + /-! ### Evasiveness -/ example : DecisionTree.complexity (majority 4) = 4 ∧ DecisionTree.complexity (threshold 7 5) = 7 :=