Main.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the Gotsman--Linial average-sensitivity bound

The first lemmas are explicitly conditional assembly bridges. The final theorems discharge their matrix and counting hypotheses using the concrete weighted Boolean-cube grading and a sign-preserving constant perturbation.

theorem OAI.LeanBlast.GotsmanLinial.normalized_edge_bound line 26
Source documentation
The two analytic constants combine to the constant 8 after normalizing by the number of cube vertices. This is only a scalar bridge.
```
theorem normalized_edge_bound {N C T a : ℝ} (hN : 0 < N)
    (hedge : C ≤ 2 * T) (henergy : T ≤ 4 * a * N) :
    C / N ≤ 8 * a := by
…
```
theorem OAI.LeanBlast.GotsmanLinial.sensitivity_bound_of_counting_energy line 37
Source documentation
Convert a counted-edge identity, edge recovery, and an anticommutator energy estimate into the desired sensitivity inequality. The counting and energy premises are explicit.
```
theorem sensitivity_bound_of_counting_energy {n d : ℕ}
    (f : Cube n → ℝ) (C T : ℝ)
    (hcount : averageSensitivity f = C / (2 : ℝ) ^ n)
    (hedge : C ≤ 2 * T)
    (henergy : T ≤ 4 * ((d : ℝ) * Real.sqrt (n : ℝ)) * (2 : ℝ) ^ n) :
    averageSensitivity f ≤ 8 * (d : ℝ) * Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.averageSensitivity

theorem OAI.LeanBlast.GotsmanLinial.sensitivity_bound_of_cube_grading line 49

Source documentation

The finite-matrix bound assuming an orthogonal projection family with binomial multiplicities, coordinate tridiagonality, and low-block vanishing.

theorem sensitivity_bound_of_cube_grading {n d : ℕ}
    (f : Cube n → ℝ) (hf : ∀ x, f x = 1 ∨ f x = -1)
    (P : Fin (n + 1) → Matrix (Cube n) (Cube n) ℂ)
    (hP : OrthogonalProjectionFamily P)
    (htrace : ∀ k, (Matrix.trace (P k)).re = (n.choose k.val : ℝ))
    (htri : ∀ i : Fin n, BlockTridiagonal P (coordinateSignMatrix i))
    (hvanish : ∀ r s : Fin (n + 1), r.val + s.val < n - d →
      P s * signMatrix (fun x => fullParity x * f x) * P r = 0) :
    averageSensitivity f ≤ 8 * (d : ℝ) * Real.sqrt (n : ℝ) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.BlockTridiagonal, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix, OAI.LeanBlast.GotsmanLinial.signMatrix, OAI.LeanBlast.GotsmanLinial.fullParity, OAI.LeanBlast.GotsmanLinial.averageSensitivity

theorem OAI.LeanBlast.GotsmanLinial.polynomialThreshold_averageSensitivity_le_of_nonzero line 95
Source documentation
The bound for a polynomial without cube zeros. The projection family and both block-vanishing properties are constructed from its absolute value, rather than retained as hypotheses.
```
theorem polynomialThreshold_averageSensitivity_le_of_nonzero {n d : ℕ}
    (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d)
    (hnz : ∀ x : Cube n, polynomialValue p x ≠ 0) :
    averageSensitivity (polynomialThreshold p) ≤ 8 * (d : ℝ) * Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.averageSensitivity, OAI.LeanBlast.GotsmanLinial.polynomialThreshold
theorem OAI.LeanBlast.GotsmanLinial.polynomialThreshold_averageSensitivity_le line 114
Source documentation
Every real multilinear polynomial of degree at most d has average sensitivity at most 8*d*sqrt(n), including cube zeros under sign(0)=1. The argument in fact covers all natural n and d.
```
theorem polynomialThreshold_averageSensitivity_le {n d : ℕ}
    (p : MvPolynomial (Fin n) ℝ) (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) :
    averageSensitivity (polynomialThreshold p) ≤ 8 * (d : ℝ) * Real.sqrt (n : ℝ) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.averageSensitivity, OAI.LeanBlast.GotsmanLinial.polynomialThreshold
theorem OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement line 123
Source documentation
The average-sensitivity bound for 1 ≤ d ≤ n, without auxiliary construction hypotheses.
Distinct definitions of this name: ComparatorChallenges/GotsmanLinial.lean:49 (same statement text; different proof or body). Qualify references as OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement@path.
```
theorem gotsmanLinialStatement : GotsmanLinialStatement := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.GotsmanLinialStatement