Conversation
… Tree Complexity). Defines sensitivity, block sensitivity and certificate complexity.
| abbrev Cube (n : ℕ) : Type := Fin n → Bool | ||
|
|
||
| /-- `f : {0,1}ⁿ → {0,1}`. -/ | ||
| abbrev BoolFunc (n : ℕ) : Type := Cube n → Bool |
There was a problem hiding this comment.
I mean it's kind of trivial but maybe you should sync some of the definitions here with #890 ?
|
|
||
| ## Main definitions | ||
|
|
||
| - `Cube n`: bit strings of length `n`, i.e. `Fin n → Bool`. |
There was a problem hiding this comment.
Do you have a reference for naming this object Cube? Wouldn't "Assignment" be easier to understand?
There was a problem hiding this comment.
Cube is short for the boolean hypercube (or hamming cube) which views {0,1}^n as vertices of a graph such that two strings are connected by an edge if their hamming distance is 1. Analysis of Boolean Functions by O'Donnell also calls it that.
If you prefer not to have Cube, then would something like "Input" or "BooleanInput" be better than "Assignment"?
"Assignment" is the term used for partial assignments in the survey by BuhrmanDeWolf. See the section Certificate Complexity.
| - `BoolFunc n`: Boolean functions `Cube n → Bool`. | ||
| - `Block n`: a set of coordinates. | ||
| - `flipBit`, `flipBlock`: flipping one coordinate, or every coordinate of a block. | ||
| - `Assignment n`: a partial assignment, fixing some coordinates and leaving others free. |
There was a problem hiding this comment.
If you rename Cube to Assignment, then this could be PartialAssignment (and also could be in general)
There was a problem hiding this comment.
My bad, my main reference and the place I studied this topic from is the Buhrman and de Wolf survey so most of my naming choices match that rather than Arora-Barak. I've addressed this in my previous comment.
| /-- `f : {0,1}ⁿ → {0,1}`. -/ | ||
| abbrev BoolFunc (n : ℕ) : Type := Cube n → Bool | ||
|
|
||
| /-- A block: a set of coordinates. -/ |
There was a problem hiding this comment.
Sorry that I have so many remarks about terminology and please push back, but Arora-Bark talks about "bit position". I know it makes sense when talking about hypercubes and so on, but currently, "index" would be equally valid and understandable, right?
There was a problem hiding this comment.
I agree, "index" and "coordinate" are interchangeable. I'd keep "coordinate" because thats what most of the definitions about blocks use in the file.
| ∀ P ∈ F, ∀ Q ∈ F, P ≠ Q → Disjoint P Q) Iff.rfl | ||
|
|
||
| /-- All sensitive families. -/ | ||
| def sensitiveFamilies (f : BoolFunc n) (x : Cube n) : Finset (Finset (Block n)) := |
There was a problem hiding this comment.
Do we really need this definition?
|
Sorry for the many comments! In general, this is a good contribution, it just has so many definitions :) |
Sure, I'll send you a zulip dm and make a thread about this topic in a bit. |
2 participants
Defines three Boolean function complexity measures : sensitivity
s(f), block sensitivitybs(f)and certificate complexityC(f)with the inequality chain :s(f) ≤ bs(f) ≤ C(f).Defs.leansets up the boolean hypercube and boolean functions which is defined as a function from{0,1}^nto{0,1}.Measures.leandefines the above three measures and proves the inequality chain.D(f): the decision tree complexity of boolean functionfwill follow in a second PR.AI usage : Used claude to help me fill in proofs in a few places and refactor my handwritten proofs.