Gluing two points along a set of coordinates

glue F z u agrees with u on F and with z off F; it is the point γ_F(z,u) of Section 5.1 of the paper. For fixed F and z the map u ↦ glue F z u parametrises the subcube through z with free coordinates F (with multiplicity 2 ^ (n - |F|)), and (z, u) ↦ (glue F z u, glue F u z) is an involution of Cube ι × Cube ι.

The file proves the gluing lemma (Lemma 5.1 of the paper): part (i) is glue_flipSet, with the special cases glue_antipode, glue_flipSet_singleton_of_mem and glue_flipSet_singleton_of_not_mem; part (ii) is sum_sum_glue.

def AaronsonAmbainis.glue {ι : Type u_1} [DecidableEq ι] (F : Finset ι) (z u : Cube ι) : Cube ι

glue F z u agrees with u on F and with z off F.

Equations

• AaronsonAmbainis.glue F z u i = if i ∈ F then u i else z i

theorem AaronsonAmbainis.glue_flipSet {ι : Type u_1} [DecidableEq ι] (F : Finset ι) (z u : Cube ι) (S : Finset ι) : glue F z (flipSet u S) = flipSet (glue F z u) (S ∩ F)

theorem AaronsonAmbainis.glue_antipode {ι : Type u_1} [DecidableEq ι] (F : Finset ι) (z u : Cube ι) : glue F z (antipode u) = flipSet (glue F z u) F

theorem AaronsonAmbainis.glue_flipSet_singleton_of_mem {ι : Type u_1} [DecidableEq ι] {F : Finset ι} {j : ι} (hj : j ∈ F) (z u : Cube ι) : glue F z (flipSet u {j}) = flipSet (glue F z u) {j}

theorem AaronsonAmbainis.glue_flipSet_singleton_of_not_mem {ι : Type u_1} [DecidableEq ι] {F : Finset ι} {j : ι} (hj : j ∉ F) (z u : Cube ι) : glue F z (flipSet u {j}) = glue F z u

theorem AaronsonAmbainis.glue_glue_swap {ι : Type u_1} [DecidableEq ι] (F : Finset ι) (z u : Cube ι) : glue F (glue F z u) (glue F u z) = z

def AaronsonAmbainis.glueEquiv {ι : Type u_1} [DecidableEq ι] (F : Finset ι) : Cube ι × Cube ι ≃ Cube ι × Cube ι

The double-counting involution (z, u) ↦ (glue F z u, glue F u z).

Equations

• One or more equations did not get rendered due to their size.

theorem AaronsonAmbainis.sum_sum_glue {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Finset ι) (φ : Cube ι → ℝ) : ∑ z : Cube ι, ∑ u : Cube ι, φ (glue F z u) = 2 ^ Fintype.card ι * ∑ x : Cube ι, φ x

Every point x is glue F z u for exactly 2 ^ n pairs (z, u).