Model.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial thresholds and average sensitivity

The Boolean cube encodes the sign cube {−1,1}^n: false represents −1 and true represents 1. The public statement quantifies directly over real multilinear polynomials and uses uniform counting probability, the convention sign(0) = 1, and the exact constant 8.

GotsmanLinialStatement is a proposition definition, not a proof of the bound.

abbrev OAI.LeanBlast.GotsmanLinial.Cube line 25
Source documentation
The sign cube {−1,1}^n, with Boolean coordinates encoding the signs.
Also declared: ComparatorChallenges/CourtadeKumar.lean:9 (same declaration text), ComparatorChallenges/GotsmanLinial.lean:13 (same declaration text).
```
abbrev Cube (n : ℕ) := Fin n → Bool
```
def OAI.LeanBlast.GotsmanLinial.cubeCoord line 28
Source documentation
Interpret a Boolean cube coordinate as the corresponding real sign.
Also declared: ComparatorChallenges/GotsmanLinial.lean:15 (same declaration text).
```
def cubeCoord {n : ℕ} (x : Cube n) (i : Fin n) : ℝ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.flip line 32
Source documentation
Reverse one coordinate of a cube vertex.
Also declared: ComparatorChallenges/GotsmanLinial.lean:18 (same declaration text).
```
def flip {n : ℕ} (i : Fin n) (x : Cube n) : Cube n :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.thresholdSign line 36
Source documentation
The threshold convention assigns 1 at zero.
Also declared: ComparatorChallenges/GotsmanLinial.lean:21 (same declaration text).
```
noncomputable def thresholdSign (t : ℝ) : ℝ :=
…
```
def OAI.LeanBlast.GotsmanLinial.sensitiveVertices line 40
Source documentation
Vertices at which reversing coordinate i changes the function.
Also declared: ComparatorChallenges/GotsmanLinial.lean:24 (same declaration text).
```
noncomputable def sensitiveVertices {n : ℕ} (f : Cube n → ℝ) (i : Fin n) :
    Finset (Cube n) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.sensitiveEdgeCount line 46
Source documentation
Number of ordered sensitive edges, indexed by their initial vertex and direction.
```
noncomputable def sensitiveEdgeCount {n : ℕ} (f : Cube n → ℝ) : ℕ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.averageSensitivity line 50
Source documentation
Sum of the uniform probabilities that a coordinate flip changes f.
Also declared: ComparatorChallenges/GotsmanLinial.lean:29 (same declaration text).
```
noncomputable def averageSensitivity {n : ℕ} (f : Cube n → ℝ) : ℝ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.IsMultilinear line 54
Source documentation
Every exponent in every supported monomial is at most one.
Also declared: ComparatorChallenges/GotsmanLinial.lean:32 (same declaration text).
```
def IsMultilinear {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : Prop :=
…
```
def OAI.LeanBlast.GotsmanLinial.polynomialValue line 58
Source documentation
Evaluate a real polynomial at the signs represented by a cube vertex.
Also declared: ComparatorChallenges/GotsmanLinial.lean:35 (same declaration text).
```
noncomputable def polynomialValue {n : ℕ} (p : MvPolynomial (Fin n) ℝ)
    (x : Cube n) : ℝ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.polynomialThreshold line 63
Source documentation
The polynomial threshold function with the nonnegative-at-zero convention.
Also declared: ComparatorChallenges/GotsmanLinial.lean:39 (same declaration text).
```
noncomputable def polynomialThreshold {n : ℕ} (p : MvPolynomial (Fin n) ℝ) :
    Cube n → ℝ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.GotsmanLinialStatement line 68
Source documentation
The average-sensitivity bound for positive dimension and degree at most the dimension.
Also declared: ComparatorChallenges/GotsmanLinial.lean:43 (same declaration text).
```
def GotsmanLinialStatement : Prop :=
…
```