CubeOperators.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate commutators and Hamming-distance energy

The coordinate sign matrices are the actual diagonal operators of the Boolean cube. The identities here turn their Hilbert--Schmidt and entry estimates into the energy estimates used by the edge-recovery argument.

theorem OAI.LeanBlast.GotsmanLinial.coordinate_commutator_apply line 24
Source documentation
In the point basis, a coordinate commutator records the difference of the two endpoint signs.
```
theorem coordinate_commutator_apply
    (M : Matrix (Cube n) (Cube n) ℂ) (i : Fin n) (x y : Cube n) :
    (M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y =
      (((cubeCoord y i - cubeCoord x i : ℝ) : ℂ)) * M x y := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix, OAI.LeanBlast.GotsmanLinial.cubeCoord
theorem OAI.LeanBlast.GotsmanLinial.coordinate_commutator_sq_norm line 34
Source documentation
Squaring a coordinate difference gives four exactly on the coordinates where the Boolean endpoints differ.
```
theorem coordinate_commutator_sq_norm
    (M : Matrix (Cube n) (Cube n) ℂ) (i : Fin n) (x y : Cube n) :
    ‖(M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y‖ ^ 2 =
      (if x i ≠ y i then (4 : ℝ) else 0) * ‖M x y‖ ^ 2 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix

theorem OAI.LeanBlast.GotsmanLinial.sum_coordinate_commutator_sq_norm line 43

Source documentation

Summing the squared entries over coordinates counts Hamming distance.

theorem sum_coordinate_commutator_sq_norm
    (M : Matrix (Cube n) (Cube n) ℂ) (x y : Cube n) :
    (∑ i : Fin n,
      ‖(M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y‖ ^ 2) =
      4 * (hammingDist x y : ℝ) * ‖M x y‖ ^ 2 := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix

theorem OAI.LeanBlast.GotsmanLinial.sum_hsNormSq_coordinate_commutator line 60
Source documentation
The total coordinate-commutator energy is four times the distance-weighted entry energy.
```
theorem sum_hsNormSq_coordinate_commutator
    (M : Matrix (Cube n) (Cube n) ℂ) :
    (∑ i : Fin n, hsNormSq (M * coordinateSignMatrix i - coordinateSignMatrix i * M)) =
      4 * ∑ x : Cube n, ∑ y : Cube n, (hammingDist x y : ℝ) * ‖M x y‖ ^ 2 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix
theorem OAI.LeanBlast.GotsmanLinial.distance_energy_le_of_coordinate_commutator_bound line 82
Source documentation
A uniform coordinate-commutator Hilbert--Schmidt bound gives the distance energy inequality for the actual cube matrix.
```
theorem distance_energy_le_of_coordinate_commutator_bound
    (M : Matrix (Cube n) (Cube n) ℂ)
    (hbound : ∀ i : Fin n,
      hsNormSq (M * coordinateSignMatrix i - coordinateSignMatrix i * M) ≤ (2 : ℝ) ^ n) :
    (∑ x : Cube n, ∑ y : Cube n, (hammingDist x y : ℝ) * ‖M x y‖ ^ 2) ≤
      (n : ℝ) * (2 : ℝ) ^ n / 4 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix
theorem OAI.LeanBlast.GotsmanLinial.off_diagonal_sq_norm_le_quarter_of_commutator_bound line 95
Source documentation
A coordinate at which distinct endpoints differ turns an entrywise commutator estimate into the edge-entry cap 1/4.
```
theorem off_diagonal_sq_norm_le_quarter_of_commutator_bound
    (M : Matrix (Cube n) (Cube n) ℂ)
    (hbound : ∀ (i : Fin n) (x y : Cube n),
      ‖(M * coordinateSignMatrix i - coordinateSignMatrix i * M) x y‖ ^ 2 ≤ 1)
    (x y : Cube n) (hxy : x ≠ y) : ‖M x y‖ ^ 2 ≤ (1 : ℝ) / 4 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.coordinateSignMatrix