refactor(query-complexity): consolidate one-sided measures and move parity measures (#610)

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`. -/

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. -/

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
 

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